Tame ramification and the different

AbbreviationGraded pieces of the maximal-ideal filtration#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\). For \(i \in \mathbb{N}\), the \(i\)-th graded piece is the \(R\)-module \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\), realized as the quotient of the ideal \(\mathfrak{m}^i\), viewed as an \(R\)-module, by its submodule \(\mathfrak{m} \cdot \mathfrak{m}^i\).

abbrev MaximalIdealGradedPiece (i : ℕ) :=
  ((IsLocalRing.maximalIdeal R) ^ i : Ideal R) ⧸
    (IsLocalRing.maximalIdeal R • ⊤ :
      Submodule R ((IsLocalRing.maximalIdeal R) ^ i : Ideal R))
Used by 10
Used byGraded pieces of a DVR are one-dimensional · Graded pieces of a DVR as copies of the residue field · The residue-field isomorphism intertwines multiplication · Graded pieces as kernels of the transition maps · The kernel identification on representatives · Multiplication by a residue class on a graded piece · Multiplication by a residue class on representatives · One-step trace recurrence for the maximal-ideal-power quotients · Trace on the maximal-ideal-power quotients · Trace of multiplication on a graded piece

DefinitionGraded pieces of a DVR as copies of the residue field#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\), and let \(\varpi\) be a generator of \(\mathfrak{m}\) chosen once and for all. For \(i \in \mathbb{N}\), the map \(\kappa \to \mathfrak{m}^i/\mathfrak{m}^{i+1}\) sending the class of \(r \in R\) to the class of \(r \varpi^i\) is a \(\kappa\)-linear isomorphism.

Here \(\kappa\) acts on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\) through \(R\), which is well defined because \(\mathfrak{m}\) annihilates the graded piece.

noncomputable def residueFieldLinearEquivMaximalIdealGradedPiece (i : ℕ) :
    IsLocalRing.ResidueField R ≃ₗ[IsLocalRing.ResidueField R]
      MaximalIdealGradedPiece R i :=
  let e : (R ⧸ IsLocalRing.maximalIdeal R) ≃ₗ[R] MaximalIdealGradedPiece R i :=
    Ideal.quotEquivPowQuotPowSucc
      (IsPrincipalIdealRing.principal _) (not_a_field R) i
  { e with
    map_smul' := fun q x => by
      obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective q
      exact e.map_smul r x }
Uses 1 · Used by 3
Statement usesGraded pieces of the maximal-ideal filtration
Used byGraded pieces of a DVR are one-dimensional · The residue-field isomorphism intertwines multiplication · Trace of multiplication on a graded piece

TheoremGraded pieces of a DVR are one-dimensional#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\). For every \(i \in \mathbb{N}\), the graded piece \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\) is a vector space of dimension one over \(\kappa\).

theorem finrank_maximalIdealGradedPiece (i : ℕ) :
    Module.finrank (IsLocalRing.ResidueField R)
      (MaximalIdealGradedPiece R i) = 1
Uses 2
Statement usesGraded pieces of the maximal-ideal filtration
Proof usesGraded pieces of a DVR as copies of the residue field

DefinitionMultiplication by a residue class on a graded piece#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\). For \(a \in \kappa\) and \(i \in \mathbb{N}\), this is the \(\kappa\)-linear endomorphism \(x \mapsto a x\) of the graded piece \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\).

noncomputable def residueFieldMulMaximalIdealGradedPiece
    (a : IsLocalRing.ResidueField R) (i : ℕ) :
    Module.End (IsLocalRing.ResidueField R) (MaximalIdealGradedPiece R i) :=
  LinearMap.lsmul _ _ a
Uses 1 · Used by 4
Statement usesGraded pieces of the maximal-ideal filtration
Used byThe residue-field isomorphism intertwines multiplication · Multiplication by a residue class on representatives · One-step trace recurrence for the maximal-ideal-power quotients · Trace of multiplication on a graded piece

TheoremMultiplication by a residue class on representatives#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\). For \(x \in R\), \(i \in \mathbb{N}\) and \(y \in \mathfrak{m}^i\), multiplication by the residue class \(\bar{x} \in \kappa\) on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\) sends the class of \(y\) to the class of \(x y\).

@[simp]
theorem residueFieldMulMaximalIdealGradedPiece_residue_mk
    (x : R) (i : ℕ) (y : ((IsLocalRing.maximalIdeal R) ^ i : Ideal R)) :
    residueFieldMulMaximalIdealGradedPiece R (IsLocalRing.residue R x) i
        (Submodule.Quotient.mk y) =
      Submodule.Quotient.mk (x • y)
Uses 2 · Used by 1
Statement usesGraded pieces of the maximal-ideal filtration · Multiplication by a residue class on a graded piece
Used byOne-step trace recurrence for the maximal-ideal-power quotients

TheoremThe residue-field isomorphism intertwines multiplication#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\), let \(i \in \mathbb{N}\), and let \(e : \kappa \to \mathfrak{m}^i/\mathfrak{m}^{i+1}\) be the \(\kappa\)-linear isomorphism of the residue field with the graded piece. Let \(K\) be a field, with a \(K\)-algebra structure on \(\kappa\) and a \(K\)-module structure on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\) such that \((c b) x = c (b x)\) for all \(c \in K\), \(b \in \kappa\) and \(x \in \mathfrak{m}^i/\mathfrak{m}^{i+1}\). Then for every \(a \in \kappa\), writing \(\mu_a : \kappa \to \kappa\) for multiplication by \(a\), the \(K\)-linear map \(e \circ \mu_a \circ e^{-1}\) equals multiplication by \(a\) on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\), viewed as a \(K\)-linear map.

theorem residueFieldLinearEquivMaximalIdealGradedPiece_conj_lmul
    {K : Type*} [Field K] [Algebra K (IsLocalRing.ResidueField R)]
    (i : ℕ) [Module K (MaximalIdealGradedPiece R i)]
    [IsScalarTower K (IsLocalRing.ResidueField R) (MaximalIdealGradedPiece R i)]
    (a : IsLocalRing.ResidueField R) :
    ((residueFieldLinearEquivMaximalIdealGradedPiece R i).restrictScalars K).conj
        (Algebra.lmul K (IsLocalRing.ResidueField R) a) =
      (residueFieldMulMaximalIdealGradedPiece R a i).restrictScalars K
Uses 3 · Used by 1
Statement usesGraded pieces of the maximal-ideal filtration · Graded pieces of a DVR as copies of the residue field · Multiplication by a residue class on a graded piece
Used byTrace of multiplication on a graded piece

TheoremTrace of multiplication on a graded piece#✓fully proved

Let \(R\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and residue field \(\kappa = R/\mathfrak{m}\), let \(i \in \mathbb{N}\), and let \(K\) be a field, with a \(K\)-algebra structure on \(\kappa\) and a \(K\)-module structure on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\) such that \((c b) x = c (b x)\) for all \(c \in K\), \(b \in \kappa\) and \(x \in \mathfrak{m}^i/\mathfrak{m}^{i+1}\). Then for every \(a \in \kappa\), the trace of multiplication by \(a\) on \(\mathfrak{m}^i/\mathfrak{m}^{i+1}\), as a \(K\)-linear map, equals the trace \(\operatorname{Tr}_{\kappa/K}(a)\).

Each trace is taken to be \(0\) when the corresponding space is not finite-dimensional over \(K\).

theorem trace_residueFieldMulMaximalIdealGradedPiece
    {K : Type*} [Field K] [Algebra K (IsLocalRing.ResidueField R)]
    (i : ℕ) [Module K (MaximalIdealGradedPiece R i)]
    [IsScalarTower K (IsLocalRing.ResidueField R) (MaximalIdealGradedPiece R i)]
    (a : IsLocalRing.ResidueField R) :
    LinearMap.trace K (MaximalIdealGradedPiece R i)
        ((residueFieldMulMaximalIdealGradedPiece R a i).restrictScalars K) =
      Algebra.trace K (IsLocalRing.ResidueField R) a
Uses 4 · Used by 1
Statement usesGraded pieces of the maximal-ideal filtration · Multiplication by a residue class on a graded piece
Proof usesGraded pieces of a DVR as copies of the residue field · The residue-field isomorphism intertwines multiplication
Used byOne-step trace recurrence for the maximal-ideal-power quotients

AbbreviationQuotient by the extended maximal ideal plus a maximal-ideal power#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For a natural number \(n\), this is the quotient ring \(B / (\mathfrak m_A B + \mathfrak m_B^n)\).

abbrev ResidueFieldMaximalIdealPowQuotient (n : ℕ) : Type _ :=
  B ⧸ (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ n :
    Ideal B)
Used by 10
Used byTransition map between maximal-ideal-power quotients · Surjectivity of the transition maps between maximal-ideal-power quotients · The transition map on residue classes · Graded pieces as kernels of the transition maps · The kernel identification on representatives · Ring isomorphism with the quotient by a power of the maximal ideal · The power-quotient isomorphism on residue classes · Residue of the integral trace · One-step trace recurrence for the maximal-ideal-power quotients · Trace on the maximal-ideal-power quotients

TheoremCollapse of the quotient-defining ideal#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For every natural number \(n\), if \(\mathfrak m_A B \subseteq \mathfrak m_B^n\), then \(\mathfrak m_A B + \mathfrak m_B^n = \mathfrak m_B^n\).

theorem maximalIdealPowQuotientIdeal_eq (n : ℕ)
    (h : Ideal.map (algebraMap A B) (maximalIdeal A) ≤ maximalIdeal B ^ n) :
    (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ n :
      Ideal B) = maximalIdeal B ^ n
Used by 1
Used byRing isomorphism with the quotient by a power of the maximal ideal

TheoremThe quotient-defining ideals decrease#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For every natural number \(n\), the ideal \(\mathfrak m_A B + \mathfrak m_B^{n+1}\) is contained in \(\mathfrak m_A B + \mathfrak m_B^n\).

theorem maximalIdealPowQuotientIdeal_le (n : ℕ) :
    (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ (n + 1) :
      Ideal B) ≤
      Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ n
Used by 2
Used byTransition map between maximal-ideal-power quotients · Surjectivity of the transition maps between maximal-ideal-power quotients

DefinitionTransition map between maximal-ideal-power quotients#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\) and let \(\kappa_A = A/\mathfrak m_A\) be the residue field of \(A\). Let \(B\) be an \(A\)-algebra, write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\), and for each \(m\) let \(Q_m = B/(\mathfrak m_A B + \mathfrak m_B^m)\), a \(\kappa_A\)-algebra in which the class of \(r \in A\) acts as multiplication by the class of its image in \(B\). For a natural number \(n\), this is the \(\kappa_A\)-algebra homomorphism \(Q_{n+1} \to Q_n\) sending the class of each \(b \in B\) to its class in \(Q_n\); it is well defined because \(\mathfrak m_A B + \mathfrak m_B^{n+1} \subseteq \mathfrak m_A B + \mathfrak m_B^n\).

noncomputable def factorResidueFieldMaximalIdealPowQuotient (n : ℕ) :
    ResidueFieldMaximalIdealPowQuotient A B (n + 1) →ₐ[ResidueField A]
      ResidueFieldMaximalIdealPowQuotient A B n :=
  { Ideal.Quotient.factor (maximalIdealPowQuotientIdeal_le A B n) with
    commutes' := fun r => by
      obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective r
      rfl }
Uses 2 · Used by 6
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power · The quotient-defining ideals decrease
Used bySurjectivity of the transition maps between maximal-ideal-power quotients · The transition map on residue classes · Graded pieces as kernels of the transition maps · The kernel identification on representatives · One-step trace recurrence for the maximal-ideal-power quotients · Trace on the maximal-ideal-power quotients

TheoremSurjectivity of the transition maps between maximal-ideal-power quotients#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\), and for each \(m\) let \(Q_m = B/(\mathfrak m_A B + \mathfrak m_B^m)\). For every natural number \(n\), the transition homomorphism \(Q_{n+1} \to Q_n\) that sends the class of each \(b \in B\) to its class in \(Q_n\) is surjective.

theorem factorResidueFieldMaximalIdealPowQuotient_surjective (n : ℕ) :
    Function.Surjective (factorResidueFieldMaximalIdealPowQuotient A B n)
Uses 3 · Used by 2
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power · Transition map between maximal-ideal-power quotients
Proof usesThe quotient-defining ideals decrease
Used byOne-step trace recurrence for the maximal-ideal-power quotients · Trace on the maximal-ideal-power quotients

TheoremThe transition map on residue classes#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\), and for each \(m\) let \(Q_m = B/(\mathfrak m_A B + \mathfrak m_B^m)\). For every natural number \(n\) and every \(b \in B\), the transition homomorphism \(Q_{n+1} \to Q_n\) maps the class of \(b\) in \(Q_{n+1}\) to the class of \(b\) in \(Q_n\).

@[simp]
theorem factorResidueFieldMaximalIdealPowQuotient_mk (n : ℕ) (b : B) :
    factorResidueFieldMaximalIdealPowQuotient A B n
        (Ideal.Quotient.mk _ b) =
      Ideal.Quotient.mk _ b
Uses 2 · Used by 1
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power · Transition map between maximal-ideal-power quotients
Used byGraded pieces as kernels of the transition maps

DefinitionRing isomorphism with the quotient by a power of the maximal ideal#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For a natural number \(n\) with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\), this is the ring isomorphism \(B/(\mathfrak m_A B + \mathfrak m_B^n) \cong B/\mathfrak m_B^n\) sending the class of each \(b \in B\) to the class of \(b\); it exists because the two ideals are equal.

noncomputable def residueFieldMaximalIdealPowQuotientEquivPow (n : ℕ)
    (h : Ideal.map (algebraMap A B) (maximalIdeal A) ≤ maximalIdeal B ^ n) :
    ResidueFieldMaximalIdealPowQuotient A B n ≃+* B ⧸ maximalIdeal B ^ n :=
  Ideal.quotEquivOfEq (maximalIdealPowQuotientIdeal_eq A B n h)
Uses 2 · Used by 2
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power · Collapse of the quotient-defining ideal
Used byGraded pieces as kernels of the transition maps · The power-quotient isomorphism on residue classes

TheoremThe power-quotient isomorphism on residue classes#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\), let \(B\) be an \(A\)-algebra, and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For every natural number \(n\) with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\) and every \(b \in B\), the ring isomorphism \(B/(\mathfrak m_A B + \mathfrak m_B^n) \cong B/\mathfrak m_B^n\) induced by the equality of these two ideals sends the class of \(b\) to the class of \(b\).

@[simp]
theorem residueFieldMaximalIdealPowQuotientEquivPow_mk (n : ℕ)
    (h : Ideal.map (algebraMap A B) (maximalIdeal A) ≤ maximalIdeal B ^ n)
    (b : B) :
    residueFieldMaximalIdealPowQuotientEquivPow A B n h
        (Ideal.Quotient.mk _ b) =
      Ideal.Quotient.mk _ b
Uses 2 · Used by 1
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power · Ring isomorphism with the quotient by a power of the maximal ideal
Used byGraded pieces as kernels of the transition maps

DefinitionGraded pieces as kernels of the transition maps#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\) and residue fields \(\kappa_A = A/\mathfrak m_A\) and \(\kappa_B = B/\mathfrak m_B\), let \(B\) be an \(A\)-algebra whose algebra map \(A \to B\) is a local homomorphism, so that it induces a field homomorphism \(\kappa_A \to \kappa_B\), and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For each \(m\) let \(Q_m = B/(\mathfrak m_A B + \mathfrak m_B^m)\), a \(\kappa_A\)-algebra in which the class of \(r \in A\) acts as multiplication by the class of its image in \(B\). Let \(n\) be a natural number with \(\mathfrak m_A B \subseteq \mathfrak m_B^{n+1}\), and suppose the \(\kappa_B\)-vector space \(\mathfrak m_B^n/\mathfrak m_B^{n+1}\) carries a \(\kappa_A\)-module structure such that \((\bar a c) \cdot x = a \cdot (c \cdot x)\) for all \(a \in \kappa_A\), \(c \in \kappa_B\) and \(x \in \mathfrak m_B^n/\mathfrak m_B^{n+1}\), where \(\bar a\) is the image of \(a\) in \(\kappa_B\). This is the \(\kappa_A\)-linear isomorphism from \(\mathfrak m_B^n/\mathfrak m_B^{n+1}\) onto the kernel of the \(\kappa_A\)-algebra homomorphism \(Q_{n+1} \to Q_n\) that sends the class of each \(b \in B\) to its class in \(Q_n\); it sends the class of each \(z \in \mathfrak m_B^n\) to the class of \(z\) in \(Q_{n+1}\).

residueFieldLinearEquivMaximalIdealGradedPieceKerFactor · 199 lines 
noncomputable def residueFieldLinearEquivMaximalIdealGradedPieceKerFactor
    (n : ℕ)
    (hSucc : Ideal.map (algebraMap A B) (maximalIdeal A) ≤
      maximalIdeal B ^ (n + 1))
    [IsLocalHom (algebraMap A B)]
    [Module (ResidueField A)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)]
    [IsScalarTower (ResidueField A) (ResidueField B)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)] :
    IsDiscreteValuationRing.MaximalIdealGradedPiece B n ≃ₗ[ResidueField A]
      LinearMap.ker (factorResidueFieldMaximalIdealPowQuotient A B n).toLinearMap := by
  have hpow : maximalIdeal B ^ (n + 1) ≤ maximalIdeal B ^ n :=
    Ideal.pow_le_pow_right n.le_succ
  have hmap : Ideal.map (algebraMap A B) (maximalIdeal A) ≤ maximalIdeal B ^ n :=
    le_trans hSucc hpow
  have hcomm : ∀ b : B,
      residueFieldMaximalIdealPowQuotientEquivPow A B n hmap
          (factorResidueFieldMaximalIdealPowQuotient A B n
            (Ideal.Quotient.mk _ b)) =
        Ideal.Quotient.factor hpow
          (residueFieldMaximalIdealPowQuotientEquivPow A B (n + 1) hSucc
            (Ideal.Quotient.mk _ b)) := by
    intro b
    rw [factorResidueFieldMaximalIdealPowQuotient_mk,
      residueFieldMaximalIdealPowQuotientEquivPow_mk,
      residueFieldMaximalIdealPowQuotientEquivPow_mk, Ideal.Quotient.factor_mk]
  let F : (maximalIdeal B ^ n : Ideal B) →
      LinearMap.ker (factorResidueFieldMaximalIdealPowQuotient A B n).toLinearMap :=
    fun x =>
      ⟨Ideal.Quotient.mk _ (x : B),
        LinearMap.mem_ker.mpr (by
          simp only [AlgHom.toLinearMap_apply,
            factorResidueFieldMaximalIdealPowQuotient_mk]
          exact Ideal.Quotient.eq_zero_iff_mem.mpr (Submodule.mem_sup_right x.2))⟩
  have F_add : ∀ x y : (maximalIdeal B ^ n : Ideal B),
      F (x + y) = F x + F y := by
    intro x y
    apply Subtype.ext
    change Ideal.Quotient.mk _ (((x + y : _) : B)) =
      Ideal.Quotient.mk _ ((x : B)) + Ideal.Quotient.mk _ ((y : B))
    rw [Submodule.coe_add, map_add]
  have hmem : ∀ a b : (maximalIdeal B ^ n : Ideal B),
      a - b ∈ (maximalIdeal B • ⊤ :
        Submodule B (maximalIdeal B ^ n : Ideal B)) →
      ((a - b : _) : B) ∈ maximalIdeal B ^ (n + 1) := by
    intro a b hab
    simpa [Submodule.mem_smul_top_iff, pow_succ'] using hab
  have F_resp : ∀ a b : (maximalIdeal B ^ n : Ideal B),
      a - b ∈ (maximalIdeal B • ⊤ :
        Submodule B (maximalIdeal B ^ n : Ideal B)) →
      F a = F b := by
    intro a b hab
    have h0 : F (a - b) = 0 := by
      apply Subtype.ext
      change Ideal.Quotient.mk _ (((a - b : _) : B)) = 0
      rw [Ideal.Quotient.eq_zero_iff_mem]
      exact Submodule.mem_sup_right (hmem a b hab)
    have hadd : a = b + (a - b) := by abel
    conv_lhs => rw [hadd]
    rw [F_add, h0, add_zero]
  let φ : IsDiscreteValuationRing.MaximalIdealGradedPiece B n →ₗ[ResidueField A]
      LinearMap.ker (factorResidueFieldMaximalIdealPowQuotient A B n).toLinearMap :=
    { toFun := fun q =>
        Quotient.lift F
          (fun a b h => F_resp a b ((Submodule.quotientRel_def _).mp h)) q
      map_add' := fun x y => by
        obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x
        obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ y
        have hadd : (Submodule.Quotient.mk (x + y) :
              IsDiscreteValuationRing.MaximalIdealGradedPiece B n) =
            (Submodule.Quotient.mk x + Submodule.Quotient.mk y :
              IsDiscreteValuationRing.MaximalIdealGradedPiece B n) := by
          change Submodule.mkQ (maximalIdeal B • ⊤ :
              Submodule B (maximalIdeal B ^ n : Ideal B)) (x + y) =
            Submodule.mkQ (maximalIdeal B • ⊤ :
              Submodule B (maximalIdeal B ^ n : Ideal B)) x +
              Submodule.mkQ (maximalIdeal B • ⊤ :
              Submodule B (maximalIdeal B ^ n : Ideal B)) y
          exact map_add _ _ _
        rw [← hadd]
        exact F_add x y
      map_smul' := fun c x => by
        obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective c
        obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ x
        obtain ⟨b, hb⟩ := y
        have hsmulG :
            IsLocalRing.residue A a •
              (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) :
                IsDiscreteValuationRing.MaximalIdealGradedPiece B n) =
              Submodule.Quotient.mk
                (⟨algebraMap A B a * b, Ideal.mul_mem_left _ _ hb⟩ :
                  (maximalIdeal B ^ n : Ideal B)) := by
          have htower :
              IsLocalRing.residue A a •
                (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) :
                  IsDiscreteValuationRing.MaximalIdealGradedPiece B n) =
                (algebraMap (ResidueField A) (ResidueField B)
                    (IsLocalRing.residue A a)) •
                  (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) :
                    IsDiscreteValuationRing.MaximalIdealGradedPiece B n) := by
            conv_lhs =>
              rw [← one_smul (ResidueField B)
                (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) :
                  IsDiscreteValuationRing.MaximalIdealGradedPiece B n),
                ← smul_assoc]
            congr 1
            rw [Algebra.smul_def, mul_one]
          rw [htower, IsLocalRing.ResidueField.algebraMap_residue]
          exact Module.Quotient.mk_smul_mk _ _ _ _
        rw [hsmulG]
        change F _ = IsLocalRing.residue A a •
          F (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B))
        apply Subtype.ext
        change Ideal.Quotient.mk _ (algebraMap A B a * b) =
          ((IsLocalRing.residue A a •
            F (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B))) :
            LinearMap.ker _).val
        rw [show ((IsLocalRing.residue A a •
              F (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B))) :
              LinearMap.ker _).val =
            IsLocalRing.residue A a •
              Ideal.Quotient.mk
                (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔
                  maximalIdeal B ^ (n + 1))
                b from rfl,
          Algebra.smul_def,
          show algebraMap (ResidueField A)
              (ResidueFieldMaximalIdealPowQuotient A B (n + 1))
              (IsLocalRing.residue A a) =
            Ideal.Quotient.mk _ (algebraMap A B a) from rfl, map_mul] }
  have hinj : Function.Injective φ := by
    rw [← LinearMap.ker_eq_bot]
    ext q
    simp only [Submodule.mem_bot, LinearMap.mem_ker]
    constructor
    · intro hq
      obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ q
      obtain ⟨b, hb⟩ := x
      have hF : F (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) = 0 := hq
      have hval : Ideal.Quotient.mk
          (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ (n + 1))
          b = 0 := congrArg Subtype.val hF
      have hB : Ideal.Quotient.mk (maximalIdeal B ^ (n + 1)) b = 0 := by
        have hcongr := congrArg
          (residueFieldMaximalIdealPowQuotientEquivPow A B (n + 1) hSucc) hval
        simpa [residueFieldMaximalIdealPowQuotientEquivPow_mk] using hcongr
      have hrep : Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow (maximalIdeal B) n
            (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B))) =
            (⟨Ideal.Quotient.mk (maximalIdeal B ^ (n + 1)) b,
              Ideal.mem_map_of_mem _ hb⟩ :
              Ideal.map (Ideal.Quotient.mk (maximalIdeal B ^ (n + 1)))
                (maximalIdeal B ^ n)) := rfl
      have e0 : Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow (maximalIdeal B) n
            (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B))) = 0 := by
        rw [hrep]
        simp [hB]
      have hzero : (Submodule.Quotient.mk (⟨b, hb⟩ : (maximalIdeal B ^ n : Ideal B)) :
          IsDiscreteValuationRing.MaximalIdealGradedPiece B n) = 0 := by
        have hinjE :=
          (Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow (maximalIdeal B) n).injective
        apply hinjE
        rw [e0, map_zero]
      exact hzero
    · intro hq
      rw [hq, map_zero]
  have hsurj : Function.Surjective φ := by
    rintro ⟨y, hy⟩
    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective y
    have hfactor0 : factorResidueFieldMaximalIdealPowQuotient A B n
        (Ideal.Quotient.mk _ b) = 0 :=
      LinearMap.mem_ker.mp hy
    have hkerB : Ideal.Quotient.factor hpow
        (residueFieldMaximalIdealPowQuotientEquivPow A B (n + 1) hSucc
          (Ideal.Quotient.mk _ b)) = 0 := by
      rw [← hcomm b, hfactor0, map_zero]
    have hmemMap :
        residueFieldMaximalIdealPowQuotientEquivPow A B (n + 1) hSucc
            (Ideal.Quotient.mk _ b) ∈
          Ideal.map (Ideal.Quotient.mk (maximalIdeal B ^ (n + 1)))
            (maximalIdeal B ^ n) := by
      rw [← Ideal.Quotient.factor_ker hpow]
      exact RingHom.mem_ker.mpr hkerB
    obtain ⟨b', hb', hbe⟩ := (Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective).mp
      hmemMap
    rw [residueFieldMaximalIdealPowQuotientEquivPow_mk] at hbe
    have hsub : Ideal.Quotient.mk (maximalIdeal B ^ (n + 1)) (b' - b) = 0 := by
      rw [map_sub, sub_eq_zero]
      exact hbe
    have hmem' : b' - b ∈ maximalIdeal B ^ (n + 1) :=
      Ideal.Quotient.eq_zero_iff_mem.mp hsub
    refine ⟨Submodule.Quotient.mk (⟨b', hb'⟩ : (maximalIdeal B ^ n : Ideal B)), ?_⟩
    apply Subtype.ext
    change Ideal.Quotient.mk
      (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ (n + 1)) b' =
      Ideal.Quotient.mk
        (Ideal.map (algebraMap A B) (maximalIdeal A) ⊔ maximalIdeal B ^ (n + 1)) b
    rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
    exact Submodule.mem_sup_right hmem'
  exact LinearEquiv.ofBijective φ ⟨hinj, hsurj⟩
Uses 6 · Used by 2
Statement usesGraded pieces of the maximal-ideal filtration · Quotient by the extended maximal ideal plus a maximal-ideal power · Transition map between maximal-ideal-power quotients · The transition map on residue classes · Ring isomorphism with the quotient by a power of the maximal ideal · The power-quotient isomorphism on residue classes
Used byThe kernel identification on representatives · One-step trace recurrence for the maximal-ideal-power quotients

TheoremThe kernel identification on representatives#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\) and \(\mathfrak m_B\) and residue fields \(\kappa_A = A/\mathfrak m_A\) and \(\kappa_B = B/\mathfrak m_B\), let \(B\) be an \(A\)-algebra whose algebra map \(A \to B\) is a local homomorphism, so that it induces a field homomorphism \(\kappa_A \to \kappa_B\), and write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). For each \(m\) let \(Q_m = B/(\mathfrak m_A B + \mathfrak m_B^m)\), a \(\kappa_A\)-algebra in which the class of \(r \in A\) acts as multiplication by the class of its image in \(B\). Let \(n\) be a natural number with \(\mathfrak m_A B \subseteq \mathfrak m_B^{n+1}\), and suppose the \(\kappa_B\)-vector space \(\mathfrak m_B^n/\mathfrak m_B^{n+1}\) carries a \(\kappa_A\)-module structure such that \((\bar a c) \cdot x = a \cdot (c \cdot x)\) for all \(a \in \kappa_A\), \(c \in \kappa_B\) and \(x \in \mathfrak m_B^n/\mathfrak m_B^{n+1}\), where \(\bar a\) is the image of \(a\) in \(\kappa_B\). Let \(\pi \colon Q_{n+1} \to Q_n\) be the \(\kappa_A\)-algebra homomorphism sending the class of each \(b \in B\) to its class in \(Q_n\). Then for every \(z \in \mathfrak m_B^n\), the \(\kappa_A\)-linear isomorphism from \(\mathfrak m_B^n/\mathfrak m_B^{n+1}\) onto \(\ker \pi\) sends the class of \(z\) to the class of \(z\) in \(Q_{n+1}\).

@[simp]
theorem residueFieldLinearEquivMaximalIdealGradedPieceKerFactor_mk (n : ℕ)
    (hSucc : Ideal.map (algebraMap A B) (maximalIdeal A) ≤
      maximalIdeal B ^ (n + 1))
    [IsLocalHom (algebraMap A B)]
    [Module (ResidueField A)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)]
    [IsScalarTower (ResidueField A) (ResidueField B)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)]
    (z : (maximalIdeal B ^ n : Ideal B)) :
    ((residueFieldLinearEquivMaximalIdealGradedPieceKerFactor A B n hSucc
        (Submodule.Quotient.mk z) :
        ResidueFieldMaximalIdealPowQuotient A B (n + 1)) =
      Ideal.Quotient.mk _ (z : B))
Uses 4
Statement usesGraded pieces of the maximal-ideal filtration · Quotient by the extended maximal ideal plus a maximal-ideal power · Transition map between maximal-ideal-power quotients · Graded pieces as kernels of the transition maps

TheoremOne-step trace recurrence for the maximal-ideal-power quotients#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra whose structure map is a local homomorphism. Write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\), and for each \(m\) let \(Q_m = B / (\mathfrak m_A B + \mathfrak m_B^m)\), a \(\kappa_A\)-algebra. Let \(n\) be a natural number with \(\mathfrak m_A B \subseteq \mathfrak m_B^{n+1}\), suppose \(Q_{n+1}\) is finite-dimensional over \(\kappa_A\), and equip the graded piece \(\mathfrak m_B^n / \mathfrak m_B^{n+1}\) with a \(\kappa_A\)-module structure compatible with its \(\kappa_B\)-module structure through \(\kappa_A \to \kappa_B\). Then for every \(b \in B\), writing \(\bar b\) for the residue of \(b\) in \(\kappa_B\), the trace over \(\kappa_A\) of multiplication by the class of \(b\) on \(Q_{n+1}\) equals \(\operatorname{Tr}_{\kappa_B/\kappa_A}(\bar b)\) plus the trace over \(\kappa_A\) of multiplication by the class of \(b\) on \(Q_n\).

trace_residueFieldMaximalIdealPowQuotient_succ · 20 lines 
theorem trace_residueFieldMaximalIdealPowQuotient_succ
    (n : ℕ)
    (hSucc : Ideal.map (algebraMap A B) (maximalIdeal A) ≤
      maximalIdeal B ^ (n + 1))
    [IsLocalHom (algebraMap A B)]
    [Module (ResidueField A)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)]
    [IsScalarTower (ResidueField A) (ResidueField B)
      (IsDiscreteValuationRing.MaximalIdealGradedPiece B n)]
    [FiniteDimensional (ResidueField A)
      (ResidueFieldMaximalIdealPowQuotient A B (n + 1))]
    (b : B) :
    Algebra.trace (ResidueField A)
        (ResidueFieldMaximalIdealPowQuotient A B (n + 1))
        (Ideal.Quotient.mk _ b) =
      Algebra.trace (ResidueField A) (ResidueField B)
        (IsLocalRing.residue B b) +
        Algebra.trace (ResidueField A)
          (ResidueFieldMaximalIdealPowQuotient A B n)
          (Ideal.Quotient.mk _ b)
Uses 9 · Used by 1
Statement usesGraded pieces of the maximal-ideal filtration · Quotient by the extended maximal ideal plus a maximal-ideal power
Proof usesMultiplication by a residue class on a graded piece · Multiplication by a residue class on representatives · Trace of multiplication on a graded piece · Trace splits along a surjective intertwining map · Transition map between maximal-ideal-power quotients · Surjectivity of the transition maps between maximal-ideal-power quotients · Graded pieces as kernels of the transition maps
Used byTrace on the maximal-ideal-power quotients

TheoremTrace on the maximal-ideal-power quotients#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra whose structure map is a local homomorphism. Write \(\mathfrak m_A B\) for the ideal of \(B\) generated by the image of \(\mathfrak m_A\). Let \(n\) be a natural number with \(\mathfrak m_A B \subseteq \mathfrak m_B^n\), and suppose the \(\kappa_A\)-algebra \(Q_n = B / (\mathfrak m_A B + \mathfrak m_B^n)\) is finite-dimensional over \(\kappa_A\). Then for every \(b \in B\), writing \(\bar b\) for the residue of \(b\) in \(\kappa_B\), the trace over \(\kappa_A\) of multiplication by the class of \(b\) on \(Q_n\) equals \(n \cdot \operatorname{Tr}_{\kappa_B/\kappa_A}(\bar b)\).

theorem trace_residueFieldMaximalIdealPowQuotient
    (n : ℕ)
    (h : Ideal.map (algebraMap A B) (maximalIdeal A) ≤ maximalIdeal B ^ n)
    [IsLocalHom (algebraMap A B)]
    [FiniteDimensional (ResidueField A)
      (ResidueFieldMaximalIdealPowQuotient A B n)]
    (b : B) :
    Algebra.trace (ResidueField A)
        (ResidueFieldMaximalIdealPowQuotient A B n)
        (Ideal.Quotient.mk _ b) =
      n • Algebra.trace (ResidueField A) (ResidueField B)
        (IsLocalRing.residue B b)
Uses 5 · Used by 1
Statement usesQuotient by the extended maximal ideal plus a maximal-ideal power
Proof usesGraded pieces of the maximal-ideal filtration · Transition map between maximal-ideal-power quotients · Surjectivity of the transition maps between maximal-ideal-power quotients · One-step trace recurrence for the maximal-ideal-power quotients
Used byResidue of the integral trace

TheoremResidue of the integral trace#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated and torsion-free as an \(A\)-module. Let \(e\) be a natural number such that the ideal \(\mathfrak m_A B\) generated by the image of \(\mathfrak m_A\) equals \(\mathfrak m_B^e\). Then for every \(b \in B\), writing \(\bar b\) for the residue of \(b\) in \(\kappa_B\), the residue in \(\kappa_A\) of the integral trace \(\operatorname{Tr}_{B/A}(b)\) (the trace of the extension of fraction fields, restricted to \(B\)) equals \(e \cdot \operatorname{Tr}_{\kappa_B/\kappa_A}(\bar b)\).

This determines the integral trace only modulo \(\mathfrak m_A\).

theorem residue_intTrace_eq_nsmul_trace_residue_of_map_maximalIdeal_eq_pow
    (e : ℕ)
    [Module.IsTorsionFree A B] [Module.Finite A B]
    (he : Ideal.map (algebraMap A B) (maximalIdeal A) =
      maximalIdeal B ^ e)
    (b : B) :
    residue A (Algebra.intTrace A B b) =
      e • Algebra.trace (ResidueField A)
        (ResidueField B) (residue B b)
Uses 2 · Used by 1
Proof usesQuotient by the extended maximal ideal plus a maximal-ideal power · Trace on the maximal-ideal-power quotients
Used byTame extensions have surjective integral trace

TheoremTame extensions have surjective integral trace#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak m_A\), \(\mathfrak m_B\) and residue fields \(\kappa_A\), \(\kappa_B\), and let \(B\) be an \(A\)-algebra that is finitely generated and torsion-free as an \(A\)-module, with \(\kappa_B / \kappa_A\) separable. Let \(e\) be a natural number that is a unit in \(B\) and such that the ideal \(\mathfrak m_A B\) generated by the image of \(\mathfrak m_A\) equals \(\mathfrak m_B^e\). Then the integral trace \(\operatorname{Tr}_{B/A} \colon B \to A\) (the trace of the extension of fraction fields, restricted to \(B\)) is surjective.

Since \(A \to B\) is local, \(e\) is a unit in \(B\) if and only if it is a unit in \(A\).

theorem intTrace_surjective_of_isUnit_natCast_of_map_maximalIdeal_eq_pow
    (e : ℕ)
    [Module.IsTorsionFree A B] [Module.Finite A B]
    [Algebra.IsSeparable (ResidueField A) (ResidueField B)]
    (heUnit : IsUnit (e : B))
    (he : Ideal.map (algebraMap A B) (maximalIdeal A) =
      maximalIdeal B ^ e) :
    Function.Surjective (Algebra.intTrace A B)
Uses 1 · Used by 1
Proof usesResidue of the integral trace
Used byDifferent ideal of a tamely ramified extension of DVRs

TheoremDifferent ideal of a tamely ramified extension of DVRs#✓fully proved

Let \(A\) and \(B\) be discrete valuation rings with maximal ideals \(\mathfrak{m}_A\) and \(\mathfrak{m}_B\), and let \(B\) be an \(A\)-algebra that is finite and torsion-free as an \(A\)-module, such that the extension of fraction fields and the extension of residue fields are both separable. Let \(e\) be a natural number whose image in \(B\) is a unit, and suppose that the ideal of \(B\) generated by the image of \(\mathfrak{m}_A\) equals \(\mathfrak{m}_B^e\). Then the different ideal of \(B\) over \(A\) equals \(\mathfrak{m}_B^{e-1}\).

Without the tameness hypothesis that \(e\) is a unit in \(B\), this equality fails in general.

theorem differentIdeal_eq_maximalIdeal_pow_sub_one_of_isUnit_natCast
    (e : ℕ) (heUnit : IsUnit (e : B))
    (he : Ideal.map (algebraMap A B) (maximalIdeal A) =
      maximalIdeal B ^ e) :
    differentIdeal A B = maximalIdeal B ^ (e - 1)
Uses 1
Proof usesTame extensions have surjective integral trace
22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.