HasseArf.lean

theorem lowerRamificationGroup_finite
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (A : ValuationSubring L) (n : ℕ) :
    Finite (lowerRamificationGroup K A n)

theorem lowerRamificationGroup_card_pos
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L]
    (A : ValuationSubring L) (n : ℕ) :
    0 < Nat.card (lowerRamificationGroup K A n)

theorem herbrandFunctionAtLowerIndex_succ
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
    (A : ValuationSubring L) (n : ℕ) :
    herbrandFunctionAtLowerIndex K A (n + 1) =
      herbrandFunctionAtLowerIndex K A n +
        (Nat.card (lowerRamificationGroup K A (n + 1)) : ℚ) /
          Nat.card (lowerRamificationGroup K A 0)

theorem
    localUpperRamificationGroupAfter_eq_artinPrincipalUnitStepGroupAfter_of_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (hfiltered : ∀ t, 0 ≤ t →
      artinPrincipalUnitStepGroup K L t =
        localUpperRamificationGroup K L t)
    (t : ℝ) (ht : 0 ≤ t) :
    localUpperRamificationGroupAfter K L t =
      natCeilStepFiltrationAfter (artinPrincipalUnitGroup K L) t

theorem
    isLocalUpperRamificationJump_iff_isArtinPrincipalUnitJump_of_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (hfiltered : ∀ t, 0 ≤ t →
      artinPrincipalUnitStepGroup K L t =
        localUpperRamificationGroup K L t)
    (t : ℝ) (ht : 0 ≤ t) :
    IsLocalUpperRamificationJump K L t ↔
      IsArtinPrincipalUnitJump K L t

theorem
    isLocalUpperRamificationJump_integer_of_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (hfiltered : ∀ t, 0 ≤ t →
      artinPrincipalUnitStepGroup K L t =
        localUpperRamificationGroup K L t)
    {t : ℝ} (ht0 : 0 ≤ t)
    (ht : IsLocalUpperRamificationJump K L t) :
    ∃ n : ℕ, t = n

theorem
    isLocalUpperRamificationJump_int_of_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (hfiltered : ∀ t, 0 ≤ t →
      artinPrincipalUnitStepGroup K L t =
        localUpperRamificationGroup K L t)
    {t : ℝ} (ht : IsLocalUpperRamificationJump K L t) :
    ∃ z : ℤ, t = z

theorem isLocalUpperRamificationJump_int
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    {t : ℝ} (ht : IsLocalUpperRamificationJump K L t) :
    ∃ z : ℤ, t = z

theorem chosenLocalExtension_decompositionSubgroup_eq_top
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring).decompositionSubgroup K =
      ⊤

theorem mem_chosenLowerRamificationGroup_iff_mem_localLowerRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) (σ : Gal(L/K))
    (hσ : σ ∈
      ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring).decompositionSubgroup K) :
    (⟨σ, hσ⟩ :
      ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring).decompositionSubgroup K) ∈
        ClassFieldTheory.lowerRamificationGroup K
          (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring n ↔
      σ ∈ localLowerRamificationGroup K L (n : ℝ)

theorem mem_chosenRealLowerRamificationGroup_iff_mem_localLowerRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (s : ℝ) (σ : Gal(L/K))
    (hσ : σ ∈
      ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring).decompositionSubgroup K) :
    (⟨σ, hσ⟩ :
      ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring).decompositionSubgroup K) ∈
        ClassFieldTheory.realLowerRamificationGroup K
          (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring s ↔
      σ ∈ localLowerRamificationGroup K L s

def chosenLowerRamificationGroupEquiv
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : ℕ) :
    ClassFieldTheory.lowerRamificationGroup K
        (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring n ≃
      localLowerRamificationGroup K L (n : ℝ)

theorem card_chosenLowerRamificationGroup_eq_card_localLowerRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : ℕ) :
    Nat.card (ClassFieldTheory.lowerRamificationGroup K
      (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring n) =
      Nat.card (localLowerRamificationGroup K L (n : ℝ))

theorem herbrandFunctionAtLowerIndex_succ
    (K L : Type) [Field K] [Field L] [Algebra K L]
    (A : ValuationSubring L) (n : ℕ) :
    ClassFieldTheory.herbrandFunctionAtLowerIndex K A (n + 1) =
    ClassFieldTheory.herbrandFunctionAtLowerIndex K A n +
        (Nat.card (ClassFieldTheory.lowerRamificationGroup K A (n + 1)) : ℚ) /
          Nat.card (ClassFieldTheory.lowerRamificationGroup K A 0)

theorem chosenHerbrandFunctionAtLowerIndex_real_eq
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : ℕ) :
    ((ClassFieldTheory.herbrandFunctionAtLowerIndex K
      (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring n : ℚ) : ℝ) =
      herbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L)
        (n : ℝ)

theorem chosenLocalExtension_valuationSubring_eq_canonical
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
    (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring =
      (ValuativeRel.valuation L).valuationSubring

theorem canonicalHerbrandFunctionAtLowerIndex_real_eq
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (n : ℕ) :
    ((ClassFieldTheory.herbrandFunctionAtLowerIndex K
      (ValuativeRel.valuation L).valuationSubring n : ℚ) : ℝ) =
      herbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L)
        (n : ℝ)

theorem chosenHerbrandFunction_eq_localHerbrandFunction
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (s : ℝ) :
    ClassFieldTheory.herbrandFunction K
        (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring s =
      herbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L) s

theorem canonicalHerbrandFunction_eq_localHerbrandFunction
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (s : ℝ) :
    ClassFieldTheory.herbrandFunction K
        (ValuativeRel.valuation L).valuationSubring s =
      herbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L) s

theorem canonicalInverseHerbrandFunction_eq_localInverseHerbrandFunction
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (t : ℝ) :
    ClassFieldTheory.inverseHerbrandFunction K L t =
      inverseHerbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L) t

theorem mem_canonicalUpperRamificationGroup_iff_mem_localUpperRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (t : ℝ) (σ : Gal(L/K))
    (hσ : σ ∈
      ((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K) :
    (⟨σ, hσ⟩ :
      ((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K) ∈
        ClassFieldTheory.upperRamificationGroup K L t ↔
      σ ∈ localUpperRamificationGroup K L t

theorem upperRamificationGroup_map_subtype_eq_localUpperRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (t : ℝ) :
    (ClassFieldTheory.upperRamificationGroup K L t).map
      (((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K).subtype =
        localUpperRamificationGroup K L t

theorem upperRamificationGroupAfter_map_subtype_eq_localUpperRamificationGroupAfter
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (t : ℝ) :
    (ClassFieldTheory.upperRamificationGroupAfter K L t).map
      (((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K).subtype =
        localUpperRamificationGroupAfter K L t

theorem chosenLowerRamificationGroup_eq_iff_localLowerRamificationGroup_eq
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (m n : ℕ) :
    ClassFieldTheory.lowerRamificationGroup K
        (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring m =
      ClassFieldTheory.lowerRamificationGroup K
        (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring n ↔
      localLowerRamificationGroup K L (m : ℝ) =
        localLowerRamificationGroup K L (n : ℝ)

theorem canonicalIsLowerRamificationJump_iff
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (n : ℕ) :
    ClassFieldTheory.IsLowerRamificationJump K
        (ValuativeRel.valuation L).valuationSubring n ↔
      localLowerRamificationGroup K L (n : ℝ) ≠
        localLowerRamificationGroup K L ((n + 1 : ℕ) : ℝ)

theorem localLowerRamificationGroup_le_succ_of_nat_lt
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ) {s : ℝ} (hs : (n : ℝ) < s) :
    localLowerRamificationGroup K L s ≤
      localLowerRamificationGroup K L ((n + 1 : ℕ) : ℝ)

theorem isLocalUpperRamificationJump_herbrand_nat_of_lower_ne_succ
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    (n : ℕ)
    (hjump : localLowerRamificationGroup K L (n : ℝ) ≠
      localLowerRamificationGroup K L ((n + 1 : ℕ) : ℝ)) :
    IsLocalUpperRamificationJump K L
      (herbrandFunctionOfUniqueExtension
        (base := (localCompleteDVF K).toDVF)
        (target := (chosenLocalExtensionCompleteDVF K L).toDVF)
        (chosenLocalExtensionCompleteDVF_hasUniqueDVFValuationExtension.{0} K L)
        (n : ℝ))

theorem hasseArf_canonical
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    {n : ℕ}
    (hn : ClassFieldTheory.IsLowerRamificationJump K
      (ValuativeRel.valuation L).valuationSubring n) :
    ∃ z : ℤ,
      ClassFieldTheory.herbrandFunctionAtLowerIndex K
        (ValuativeRel.valuation L).valuationSubring n = (z : ℚ)

def shrinkAlgebra
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L] :
    Algebra (Shrink.{0} K) (Shrink.{0} L)

theorem shrinkAlgebra_commutes
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    (algebraMap (Shrink.{0} K) (Shrink.{0} L)).comp
      (Shrink.ringEquiv K).symm.toRingHom =
        (Shrink.ringEquiv L).symm.toRingHom.comp (algebraMap K L) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  by
    apply RingHom.ext
    intro x
    change (Shrink.ringEquiv L).symm
      (algebraMap K L (Shrink.ringEquiv K ((Shrink.ringEquiv K).symm x))) =
        (Shrink.ringEquiv L).symm (algebraMap K L x)
    simp

theorem shrink_finiteDimensional
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Small.{0} K] [Small.{0} L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    FiniteDimensional (Shrink.{0} K) (Shrink.{0} L) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  Module.Finite.of_equiv_equiv
    (Shrink.ringEquiv K).symm (Shrink.ringEquiv L).symm
    (shrinkAlgebra_commutes K L)

theorem shrink_isAbelianGalois
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [IsAbelianGalois K L] [Small.{0} K] [Small.{0} L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    IsAbelianGalois (Shrink.{0} K) (Shrink.{0} L) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  ClassFieldTheory.isAbelianGalois_of_equiv_equiv
    (Shrink.ringEquiv K).symm (Shrink.ringEquiv L).symm
    (shrinkAlgebra_commutes K L)

def shrinkGalEquiv
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    Gal(Shrink.{0} L / Shrink.{0} K) ≃ Gal(L/K) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  ClassFieldTheory.galEquiv_of_equiv_equiv
    (Shrink.ringEquiv K).symm (Shrink.ringEquiv L).symm
    (shrinkAlgebra_commutes K L)

theorem shrinkGalEquiv_apply
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    ∀ (σ : Gal(Shrink.{0} L / Shrink.{0} K)) (x : Shrink.{0} L),
      shrinkGalEquiv K L σ (Shrink.ringEquiv L x) =
        Shrink.ringEquiv L (σ x) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  by
    intro σ x
    simp [shrinkGalEquiv, ClassFieldTheory.galEquiv_of_equiv_equiv]

theorem shrink_valuationSubring_eq_comap
    (L : Type*) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Small.{0} L] :
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring =
      (ValuativeRel.valuation L).valuationSubring.comap
        (Shrink.ringEquiv L).toRingHom :=
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    let v := shrinkLocalFieldValuation L
    have hv : (ValuativeRel.valuation (Shrink.{0} L)).IsEquiv v :=
      letI : v.Compatible := Valuation.Compatible.ofValuation v
      ValuativeRel.isEquiv _ _
    ext x
    change (ValuativeRel.valuation (Shrink.{0} L)) x ≤ 1 ↔
      (ValuativeRel.valuation L) (Shrink.ringEquiv L x) ≤ 1
    exact hv.le_one_iff_le_one.trans (by simp [v, shrinkLocalFieldValuation])

theorem shrink_mem_pointwise_smul_iff
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ∀ (σ : Gal(Shrink.{0} L / Shrink.{0} K)) (x : Shrink.{0} L),
      x ∈ σ • (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring ↔
        Shrink.ringEquiv L x ∈
          shrinkGalEquiv K L σ •
            (ValuativeRel.valuation L).valuationSubring :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    let e := Shrink.ringEquiv L
    let B := (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring
    let A := (ValuativeRel.valuation L).valuationSubring
    have hmem (y : Shrink.{0} L) : y ∈ B ↔ e y ∈ A := by
      rw [show B = A.comap e.toRingHom from shrink_valuationSubring_eq_comap L]
      rfl
    intro σ x
    have hleft := ValuationSubring.mem_smul_pointwise_iff_exists σ x B
    have hright := ValuationSubring.mem_smul_pointwise_iff_exists
      (shrinkGalEquiv K L σ) (e x) A
    constructor
    · intro hx
      obtain ⟨y, hy, heq⟩ := hleft.mp hx
      apply hright.mpr
      refine ⟨e y, (hmem y).mp hy, ?_⟩
      change σ y = x at heq
      change shrinkGalEquiv K L σ (e y) = e x
      rw [shrinkGalEquiv_apply K L σ y]
      exact congrArg e heq
    · intro hx
      obtain ⟨z, hz, heq⟩ := hright.mp hx
      let y := e.symm z
      apply hleft.mpr
      refine ⟨y, (hmem y).mpr ?_, ?_⟩
      · simpa [y] using hz
      · change shrinkGalEquiv K L σ z = e x at heq
        change σ y = x
        apply e.injective
        have hnat := shrinkGalEquiv_apply K L σ y
        change shrinkGalEquiv K L σ (e y) = e (σ y) at hnat
        rw [← hnat]
        simpa [y] using heq

theorem shrink_mem_decompositionSubgroup_iff
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ∀ σ : Gal(Shrink.{0} L / Shrink.{0} K),
      σ ∈ ((ValuativeRel.valuation (Shrink.{0} L)).valuationSubring).decompositionSubgroup
        (Shrink.{0} K) ↔
      shrinkGalEquiv K L σ ∈
        ((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    let e := Shrink.ringEquiv L
    let B := (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring
    let A := (ValuativeRel.valuation L).valuationSubring
    have hmem (x : Shrink.{0} L) : x ∈ B ↔ e x ∈ A := by
      rw [show B = A.comap e.toRingHom from shrink_valuationSubring_eq_comap L]
      rfl
    intro σ
    change σ • B = B ↔ shrinkGalEquiv K L σ • A = A
    constructor
    · intro h
      apply ValuationSubring.ext
      intro z
      let x := e.symm z
      calc
        z ∈ shrinkGalEquiv K L σ • A ↔ x ∈ σ • B := by
          simpa [x, e] using (shrink_mem_pointwise_smul_iff K L σ x).symm
        _ ↔ x ∈ B := by rw [h]
        _ ↔ z ∈ A := by simpa [x] using hmem x
    · intro h
      apply ValuationSubring.ext
      intro x
      calc
        x ∈ σ • B ↔ e x ∈ shrinkGalEquiv K L σ • A :=
          shrink_mem_pointwise_smul_iff K L σ x
        _ ↔ e x ∈ A := by rw [h]
        _ ↔ x ∈ B := (hmem x).symm

def shrink_valuationSubringRingEquiv
    (L : Type*) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Small.{0} L] :
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring ≃+*
      (ValuativeRel.valuation L).valuationSubring :=
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  RingEquiv.restrict (Shrink.ringEquiv L) _ _ (by
    intro x
    rw [shrink_valuationSubring_eq_comap L]
    rfl)

theorem shrink_mem_maximalIdeal_pow_iff
    (L : Type*) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Small.{0} L] (n : ℕ) :
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ∀ x : (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring,
      x ∈ (IsLocalRing.maximalIdeal
        (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring) ^ n ↔
      shrink_valuationSubringRingEquiv L x ∈
        (IsLocalRing.maximalIdeal
          (ValuativeRel.valuation L).valuationSubring) ^ n :=
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    intro x
    let e := shrink_valuationSubringRingEquiv L
    have hmap :
        (IsLocalRing.maximalIdeal
          (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring ^ n).map e =
          (IsLocalRing.maximalIdeal
            (ValuativeRel.valuation L).valuationSubring) ^ n := by
      rw [Ideal.map_pow, IsLocalRing.map_ringEquiv_maximalIdeal]
    rw [← hmap]
    exact (Ideal.apply_mem_of_equiv_iff (f := e)).symm

theorem shrink_mem_lowerRamificationGroup_iff
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    (n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ∀ (σ : Gal(Shrink.{0} L / Shrink.{0} K))
      (hσ : σ ∈
        ((ValuativeRel.valuation (Shrink.{0} L)).valuationSubring).decompositionSubgroup
          (Shrink.{0} K)),
      (⟨σ, hσ⟩ :
        ((ValuativeRel.valuation (Shrink.{0} L)).valuationSubring).decompositionSubgroup
          (Shrink.{0} K)) ∈
          ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K)
            (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n ↔
      (⟨shrinkGalEquiv K L σ,
          (shrink_mem_decompositionSubgroup_iff K L σ).mp hσ⟩ :
        ((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K) ∈
          ClassFieldTheory.lowerRamificationGroup K
            (ValuativeRel.valuation L).valuationSubring n :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    let B := (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring
    let A := (ValuativeRel.valuation L).valuationSubring
    let e := shrink_valuationSubringRingEquiv L
    intro σ hσ
    let τ := shrinkGalEquiv K L σ
    have hτ : τ ∈ A.decompositionSubgroup K :=
      (shrink_mem_decompositionSubgroup_iff K L σ).mp hσ
    have haction (x : B) :
        e ((⟨σ, hσ⟩ : B.decompositionSubgroup (Shrink.{0} K)) • x) =
          (⟨τ, hτ⟩ : A.decompositionSubgroup K) • e x := by
      apply Subtype.ext
      change (Shrink.ringEquiv L) (σ (x : Shrink.{0} L)) =
        τ ((Shrink.ringEquiv L) (x : Shrink.{0} L))
      exact (shrinkGalEquiv_apply K L σ x).symm
    have hpow (x : B) :
        (⟨σ, hσ⟩ : B.decompositionSubgroup (Shrink.{0} K)) • x - x ∈
          (IsLocalRing.maximalIdeal B) ^ (n + 1) ↔
        (⟨τ, hτ⟩ : A.decompositionSubgroup K) • e x - e x ∈
          (IsLocalRing.maximalIdeal A) ^ (n + 1) := by
      have h := shrink_mem_maximalIdeal_pow_iff L (n + 1)
        ((⟨σ, hσ⟩ : B.decompositionSubgroup (Shrink.{0} K)) • x - x)
      change _ ↔ e ((⟨σ, hσ⟩ : B.decompositionSubgroup (Shrink.{0} K)) • x - x) ∈
        (IsLocalRing.maximalIdeal A) ^ (n + 1) at h
      rw [map_sub, haction] at h
      exact h
    change (∀ x : B,
      (⟨σ, hσ⟩ : B.decompositionSubgroup (Shrink.{0} K)) • x - x ∈
        (IsLocalRing.maximalIdeal B) ^ (n + 1)) ↔
      (∀ y : A,
        (⟨τ, hτ⟩ : A.decompositionSubgroup K) • y - y ∈
          (IsLocalRing.maximalIdeal A) ^ (n + 1))
    constructor
    · intro h y
      have hy := (hpow (e.symm y)).mp (h (e.symm y))
      simpa using hy
    · intro h x
      exact (hpow x).mpr (h (e x))

def shrinkDecompositionGroupEquiv
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ((ValuativeRel.valuation (Shrink.{0} L)).valuationSubring).decompositionSubgroup
      (Shrink.{0} K) ≃
      ((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  (shrinkGalEquiv K L).subtypeEquiv
    (shrink_mem_decompositionSubgroup_iff K L)

def shrinkLowerRamificationGroupEquiv
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K)
      (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n ≃
    ClassFieldTheory.lowerRamificationGroup K
      (ValuativeRel.valuation L).valuationSubring n :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  (shrinkDecompositionGroupEquiv K L).subtypeEquiv (by
    intro σ
    exact shrink_mem_lowerRamificationGroup_iff K L n σ.1 σ.2)

theorem shrink_card_lowerRamificationGroup_eq
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    Nat.card (ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K)
      (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n) =
    Nat.card (ClassFieldTheory.lowerRamificationGroup K
      (ValuativeRel.valuation L).valuationSubring n) :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  Nat.card_congr (shrinkLowerRamificationGroupEquiv K L n)

theorem shrink_lowerRamificationGroup_eq_iff
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (m n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K)
        (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring m =
      ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K)
        (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n ↔
    ClassFieldTheory.lowerRamificationGroup K
        (ValuativeRel.valuation L).valuationSubring m =
      ClassFieldTheory.lowerRamificationGroup K
        (ValuativeRel.valuation L).valuationSubring n :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    let B := (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring
    let A := (ValuativeRel.valuation L).valuationSubring
    let e := shrinkDecompositionGroupEquiv K L
    have hmem (i : ℕ) (σ : B.decompositionSubgroup (Shrink.{0} K)) :
        σ ∈ ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K) B i ↔
          e σ ∈ ClassFieldTheory.lowerRamificationGroup K A i :=
      shrink_mem_lowerRamificationGroup_iff K L i σ.1 σ.2
    constructor
    · intro h
      apply Subgroup.ext
      intro τ
      let σ := e.symm τ
      calc
        τ ∈ ClassFieldTheory.lowerRamificationGroup K A m ↔
            σ ∈ ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K) B m := by
              simpa [σ] using (hmem m σ).symm
        _ ↔ σ ∈ ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K) B n := by
              rw [h]
        _ ↔ τ ∈ ClassFieldTheory.lowerRamificationGroup K A n := by
              simpa [σ] using hmem n σ
    · intro h
      apply Subgroup.ext
      intro σ
      calc
        σ ∈ ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K) B m ↔
            e σ ∈ ClassFieldTheory.lowerRamificationGroup K A m := hmem m σ
        _ ↔ e σ ∈ ClassFieldTheory.lowerRamificationGroup K A n := by rw [h]
        _ ↔ σ ∈ ClassFieldTheory.lowerRamificationGroup (Shrink.{0} K) B n :=
          (hmem n σ).symm

theorem shrink_isLowerRamificationJump_iff
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ClassFieldTheory.IsLowerRamificationJump (Shrink.{0} K)
      (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n ↔
    ClassFieldTheory.IsLowerRamificationJump K
      (ValuativeRel.valuation L).valuationSubring n :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  not_congr (shrink_lowerRamificationGroup_eq_iff K L n (n + 1))

theorem shrink_herbrandFunctionAtLowerIndex_eq
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    [Small.{0} K] [Small.{0} L]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (n : ℕ) :
    letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
    letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
    ClassFieldTheory.herbrandFunctionAtLowerIndex (Shrink.{0} K)
      (ValuativeRel.valuation (Shrink.{0} L)).valuationSubring n =
    ClassFieldTheory.herbrandFunctionAtLowerIndex K
      (ValuativeRel.valuation L).valuationSubring n :=
  letI : Algebra (Shrink.{0} K) (Shrink.{0} L) := shrinkAlgebra K L
  letI : ValuativeRel (Shrink.{0} L) := shrinkLocalFieldValuativeRel L
  by
    unfold ClassFieldTheory.herbrandFunctionAtLowerIndex
    congr 1
    · apply Finset.sum_congr rfl
      intro i hi
      rw [shrink_card_lowerRamificationGroup_eq K L i]
    · rw [shrink_card_lowerRamificationGroup_eq K L 0]