IdealLocalization.lean

abbrev idealLocalizationSubalgebra (P : Ideal B) [P.IsPrime] :
    Subalgebra B L

theorem idealLocalizationSubalgebra_dvr
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    IsDiscreteValuationRing (idealLocalizationSubalgebra B L P)

def idealLocalizationValuationSubring
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    _root_.ValuationSubring L

theorem mem_idealLocalizationValuationSubring_iff
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) (x : L) :
    x ∈ idealLocalizationValuationSubring B L P hP ↔
      x ∈ idealLocalizationSubalgebra B L P

def idealLocalizationEquiv
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    idealLocalizationSubalgebra B L P ≃+*
      idealLocalizationValuationSubring B L P hP where
  toFun x := ⟨x, x.property⟩
  invFun x := ⟨x, x.property⟩
  left_inv _ := rfl
  right_inv _ := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

theorem idealLocalizationEquiv_apply_coe
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥)
    (x : idealLocalizationSubalgebra B L P) :
    ((idealLocalizationEquiv B L P hP x :
      idealLocalizationValuationSubring B L P hP) : L) = x

instance idealLocalizationValuationSubring_dvr
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥) :
    IsDiscreteValuationRing
      (idealLocalizationValuationSubring B L P hP)

theorem idealLocalizationEquiv_mem_maximalIdeal_iff
    (P : Ideal B) [P.IsPrime] (hP : P ≠ ⊥)
    (x : idealLocalizationSubalgebra B L P) :
    letI := idealLocalizationSubalgebra_dvr B L P hP
    idealLocalizationEquiv B L P hP x ∈
        IsLocalRing.maximalIdeal
          (idealLocalizationValuationSubring B L P hP) ↔
      x ∈ IsLocalRing.maximalIdeal
        (idealLocalizationSubalgebra B L P) := by
  let : IsDiscreteValuationRing (idealLocalizationSubalgebra B L P) :=
    idealLocalizationSubalgebra_dvr B L P hP
  rw [IsLocalRing.mem_maximalIdeal, IsLocalRing.mem_maximalIdeal]
  exact not_congr
    (MulEquiv.isUnit_map
      (idealLocalizationEquiv B L P hP).toMulEquiv)

def idealLocalizationResidueEquiv
    (P : Ideal B) [P.IsMaximal] (hP : P ≠ ⊥) :
    B ⧸ P ≃+*
      IsLocalRing.ResidueField
        (idealLocalizationValuationSubring B L P hP)

theorem ringExpChar_idealLocalizationResidueField_eq
    (P : Ideal B) [P.IsMaximal] (hP : P ≠ ⊥) :
    ringExpChar
        (IsLocalRing.ResidueField
          (idealLocalizationValuationSubring B L P hP)) =
      ringExpChar (B ⧸ P)

theorem algebraMap_normalization_smul
    (sigma : Gal(L/K)) (b : B) :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    algebraMap B L (sigma • b) = sigma (algebraMap B L b) := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  change algebraMap B L (galRestrict A K L B sigma b) =
    sigma (algebraMap B L b)
  exact algebraMap_galRestrict_apply A sigma b

theorem globalInertia_maps_localization :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    ∀ (sigma : P.toAddSubgroup.inertia Gal(L/K)) {x : L},
      x ∈ idealLocalizationValuationSubring B L P hP →
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
        idealLocalizationValuationSubring B L P hP := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma x hx
  change x ∈ idealLocalizationSubalgebra B L P at hx
  change ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
    idealLocalizationSubalgebra B L P
  rcases hx with ⟨a, s, hs, rfl⟩
  have hdelta : (sigma : Gal(L/K)) • s - s ∈ P := sigma.property s
  have hsigma : (sigma : Gal(L/K)) • s ∈ P.primeCompl := by
    intro hsigmaP
    have hsP : s ∈ P := by
      simpa only [sub_sub_cancel] using P.sub_mem hsigmaP hdelta
    exact hs hsP
  refine ⟨(sigma : Gal(L/K)) • a, (sigma : Gal(L/K)) • s,
    hsigma, ?_⟩
  simp only [map_mul, map_inv₀,
    algebraMap_normalization_smul (A := A)]

theorem globalInertia_maps_localization_iff :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    ∀ (sigma : P.toAddSubgroup.inertia Gal(L/K)) (x : L),
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L) x ∈
          idealLocalizationValuationSubring B L P hP ↔
        x ∈ idealLocalizationValuationSubring B L P hP := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma x
  constructor
  · intro hx
    have hinv := globalInertia_maps_localization
      (A := A) (P := P) (hP := hP) sigma⁻¹ hx
    simpa using hinv
  · exact globalInertia_maps_localization
      (A := A) (P := P) (hP := hP) sigma

def globalIdealInertiaToDecomposition :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    P.toAddSubgroup.inertia Gal(L/K) →
      decompositionGroup K (idealLocalizationValuationSubring B L P hP) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma
  refine ⟨(sigma : Gal(L/K)), ?_⟩
  apply _root_.ValuationSubring.toSubring_injective
  ext x
  change x ∈ (sigma : Gal(L/K)) •
      idealLocalizationValuationSubring B L P hP ↔
    x ∈ idealLocalizationValuationSubring B L P hP
  rw [_root_.ValuationSubring.mem_pointwise_smul_iff_inv_smul_mem]
  exact globalInertia_maps_localization_iff
    (A := A) (P := P) (hP := hP) sigma⁻¹ x

theorem globalIdealInertiaToDecomposition_mem_localIdealInertia :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    ∀ sigma : P.toAddSubgroup.inertia Gal(L/K),
      globalIdealInertiaToDecomposition
          (A := A) (P := P) (hP := hP) sigma ∈
        (IsLocalRing.maximalIdeal
          (idealLocalizationValuationSubring B L P hP)).toAddSubgroup.inertia
            (decompositionGroup K
              (idealLocalizationValuationSubring B L P hP)) := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  intro sigma x
  let S := idealLocalizationSubalgebra B L P
  let V := idealLocalizationValuationSubring B L P hP
  let : IsDiscreteValuationRing S :=
    idealLocalizationSubalgebra_dvr B L P hP
  let e : S ≃+* V := idealLocalizationEquiv B L P hP
  let delta : decompositionGroup K V :=
    globalIdealInertiaToDecomposition
      (A := A) (P := P) (hP := hP) sigma
  rcases x.property with ⟨a, s, hs, hx⟩
  have hs0 : s ≠ 0 := by
    intro hszero
    apply hs
    simp [hszero]
  have hdeltaA : (sigma : Gal(L/K)) • a - a ∈ P := sigma.property a
  have hdeltaS : (sigma : Gal(L/K)) • s - s ∈ P := sigma.property s
  have hsigma : (sigma : Gal(L/K)) • s ∈ P.primeCompl := by
    intro hsigmaP
    have hsP : s ∈ P := by
      simpa only [sub_sub_cancel] using P.sub_mem hsigmaP hdeltaS
    exact hs hsP
  have hsL0 : algebraMap B L s ≠ 0 := by
    simpa only [map_zero] using (IsFractionRing.injective B L).ne hs0
  have hsigmaMapL0 :
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L) (algebraMap B L s) ≠ 0 :=
    by simpa only [map_zero] using
      ((sigma : Gal(L/K)) : L ≃ₐ[K] L).injective.ne hsL0
  let ys : S := ⟨x, x.property⟩
  let sigmays : S := e.symm (delta • x)
  have hys : ys = IsLocalization.mk' S a ⟨s, hs⟩ := by
    rw [IsLocalization.eq_mk'_iff_mul_eq]
    apply Subtype.ext
    change (x : L) * algebraMap B L s = algebraMap B L a
    rw [hx]
    simp [hs0]
  have hsigmays : sigmays =
      IsLocalization.mk' S ((sigma : Gal(L/K)) • a)
        ⟨(sigma : Gal(L/K)) • s, hsigma⟩ := by
    rw [IsLocalization.eq_mk'_iff_mul_eq]
    apply Subtype.ext
    change ((sigma : Gal(L/K)) : L ≃ₐ[K] L) (x : L) *
        algebraMap B L ((sigma : Gal(L/K)) • s) =
      algebraMap B L ((sigma : Gal(L/K)) • a)
    rw [algebraMap_normalization_smul (A := A),
      algebraMap_normalization_smul (A := A), hx, map_mul, map_inv₀]
    rw [mul_assoc, inv_mul_cancel₀ hsigmaMapL0, mul_one]
  have hnum :
      (sigma : Gal(L/K)) • a * s -
          a * ((sigma : Gal(L/K)) • s) ∈ P := by
    have h := P.sub_mem
      (P.mul_mem_right s hdeltaA)
      (P.mul_mem_left a hdeltaS)
    convert h using 1
    all_goals ring
  let den : P.primeCompl :=
    ⟨((sigma : Gal(L/K)) • s) * s,
      P.primeCompl.mul_mem hsigma hs⟩
  have hfrac : IsLocalization.mk' S
        ((sigma : Gal(L/K)) • a * s -
          a * ((sigma : Gal(L/K)) • s)) den ∈
      IsLocalRing.maximalIdeal S :=
    (IsLocalization.AtPrime.mk'_mem_maximal_iff S P _ den).mpr hnum
  have hsub : sigmays - ys ∈ IsLocalRing.maximalIdeal S := by
    rw [hsigmays, hys]
    rw [← IsLocalization.mk'_sub]
    exact hfrac
  have hlocal : e (sigmays - ys) ∈ IsLocalRing.maximalIdeal V :=
    (idealLocalizationEquiv_mem_maximalIdeal_iff B L P hP
      (sigmays - ys)).mpr hsub
  rw [map_sub] at hlocal
  have hesigma : e sigmays = delta • x := by
    exact e.apply_symm_apply (delta • x)
  have heys : e ys = x := by
    apply Subtype.ext
    rfl
  rwa [hesigma, heys] at hlocal

def globalIdealInertiaToLocalInertia :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    P.toAddSubgroup.inertia Gal(L/K) →*
      inertiaGroup K (idealLocalizationValuationSubring B L P hP) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  refine
    { toFun := fun sigma ↦
        ⟨globalIdealInertiaToDecomposition
            (A := A) (P := P) (hP := hP) sigma, ?_⟩
      map_one' := ?_
      map_mul' := ?_ }
  · rw [← TameInertiaCyclicCore.valuationSubring_maximalIdeal_inertia_eq]
    exact globalIdealInertiaToDecomposition_mem_localIdealInertia
      (A := A) (P := P) (hP := hP) sigma
  · rfl
  · intro sigma tau
    rfl

def localInertiaToGlobalIdealInertia :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    inertiaGroup K (idealLocalizationValuationSubring B L P hP) →*
      P.toAddSubgroup.inertia Gal(L/K) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  let S := idealLocalizationSubalgebra B L P
  let V := idealLocalizationValuationSubring B L P hP
  letI : IsDiscreteValuationRing S :=
    idealLocalizationSubalgebra_dvr B L P hP
  let e : S ≃+* V := idealLocalizationEquiv B L P hP
  refine
    { toFun := fun tau ↦ ⟨((tau : decompositionGroup K V) : Gal(L/K)), ?_⟩
      map_one' := ?_
      map_mul' := ?_ }
  · intro b
    let vb : V :=
      ⟨algebraMap B L b, by
        change algebraMap B L b ∈ idealLocalizationSubalgebra B L P
        exact ⟨b, 1, P.primeCompl.one_mem, by simp⟩⟩
    have htauIdeal : (tau : decompositionGroup K V) ∈
        (IsLocalRing.maximalIdeal V).toAddSubgroup.inertia
          (decompositionGroup K V) := by
      rw [TameInertiaCyclicCore.valuationSubring_maximalIdeal_inertia_eq]
      exact tau.property
    have hlocal : (tau : decompositionGroup K V) • vb - vb ∈
        IsLocalRing.maximalIdeal V :=
      htauIdeal vb
    let zS : S := e.symm ((tau : decompositionGroup K V) • vb - vb)
    have hzS : zS ∈ IsLocalRing.maximalIdeal S := by
      apply (idealLocalizationEquiv_mem_maximalIdeal_iff B L P hP zS).mp
      simpa [e, zS] using hlocal
    have hzEq : zS = algebraMap B S
        (((tau : decompositionGroup K V) : Gal(L/K)) • b - b) := by
      apply Subtype.ext
      change
        (((tau : decompositionGroup K V) : Gal(L/K)) : L ≃ₐ[K] L)
              (algebraMap B L b) - algebraMap B L b =
          algebraMap B L
            (((tau : decompositionGroup K V) : Gal(L/K)) • b - b)
      rw [map_sub, algebraMap_normalization_smul (A := A)]
    apply (IsLocalization.AtPrime.to_map_mem_maximal_iff S P _).mp
    rw [← hzEq]
    exact hzS
  · rfl
  · intro sigma tau
    rfl

def idealInertiaLocalizationMulEquiv :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    P.toAddSubgroup.inertia Gal(L/K) ≃*
      inertiaGroup K (idealLocalizationValuationSubring B L P hP) := by
  letI := IsIntegralClosure.MulSemiringAction A K L B
  refine
    { toFun := globalIdealInertiaToLocalInertia
        (A := A) (P := P) (hP := hP)
      invFun := localInertiaToGlobalIdealInertia
        (A := A) (P := P) (hP := hP)
      left_inv := ?_
      right_inv := ?_
      map_mul' := ?_ }
  · intro sigma
    apply Subtype.ext
    rfl
  · intro tau
    apply Subtype.ext
    apply Subtype.ext
    rfl
  · intro sigma tau
    rfl

theorem natCard_idealInertia_eq_localInertia :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    Nat.card (P.toAddSubgroup.inertia Gal(L/K)) =
      Nat.card
        (inertiaGroup K
          (idealLocalizationValuationSubring B L P hP)) := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  exact Nat.card_congr
    (idealInertiaLocalizationMulEquiv
      (A := A) (P := P) (hP := hP)).toEquiv

theorem idealInertia_isCyclic_of_card_coprime_ringExpChar
    [FiniteDimensional K L] [IsGalois K L]
    (hP0 : P ≠ ⊥)
    (hcop :
      letI := IsIntegralClosure.MulSemiringAction A K L B
      Nat.Coprime
        (Nat.card (P.toAddSubgroup.inertia Gal(L/K)))
        (ringExpChar (B ⧸ P))) :
    letI := IsIntegralClosure.MulSemiringAction A K L B
    IsCyclic (P.toAddSubgroup.inertia Gal(L/K)) := by
  let := IsIntegralClosure.MulSemiringAction A K L B
  let V := idealLocalizationValuationSubring B L P hP0
  let : Finite (L ≃ₐ[K] L) := inferInstance
  let : Finite (inertiaGroup K V) := inferInstance
  have hcard :
      Nat.card (P.toAddSubgroup.inertia Gal(L/K)) =
        Nat.card (inertiaGroup K V) :=
    natCard_idealInertia_eq_localInertia
      (A := A) (P := P) (hP := hP0)
  have hchar :
      ringExpChar (IsLocalRing.ResidueField V) =
        ringExpChar (B ⧸ P) :=
    ringExpChar_idealLocalizationResidueField_eq B L P hP0
  have hcopLocal : Nat.Coprime
      (Nat.card (inertiaGroup K V))
      (ringExpChar (IsLocalRing.ResidueField V)) := by
    rw [← hcard, hchar]
    exact hcop
  have hlocal : IsCyclic (inertiaGroup K V) :=
    inertiaGroup_isCyclic_of_card_coprime_ringExpChar_of_dvr
      K V hcopLocal
  exact (idealInertiaLocalizationMulEquiv
    (A := A) (P := P) (hP := hP0)).isCyclic.mpr hlocal