AbsoluteRamification.lean

theorem apply_pow
    (σ : Field.absoluteGaloisGroup K) (z : AlgebraicClosure K) (n : ℕ) :
    (show Gal(AlgebraicClosure K / K) from σ) (z ^ n) =
      ((show Gal(AlgebraicClosure K / K) from σ) z) ^ n := by
  exact map_pow (show Gal(AlgebraicClosure K / K) from σ) z n

instance absoluteGaloisGroupMulSemiringActionAlgebraicClosure :
    MulSemiringAction
      (Field.absoluteGaloisGroup K) (AlgebraicClosure K)

abbrev decompositionSubgroup
    (A : ValuationSubring (AlgebraicClosure K)) :
    Subgroup (Field.absoluteGaloisGroup K)

instance decompositionSubgroupMulSemiringAction
    (A : ValuationSubring (AlgebraicClosure K)) :
    MulSemiringAction (decompositionSubgroup K A) A

theorem decompositionSubgroup_eq_stabilizer
    (A : ValuationSubring (AlgebraicClosure K)) :
    decompositionSubgroup K A =
      MulAction.stabilizer (Field.absoluteGaloisGroup K) A

theorem mem_decompositionSubgroup_iff
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ decompositionSubgroup K A ↔ σ • A = A

theorem decompositionSubgroup_eq_top_iff_forall_smul_eq
    (A : ValuationSubring (AlgebraicClosure K)) :
    decompositionSubgroup K A = ⊤ ↔
      ∀ σ : Field.absoluteGaloisGroup K, σ • A = A

theorem decompositionSubgroup_eq_top_of_finite_separable_restrictUnique
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension v A.valuation]
    (huniq :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∀ (B : ValuationSubring E)
            [_root_.Valuation.HasExtension v B.valuation],
              (RamificationTheory.ValuationSubring.restrictIntermediateField A E) = B) :
    decompositionSubgroup K A = ⊤

theorem valuationSubring_mem_preserved_on_finite_separable_intermediate_of_restrictUnique
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (E : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [Algebra.IsSeparable K E]
    (huniq :
      ∀ (B : ValuationSubring E)
        [_root_.Valuation.HasExtension F.valuation B.valuation],
          (RamificationTheory.ValuationSubring.restrictIntermediateField A E) = B)
    (σ : Field.absoluteGaloisGroup K) (x : E) :
    ((x : AlgebraicClosure K) ∈ A) ↔
      (show Gal(AlgebraicClosure K / K) from σ) (x : AlgebraicClosure K) ∈ A :=
  (open RamificationTheory.ValuationSubring in
    mem_algEquiv_apply_iff_of_restrictIntermediateField_unique
      (v := F.valuation) (A := A) (E := E) huniq
      (show Gal(AlgebraicClosure K / K) from σ) x)

theorem valuationSubring_mem_preserved_on_finite_separable_intermediate_of_integral
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (E : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [Algebra.IsSeparable K E]
    (hintegral :
      ∀ (B : ValuationSubring E)
        [_root_.Valuation.HasExtension F.valuation B.valuation],
          Algebra.IsIntegral F.valuation.valuationSubring
            B.valuation.valuationSubring)
    (σ : Field.absoluteGaloisGroup K) (x : E) :
    ((x : AlgebraicClosure K) ∈ A) ↔
      (show Gal(AlgebraicClosure K / K) from σ) (x : AlgebraicClosure K) ∈ A := by
  exact
    valuationSubring_mem_preserved_on_finite_separable_intermediate_of_restrictUnique
      (K := K) (F := F) (A := A) (E := E)
      (huniq := by
        intro B _
        have hAExt : _root_.Valuation.HasExtension F.valuation
            ((RamificationTheory.ValuationSubring.restrictIntermediateField A E)).valuation :=
          RamificationTheory.ValuationSubring.restrictIntermediateField_hasExtension
            (v := F.valuation) (A := A) E
        have hAInt : Algebra.IsIntegral F.valuation.valuationSubring
            ((RamificationTheory.ValuationSubring.restrictIntermediateField A
              E)).valuation.valuationSubring :=
          hintegral ((RamificationTheory.ValuationSubring.restrictIntermediateField A E))
        have hBInt : Algebra.IsIntegral F.valuation.valuationSubring
            B.valuation.valuationSubring :=
          hintegral B
        have hsub :
            ((RamificationTheory.ValuationSubring.restrictIntermediateField A
              E)).valuation.valuationSubring =
              B.valuation.valuationSubring := by
          ext z
          constructor
          · intro hz
            have hz_int : z ∈ integralClosure F.valuation.valuationSubring E :=
              (open ValuationTheory.DiscreteValuationField.Valuation in
                valuationSubring_mem_integralClosure_of_isIntegral
                  (L := E) F.valuation
                    ((RamificationTheory.ValuationSubring.restrictIntermediateField
                    A E)).valuation ⟨z, hz⟩)
            exact
              (open ValuationTheory.DiscreteValuationField.Valuation in
                integralClosure_mem_valuationSubring_of_hasExtension
                  (L := E) F.valuation B.valuation ⟨z, hz_int⟩)
          · intro hz
            have hz_int : z ∈ integralClosure F.valuation.valuationSubring E :=
              (open ValuationTheory.DiscreteValuationField.Valuation in
                valuationSubring_mem_integralClosure_of_isIntegral
                  (L := E) F.valuation B.valuation ⟨z, hz⟩)
            exact
              (open ValuationTheory.DiscreteValuationField.Valuation in
                integralClosure_mem_valuationSubring_of_hasExtension
                  (L := E) F.valuation
                    ((RamificationTheory.ValuationSubring.restrictIntermediateField
                    A E)).valuation ⟨z, hz_int⟩)
        calc
          RamificationTheory.ValuationSubring.restrictIntermediateField A E =
              (RamificationTheory.ValuationSubring.restrictIntermediateField A
                E).valuation.valuationSubring :=
            (ValuationSubring.valuationSubring_valuation _).symm
          _ = B.valuation.valuationSubring := hsub
          _ = B := ValuationSubring.valuationSubring_valuation B)
      (σ := σ) (x := x)

theorem valuationSubring_mem_preserved_on_finite_separable_intermediate_of_moduleFinite
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (E : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [Algebra.IsSeparable K E]
    (hfinite :
      ∀ (B : ValuationSubring E)
        [_root_.Valuation.HasExtension F.valuation B.valuation],
          Module.Finite F.valuation.valuationSubring
            B.valuation.valuationSubring)
    (σ : Field.absoluteGaloisGroup K) (x : E) :
    ((x : AlgebraicClosure K) ∈ A) ↔
      (show Gal(AlgebraicClosure K / K) from σ) (x : AlgebraicClosure K) ∈ A :=
  valuationSubring_mem_preserved_on_finite_separable_intermediate_of_integral
    (K := K) (F := F) (A := A) (E := E)
    (hintegral := by
      intro B _
      let : Module.Finite F.valuation.valuationSubring
          B.valuation.valuationSubring :=
        hfinite B
      infer_instance)
    (σ := σ) (x := x)

theorem valuationSubring_mem_preserved_on_finite_separable_intermediate
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (E : IntermediateField K (AlgebraicClosure K))
    [FiniteDimensional K E] [Algebra.IsSeparable K E]
    (target : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, w} E)
    (hA : target.valuation.valuationSubring =
      (RamificationTheory.ValuationSubring.restrictIntermediateField A E))
    (huniq :
      (open ValuationTheory.DiscreteValuationField.HenselianDVF in
        HasUniqueValuationExtension.{u, v, u, w, u} F target))
    (σ : Field.absoluteGaloisGroup K) (x : E) :
    ((x : AlgebraicClosure K) ∈ A) ↔
      (show Gal(AlgebraicClosure K / K) from σ) (x : AlgebraicClosure K) ∈ A :=
  (open RamificationTheory.ValuationSubring in
    mem_algEquiv_apply_iff_of_restrictIntermediateField_henselianUnique
      (base := F) (A := A) (E := E) (target := target) hA huniq
      (show Gal(AlgebraicClosure K / K) from σ) x)

theorem decompositionSubgroup_eq_top_of_henselianDVF_restrictUnique
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (huniq :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∀ (B : ValuationSubring E)
            [_root_.Valuation.HasExtension F.valuation B.valuation],
              (RamificationTheory.ValuationSubring.restrictIntermediateField A E) = B) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_eq_top_of_finite_separable_integral
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hintegral :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∀ (B : ValuationSubring E)
            [_root_.Valuation.HasExtension F.valuation B.valuation],
              Algebra.IsIntegral F.valuation.valuationSubring
                B.valuation.valuationSubring) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_eq_top_of_finite_separable_moduleFinite
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hfinite :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∀ (B : ValuationSubring E)
            [_root_.Valuation.HasExtension F.valuation B.valuation],
              Module.Finite F.valuation.valuationSubring
                B.valuation.valuationSubring) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_eq_top_of_finite_separable_henselianUnique
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (huniq :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∃ target : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, w} E,
            target.valuation.valuationSubring =
              (RamificationTheory.ValuationSubring.restrictIntermediateField A E) ∧
              (open ValuationTheory.DiscreteValuationField.HenselianDVF in
                HasUniqueValuationExtension.{u, v, u, w, u} F target)) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_eq_top_of_henselianDVF_powerRoute
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (huniq :
      ∀ (E : IntermediateField K (AlgebraicClosure K))
        [FiniteDimensional K E] [Algebra.IsSeparable K E],
          ∃ target : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, w} E,
            target.valuation.valuationSubring =
              (RamificationTheory.ValuationSubring.restrictIntermediateField A E) ∧
              (open ValuationTheory.DiscreteValuationField.HenselianDVF in
                HasUniqueValuationExtension.{u, v, u, w, u} F target)) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_eq_top_of_forall_smul_eq
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : ∀ σ : Field.absoluteGaloisGroup K, σ • A = A) :
    decompositionSubgroup K A = ⊤

theorem decompositionSubgroup_pointwise_smul
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : Field.absoluteGaloisGroup K) :
    decompositionSubgroup K (σ • A) =
      Subgroup.map (MulAut.conj σ).toMonoidHom
        (decompositionSubgroup K A)

abbrev inertiaSubgroup
    (A : ValuationSubring (AlgebraicClosure K)) :
    Subgroup (decompositionSubgroup K A)

def decompositionResidueAction
    (A : ValuationSubring (AlgebraicClosure K)) :
    decompositionSubgroup K A →*
      (IsLocalRing.ResidueField A ≃+* IsLocalRing.ResidueField A)

theorem inertiaSubgroup_eq_ker
    (A : ValuationSubring (AlgebraicClosure K)) :
    inertiaSubgroup K A =
      MonoidHom.ker (decompositionResidueAction K A)

theorem decompositionResidueAction_ker
    (A : ValuationSubring (AlgebraicClosure K)) :
    MonoidHom.ker (decompositionResidueAction K A) =
      inertiaSubgroup K A

instance inertiaSubgroup_normal
    (A : ValuationSubring (AlgebraicClosure K)) :
    (inertiaSubgroup K A).Normal

theorem mem_inertiaSubgroup_iff
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : decompositionSubgroup K A) :
    σ ∈ inertiaSubgroup K A ↔
      decompositionResidueAction K A σ = 1

theorem inertiaSubtype_mulExact_decompositionResidueAction
    (A : ValuationSubring (AlgebraicClosure K)) :
    Function.MulExact
      (inertiaSubgroup K A).subtype
      (decompositionResidueAction K A)

abbrev inertiaSubgroupInAbsolute
    (A : ValuationSubring (AlgebraicClosure K)) :
    Subgroup (Field.absoluteGaloisGroup K)

theorem inertiaSubgroupInAbsolute_le_decompositionSubgroup
    (A : ValuationSubring (AlgebraicClosure K)) :
    inertiaSubgroupInAbsolute K A ≤ decompositionSubgroup K A

theorem mem_inertiaSubgroupInAbsolute_iff
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : Field.absoluteGaloisGroup K) :
    σ ∈ inertiaSubgroupInAbsolute K A ↔
      ∃ hσ : σ ∈ decompositionSubgroup K A,
        decompositionResidueAction K A ⟨σ, hσ⟩ = 1

theorem inertiaSubgroupInAbsolute_eq_decompositionSubgroup_iff
    (A : ValuationSubring (AlgebraicClosure K)) :
    inertiaSubgroupInAbsolute K A = decompositionSubgroup K A ↔
      decompositionResidueAction K A = 1

theorem inertiaSubgroupInAbsolute_eq_bot_iff_decompositionResidueAction_injective
    (A : ValuationSubring (AlgebraicClosure K)) :
    inertiaSubgroupInAbsolute K A = ⊥ ↔
      Function.Injective (decompositionResidueAction K A)

theorem inertiaSubgroupInAbsolute_eq_top_iff
    (A : ValuationSubring (AlgebraicClosure K)) :
    inertiaSubgroupInAbsolute K A = ⊤ ↔
      decompositionSubgroup K A = ⊤ ∧ decompositionResidueAction K A = 1

def toDecompositionSubgroupOfEqTop
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    Field.absoluteGaloisGroup K →*
      decompositionSubgroup K A where
  toFun σ := ⟨σ, by rw [hA]; exact Subgroup.mem_top σ⟩
  map_one' := by
    ext
    rfl
  map_mul' _ _ := by
    ext
    rfl

theorem toDecompositionSubgroupOfEqTop_coe
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    (toDecompositionSubgroupOfEqTop K A hA σ :
      Field.absoluteGaloisGroup K) = σ

def absoluteResidueActionOfDecompositionSubgroupEqTop
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    Field.absoluteGaloisGroup K →*
      (IsLocalRing.ResidueField A ≃+* IsLocalRing.ResidueField A)

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_apply
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    absoluteResidueActionOfDecompositionSubgroupEqTop K A hA σ =
      decompositionResidueAction K A
        (toDecompositionSubgroupOfEqTop K A hA σ)

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_range
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    MonoidHom.range
        (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA) =
      MonoidHom.range (decompositionResidueAction K A)

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_ker
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    MonoidHom.ker
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA) =
        inertiaSubgroupInAbsolute K A

theorem inertiaSubgroupInAbsoluteSubtype_mulExact_absoluteResidueActionOfDecompositionSubgroupEqTop
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    Function.MulExact
      (inertiaSubgroupInAbsolute K A).subtype
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA)

def absoluteResidueActionOfHenselianDVF
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hA : decompositionSubgroup K A = ⊤) :
    MonoidHom (Field.absoluteGaloisGroup K)
      (RingEquiv (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField A))

theorem absoluteResidueActionOfHenselianDVF_apply
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hA : decompositionSubgroup K A = ⊤)
    (sigma : Field.absoluteGaloisGroup K) :
    absoluteResidueActionOfHenselianDVF K F A hA sigma =
      absoluteResidueActionOfDecompositionSubgroupEqTop K A hA sigma

theorem absoluteResidueActionOfHenselianDVF_ker
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hA : decompositionSubgroup K A = ⊤) :
    MonoidHom.ker (absoluteResidueActionOfHenselianDVF K F A hA) =
      inertiaSubgroupInAbsolute K A

theorem inertiaSubgroupInAbsoluteSubtype_mulExact_absoluteResidueActionOfHenselianDVF
    (F : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, v} K)
    (A : ValuationSubring (AlgebraicClosure K))
    [_root_.Valuation.HasExtension F.valuation A.valuation]
    (hA : decompositionSubgroup K A = ⊤) :
    Function.MulExact
      (inertiaSubgroupInAbsolute K A).subtype
      (absoluteResidueActionOfHenselianDVF K F A hA)

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_eq_one_iff_mem_inertia
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    absoluteResidueActionOfDecompositionSubgroupEqTop K A hA σ = 1 ↔
      σ ∈ inertiaSubgroupInAbsolute K A

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_eq_iff_div_mem_inertia
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ τ : Field.absoluteGaloisGroup K) :
    absoluteResidueActionOfDecompositionSubgroupEqTop K A hA σ =
        absoluteResidueActionOfDecompositionSubgroupEqTop K A hA τ ↔
      σ / τ ∈ inertiaSubgroupInAbsolute K A

theorem inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    (inertiaSubgroupInAbsolute K A).Normal

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_eq_iff_inv_mul_mem_inertia
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ τ : Field.absoluteGaloisGroup K) :
    absoluteResidueActionOfDecompositionSubgroupEqTop K A hA σ =
        absoluteResidueActionOfDecompositionSubgroupEqTop K A hA τ ↔
      τ⁻¹ * σ ∈ inertiaSubgroupInAbsolute K A

theorem absoluteResidueActionOfDecompositionSubgroupEqTop_injective_iff_inertia_eq_bot
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    Function.Injective
        (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA) ↔
      inertiaSubgroupInAbsolute K A = ⊥

def absoluteQuotientKernelEquivResidueActionRangeOfDecompositionSubgroupEqTop
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    Field.absoluteGaloisGroup K ⧸
        MonoidHom.ker
          (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA) ≃*
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).range

theorem absoluteQuotientKernelEquivResidueActionRangeOfDecompositionSubgroupEqTop_mk
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    absoluteQuotientKernelEquivResidueActionRangeOfDecompositionSubgroupEqTop
        K A hA
        (QuotientGroup.mk'
          (MonoidHom.ker
            (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA)) σ) =
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).rangeRestrict
        σ

def absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤) :
    letI : (inertiaSubgroupInAbsolute K A).Normal :=
      inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
    Field.absoluteGaloisGroup K ⧸ inertiaSubgroupInAbsolute K A ≃*
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).range := by
  letI : (inertiaSubgroupInAbsolute K A).Normal :=
    inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
  exact (QuotientGroup.quotientMulEquivOfEq
      (absoluteResidueActionOfDecompositionSubgroupEqTop_ker K A hA).symm).trans
    (absoluteQuotientKernelEquivResidueActionRangeOfDecompositionSubgroupEqTop K A hA)

theorem absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop_mk
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    letI : (inertiaSubgroupInAbsolute K A).Normal :=
      inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
    absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop
        K A hA
        (QuotientGroup.mk' (inertiaSubgroupInAbsolute K A) σ) =
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).rangeRestrict
        σ := by
  let : (inertiaSubgroupInAbsolute K A).Normal :=
    inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
  change
    absoluteQuotientKernelEquivResidueActionRangeOfDecompositionSubgroupEqTop
        K A hA
        (QuotientGroup.mk'
          (MonoidHom.ker
            (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA)) σ) =
      (absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).rangeRestrict σ
  rfl

theorem
absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop_symm_rangeRestrict
    (A : ValuationSubring (AlgebraicClosure K))
    (hA : decompositionSubgroup K A = ⊤)
    (σ : Field.absoluteGaloisGroup K) :
    letI : (inertiaSubgroupInAbsolute K A).Normal :=
      inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
    (absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop
        K A hA).symm
        ((absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).rangeRestrict
          σ) =
      QuotientGroup.mk' (inertiaSubgroupInAbsolute K A) σ := by
  let : (inertiaSubgroupInAbsolute K A).Normal :=
    inertiaSubgroupInAbsolute_normal_of_decompositionSubgroup_eq_top K A hA
  apply
    (absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop
      K A hA).injective
  rw [absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop_mk]
  exact
    (absoluteQuotientInertiaEquivResidueActionRangeOfDecompositionSubgroupEqTop
      K A hA).apply_symm_apply
      ((absoluteResidueActionOfDecompositionSubgroupEqTop K A hA).rangeRestrict σ)

def decompositionQuotientInertiaEquivResidueActionRange
    (A : ValuationSubring (AlgebraicClosure K)) :
    decompositionSubgroup K A ⧸ inertiaSubgroup K A ≃*
      (decompositionResidueAction K A).range

theorem decompositionQuotientInertiaEquivResidueActionRange_mk
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : decompositionSubgroup K A) :
    decompositionQuotientInertiaEquivResidueActionRange K A
        (QuotientGroup.mk' (inertiaSubgroup K A) σ) =
      (decompositionResidueAction K A).rangeRestrict σ

theorem decompositionQuotientInertiaEquivResidueActionRange_symm_rangeRestrict
    (A : ValuationSubring (AlgebraicClosure K))
    (σ : decompositionSubgroup K A) :
    (decompositionQuotientInertiaEquivResidueActionRange K A).symm
        ((decompositionResidueAction K A).rangeRestrict σ) =
      QuotientGroup.mk' (inertiaSubgroup K A) σ