Ideal.lean

theorem quotient_unitGroup_isCyclic_of_isDiscreteValuationRing
    {L : Type*} [Field L] (V : _root_.ValuationSubring L)
    [IsDiscreteValuationRing V] :
    IsCyclic (Lˣ ⧸ V.unitGroup)

theorem relativeValueClass_isCyclic_of_isDiscreteValuationRing
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V] :
    IsCyclic
      ((Lˣ ⧸ V.unitGroup) ⧸ baseUnitValueClassSubgroup K V)

theorem automorphismUnitQuotient_mk_mem_unitGroup_of_dvr
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (sigma : decompositionGroup K V) (a : V) (ha : a ≠ 0) :
    automorphismUnitQuotient K V sigma
        (Units.mk0 (a : L) (by
          change algebraMap V L a ≠ 0
          exact (map_ne_zero_iff (algebraMap V L)
            (IsFractionRing.injective V L)).2 ha)) ∈
      V.unitGroup := by
  let eV : V ≃+* V :=
    MulSemiringAction.toRingEquiv (decompositionGroup K V) V sigma
  have haL : (a : L) ≠ 0 := by
    change algebraMap V L a ≠ 0
    exact (map_ne_zero_iff (algebraMap V L)
      (IsFractionRing.injective V L)).2 ha
  obtain ⟨pi, hpi⟩ := IsDiscreteValuationRing.exists_irreducible V
  obtain ⟨n, han⟩ :=
    IsDiscreteValuationRing.associated_pow_irreducible ha hpi
  obtain ⟨ua, hua⟩ := han
  have hepi : Irreducible (eV pi) := hpi.map eV.toMulEquiv
  have hepiAssoc : Associated (eV pi) pi :=
    IsDiscreteValuationRing.associated_of_irreducible V hepi hpi
  have heaPow : Associated (eV a) ((eV pi) ^ n) := by
    refine ⟨Units.map eV.toMonoidHom ua, ?_⟩
    simpa using congrArg eV hua
  have hea : Associated (eV a) a :=
    (heaPow.trans hepiAssoc.pow_pow).trans
      (Associated.symm ⟨ua, hua⟩)
  obtain ⟨u, hu⟩ := hea
  let aL : Lˣ := Units.mk0 (a : L) haL
  let uL : Lˣ := Units.map V.subtype.toMonoidHom u
  have huL : ((sigma : L ≃ₐ[K] L) (a : L)) * (u : V) = (a : L) := by
    have hu' := congrArg (fun z : V => (z : L)) hu
    change ((sigma : L ≃ₐ[K] L) • (a : L)) * (u : V) = (a : L) at hu'
    simpa only [AlgEquiv.smul_def] using hu'
  have hquotVal : ((sigma : L ≃ₐ[K] L) (a : L)) / (a : L) =
      ((u : V) : L)⁻¹ := by
    apply (mul_right_cancel₀ haL)
    rw [div_mul_cancel₀ _ haL]
    symm
    calc
      ((u : V) : L)⁻¹ * (a : L) =
          ((u : V) : L)⁻¹ *
            (((sigma : L ≃ₐ[K] L) (a : L)) * (u : V)) := by rw [huL]
      _ = (sigma : L ≃ₐ[K] L) (a : L) := by
        field_simp
  have hquot : automorphismUnitQuotient K V sigma aL = uL⁻¹ := by
    apply Units.ext
    simpa [automorphismUnitQuotient, aL, uL] using hquotVal
  rw [hquot]
  exact V.unitGroup.inv_mem
    (show uL ∈ V.unitGroup from
      (V.unitGroupMulEquiv.symm u).property)

theorem automorphismUnitQuotient_mem_unitGroup_of_dvr
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (sigma : decompositionGroup K V) (x : Lˣ) :
    automorphismUnitQuotient K V sigma x ∈ V.unitGroup

theorem valueTrivialInertiaGroup_eq_top_of_isDiscreteValuationRing
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V] :
    valueTrivialInertiaGroup K V = ⊤

theorem inertia_mem_valueTrivialInertiaGroup_of_dvr
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    (sigma : inertiaGroup K V) :
    sigma ∈ valueTrivialInertiaGroup K V

theorem inertiaGroup_isCyclic_of_card_coprime_ringExpChar_of_dvr
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (V : _root_.ValuationSubring L) [IsDiscreteValuationRing V]
    [Finite (inertiaGroup K V)]
    (hcop : Nat.Coprime (Nat.card (inertiaGroup K V))
      (ringExpChar (IsLocalRing.ResidueField V))) :
    IsCyclic (inertiaGroup K V)