AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.IsLocalRing_length_quotient_map_maximalIdeal_eq_finsum_ramificationIdx_mul_inertiaDeg.NormLength.core
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsLocalRing_length_quotient_map_maximalIdeal_eq_finsum_ramificationIdx_mul_inertiaDeg
open IsLocalRing IsDedekindDomain
namespace NormLength
Lean source · full declarationtheorem core
{C : Type*} [CommRing C] [IsDomain C] [IsDiscreteValuationRing C]
(K : Type*) [Field K] [Algebra C K] [IsFractionRing C K]
{D : Type*} [CommRing D] [IsDomain D] [IsLocalRing D] [IsNoetherianRing D] [Algebra C D]
(_hDmax : ∀ c : C, algebraMap C D c ∈ maximalIdeal D ↔ c ∈ maximalIdeal C)
(hDres : ∀ d : D, ∃ c : C, d - algebraMap C D c ∈ maximalIdeal D)
(hDdim : Ring.DimensionLEOne D) (_hDnf : maximalIdeal D ≠ ⊥)
(κ : Type*) [Field κ] [Algebra D κ] [IsFractionRing D κ] [Algebra C κ] [IsScalarTower C D κ]
[Algebra K κ] [IsScalarTower C K κ] [FiniteDimensional K κ] [Algebra.IsSeparable K κ]
(D₁ : Type*) [CommRing D₁] [IsDedekindDomain D₁] [Algebra D D₁] [Module.Finite D D₁]
[Algebra C D₁] [IsScalarTower C D D₁] [Algebra D₁ κ] [IsFractionRing D₁ κ]
[IsScalarTower D D₁ κ] [IsScalarTower C D₁ κ] :
{B : ValuationSubring κ | ∀ d : D, algebraMap D κ d ∈ B}.Finite ∧
Module.length D (D ⧸ (maximalIdeal C).map (algebraMap C D)) =
∑ᶠ B : {B : ValuationSubring κ // (∀ c : C, algebraMap C κ c ∈ B) ∧ (∀ d : D, algebraMap D κ
d ∈ B) ∧
∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal C},
((letI : Algebra C ↥B.1 := ((algebraMap C κ).codRestrict B.1 B.2.1).toAlgebra
(maximalIdeal C).ramificationIdx' (maximalIdeal ↥B.1) * (maximalIdeal ↥B.1).inertiaDeg C
: ℕ) : ℕ∞) := by
classical
have := hDdim
have hCκ : Function.Injective (algebraMap C κ) := by
rw [IsScalarTower.algebraMap_eq C K κ]
exact (algebraMap K κ).injective.comp (IsFractionRing.injective C K)
have hCD : Function.Injective (algebraMap C D) := fun a b h => hCκ (by
rw [IsScalarTower.algebraMap_apply C D κ, IsScalarTower.algebraMap_apply C D κ b, h])
obtain ⟨ϖ, hϖ⟩ := IsDiscreteValuationRing.exists_irreducible C
have hmC : maximalIdeal C = Ideal.span {ϖ} := hϖ.maximalIdeal_eq
have hϖm : ϖ ∈ maximalIdeal C := hmC ▸ Ideal.mem_span_singleton_self ϖ
set ϖD : D := algebraMap C D ϖ with hϖD
have hϖD0 : ϖD ≠ 0 := (map_ne_zero_iff _ hCD).mpr hϖ.ne_zero
have hmCD : (maximalIdeal C).map (algebraMap C D) = Ideal.span {ϖD} := by
rw [hmC, Ideal.map_span, Set.image_singleton]
have hsurj : Function.Surjective ((residue D).comp (algebraMap C D)) := by
intro x
obtain ⟨d, rfl⟩ := IsLocalRing.residue_surjective x
obtain ⟨c, hc⟩ := hDres d
refine ⟨c, ?_⟩
rw [RingHom.comp_apply]
exact ((Ideal.Quotient.eq (I := maximalIdeal D)).mpr hc).symm
have : Algebra.IsIntegral D D₁ := Algebra.IsIntegral.of_finite D D₁
have hDD₁ : Function.Injective (algebraMap D D₁) := fun a b h => by
have := congrArg (algebraMap D₁ κ) h
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply] at this
exact IsFractionRing.injective D κ this
have hCD₁ : Function.Injective (algebraMap C D₁) := by
rw [IsScalarTower.algebraMap_eq C D D₁]; exact hDD₁.comp hCD
have hmCD₁ : (maximalIdeal C).map (algebraMap C D₁) = (Ideal.span {ϖD}).map (algebraMap D D₁) :=
by
rw [IsScalarTower.algebraMap_eq C D D₁, ← Ideal.map_map, hmCD]
set N : Submodule D D₁ := LinearMap.range (Algebra.linearMap D D₁) with hN
have hNfin : Module.length D (D₁ ⧸ N) ≠ ⊤ := by
obtain ⟨s, hs⟩ := Module.Finite.fg_top (R := D) (M := D₁)
obtain ⟨b, hb⟩ := IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors D)
(s.image (fun x : D₁ => algebraMap D₁ κ x))
have hbN : ∀ x : D₁, (b : D) • x ∈ N := by
intro x
have hx : x ∈ Submodule.span D (s : Set D₁) := by rw [hs]; exact Submodule.mem_top
refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
· intro y hy
obtain ⟨a, ha⟩ := hb (algebraMap D₁ κ y) (Finset.mem_image_of_mem _ hy)
refine ⟨a, ?_⟩
apply IsFractionRing.injective D₁ κ
change algebraMap D₁ κ (algebraMap D D₁ a) = algebraMap D₁ κ ((b : D) • y)
rw [← IsScalarTower.algebraMap_apply, ha, Algebra.smul_def, Algebra.smul_def, map_mul,
← IsScalarTower.algebraMap_apply]
· rw [smul_zero]; exact N.zero_mem
· intro y z _ _ hy hz; rw [smul_add]; exact N.add_mem hy hz
· intro a y _ hy; rw [smul_comm]; exact N.smul_mem a hy
refine length_ne_top_of_smul_eq_zero hDdim (b : D) (nonZeroDivisors.ne_zero b.2) fun q => ?_
obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective N q
rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
exact hbN x
have hreg : ∀ m : D₁, ϖD • m = 0 → m = 0 := fun m hm => by
rw [Algebra.smul_def, mul_eq_zero] at hm
exact hm.resolve_left ((map_ne_zero_iff _ hDD₁).mpr hϖD0)
have hlat := length_quotient_span_singleton_smul_top_eq ϖD hreg N hNfin
have eN : ↥N ≃ₗ[D] D := (LinearEquiv.ofInjective (Algebra.linearMap D D₁) hDD₁).symm
have hleft : Module.length D (↥N ⧸ ((Ideal.span {ϖD} : Ideal D) • (⊤ : Submodule D ↥N))) =
Module.length D (D ⧸ (maximalIdeal C).map (algebraMap C D)) := by
refine (Submodule.Quotient.equiv ((Ideal.span {ϖD} : Ideal D) • (⊤ : Submodule D ↥N))
((Ideal.span {ϖD} : Ideal D) • (⊤ : Submodule D D)) eN (by
rw [Submodule.map_smul'', Submodule.map_top, LinearEquiv.range])).length_eq.trans ?_
· rw [hmCD, Submodule.ideal_span_singleton_smul]
refine (Submodule.quotEquivOfEq _ _ ?_).length_eq
ext d
rw [Submodule.mem_smul_pointwise_iff_exists, Ideal.mem_span_singleton']
exact ⟨fun ⟨e, _, h⟩ => ⟨e,
by rw [← h, smul_eq_mul, mul_comm]⟩, fun ⟨e, h⟩ => ⟨e, Submodule.mem_top, by
rw [← h, smul_eq_mul, mul_comm]⟩⟩
have hright : Module.length D (D₁ ⧸ ((Ideal.span {ϖD} : Ideal D) • (⊤ : Submodule D D₁))) =
Module.length D (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) := by
rw [Ideal.smul_top_eq_map, ← hmCD₁]
exact (Submodule.Quotient.restrictScalarsEquiv D ((maximalIdeal C).map (algebraMap C
D₁))).length_eq
have hM0 : ∀ q : D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁), ϖD • q = 0 := by
intro q
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective q
change ϖD • Submodule.Quotient.mk x = 0
rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.mk_eq_zero, Algebra.smul_def]
refine Ideal.mul_mem_right _ _ ?_
rw [hϖD, ← IsScalarTower.algebraMap_apply C D D₁]
exact Ideal.mem_map_of_mem _ hϖm
have hMfin : Module.Finite D (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
Module.Finite.of_surjective (Ideal.Quotient.mkₐ D ((maximalIdeal C).map (algebraMap C
D₁))).toLinearMap
Ideal.Quotient.mk_surjective
have hlenM : Module.length D (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) ≠ ⊤ :=
length_ne_top_of_smul_eq_zero hDdim ϖD hϖD0 hM0
have h1 : Module.length C (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) =
Module.length D (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
Module.length_restrictScalars_eq_of_surjective_residue hsurj (Module.length_ne_top_iff.mp hlenM)
have h2 : Module.length C (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) =
Module.length (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
Module.length_eq_of_surjective (R := C ⧸ maximalIdeal C) (S := C) Ideal.Quotient.mk_surjective
have := IsLocalRing.maximalIdeal.isMaximal C
let : Field (C ⧸ maximalIdeal C) := Ideal.Quotient.field _
have hflk : IsFiniteLength (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
by
rw [← Module.length_ne_top_iff, ← h2, h1]; exact hlenM
have : IsNoetherian (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
(isFiniteLength_iff_isNoetherian_isArtinian.mp hflk).1
have : Module.Finite (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
inferInstance
have h3 : Module.length (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) =
Module.finrank (C ⧸ maximalIdeal C) (D₁ ⧸ (maximalIdeal C).map (algebraMap C D₁)) :=
Module.length_eq_finrank _ _
obtain ⟨hIfin, hsum⟩ := finrank_quotient_map_maximalIdeal_eq_finsum (C := C) K (D₁ := D₁) κ hCD₁
have hDκ : ∀ d : D, algebraMap D κ d = algebraMap D₁ κ (algebraMap D D₁ d) := fun d =>
IsScalarTower.algebraMap_apply D D₁ κ d
have hD₁B : ∀ B : ValuationSubring κ, (∀ d : D, algebraMap D κ d ∈ B) → ∀ x : D₁, algebraMap D₁ κ
x ∈ B := by
intro B hB x
let : Algebra D ↥B := ((algebraMap D κ).codRestrict B hB).toAlgebra
have : IsScalarTower D ↥B κ := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
have hx : IsIntegral D (algebraMap D₁ κ x) :=
(Algebra.IsIntegral.isIntegral (R := D) x).map (IsScalarTower.toAlgHom D D₁ κ)
have hx' : IsIntegral ↥B (algebraMap D₁ κ x) := hx.tower_top
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff κ).mp inferInstance hx'
rw [← hz]; exact z.2
let e : {B : ValuationSubring κ // (∀ c : C, algebraMap C κ c ∈ B) ∧ (∀ x : D₁, algebraMap D₁ κ x
∈ B) ∧
∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal C} ≃
{B : ValuationSubring κ // (∀ c : C, algebraMap C κ c ∈ B) ∧ (∀ d : D, algebraMap D κ d ∈ B) ∧
∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal C} :=
{ toFun := fun B => ⟨B.1, B.2.1, fun d => by rw [hDκ]; exact B.2.2.1 _, B.2.2.2⟩
invFun := fun B => ⟨B.1, B.2.1, hD₁B B.1 B.2.2.1, B.2.2.2⟩
left_inv := fun B => rfl
right_inv := fun B => rfl }
have := hIfin
have : Finite {B : ValuationSubring κ // (∀ c : C, algebraMap C κ c ∈ B) ∧ (∀ d : D, algebraMap D
κ d ∈ B) ∧
∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal C} := Finite.of_equiv _ e
have : Algebra.IsIntegral K κ := Algebra.IsIntegral.of_finite K κ
have hcentred : ∀ B : ValuationSubring κ, (∀ d : D, algebraMap D κ d ∈ B) → B ≠ ⊤ →
∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal C := by
intro B hB hBtop
have hCB : ∀ c : C, algebraMap C κ c ∈ B := fun c => by
rw [IsScalarTower.algebraMap_apply C D κ]; exact hB _
have hϖκ0 : algebraMap C κ ϖ ≠ 0 := (map_ne_zero_iff _ hCκ).mpr hϖ.ne_zero
have hϖB : algebraMap C κ ϖ ∈ B.nonunits := by
rw [ValuationSubring.mem_nonunits_iff_or]
refine Or.inr fun hinv => hBtop ?_
have hKB : ∀ k : K, algebraMap K κ k ∈ B := by
intro k
obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := C) k
have hb0 : b ≠ 0 := nonZeroDivisors.ne_zero hb
obtain ⟨n, hn⟩ := IsDiscreteValuationRing.associated_pow_irreducible hb0 hϖ
obtain ⟨u, hu⟩ := hn
have hbinv : (algebraMap C κ b)⁻¹ = algebraMap C κ u * ((algebraMap C κ ϖ)⁻¹) ^ n := by
refine inv_eq_of_mul_eq_one_right ?_
rw [← mul_assoc, ← map_mul, hu, map_pow, inv_pow, mul_inv_cancel₀ (pow_ne_zero n hϖκ0)]
rw [map_div₀, ← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
div_eq_mul_inv, hbinv]
exact B.mul_mem _ _ (hCB a) (B.mul_mem _ _ (hCB u) (pow_mem hinv n))
let : Algebra K ↥B := ((algebraMap K κ).codRestrict B hKB).toAlgebra
have : IsScalarTower K ↥B κ := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
refine eq_top_iff.mpr fun x _ => ?_
have hx' : IsIntegral ↥B x := (Algebra.IsIntegral.isIntegral (R := K) x).tower_top
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff κ).mp inferInstance hx'
rw [← hz]; exact z.2
intro c
constructor
· intro hc
by_contra hcm
have hu : IsUnit c := by
by_contra h; exact hcm ((IsLocalRing.mem_maximalIdeal c).mpr h)
obtain ⟨u, rfl⟩ := hu
rw [ValuationSubring.mem_nonunits_iff_or] at hc
rcases hc with h | h
· exact ((map_ne_zero_iff _ hCκ).mpr u.ne_zero) h
· apply h
have hui : (algebraMap C κ ↑u)⁻¹ = algebraMap C κ ↑u⁻¹ :=
inv_eq_of_mul_eq_one_right (by rw [← map_mul, Units.mul_inv, map_one])
rw [hui]
exact hCB _
· intro hc
rw [hmC, Ideal.mem_span_singleton'] at hc
obtain ⟨c', rfl⟩ := hc
rw [map_mul, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal]
refine ⟨B.mul_mem _ _ (hCB c') (hCB ϖ), ?_⟩
have : (⟨algebraMap C κ c' * algebraMap C κ ϖ, B.mul_mem _ _ (hCB c') (hCB ϖ)⟩ : ↥B) =
⟨algebraMap C κ c', hCB c'⟩ * ⟨algebraMap C κ ϖ, hCB ϖ⟩ := rfl
rw [this]
exact Ideal.mul_mem_left _ _ (ValuationSubring.coe_mem_nonunits_iff.mp hϖB)
have hfinite : {B : ValuationSubring κ | ∀ d : D, algebraMap D κ d ∈ B}.Finite := by
refine ((Set.finite_range (fun B : {B : ValuationSubring κ // (∀ c : C, algebraMap C κ c ∈ B) ∧
(∀ d : D, algebraMap D κ d ∈ B) ∧ ∀ c : C, algebraMap C κ c ∈ B.nonunits ↔ c ∈ maximalIdeal
C} => B.1)).insert
⊤).subset ?_
intro B hB
by_cases hBtop : B = ⊤
· exact Or.inl hBtop
· refine Or.inr ⟨⟨B, fun c => ?_, hB, hcentred B hB hBtop⟩, rfl⟩
rw [IsScalarTower.algebraMap_apply C D κ]; exact hB _
refine ⟨hfinite, ?_⟩
rw [← hleft, hlat, hright, ← h1, h2, h3, hsum]
exact finsum_eq_of_bijective e e.bijective (fun B => rfl)