Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ExtCitation_LocalLevelResidues.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/RepresentationTheory/AbsoluteGaloisGroup.lean

Local Galois action at : valuation ring, residues, Frobenius

For a prime q the module writes \mathcal O = OO q for the valuation subring \{x : \|x\|_{+} \le 1\} of an algebraic closure PadicAlgCl q of \mathbb Q_q, and G = GG q for \mathrm{Aut}_{\mathbb Q_q}(\overline{\mathbb Q_q}). It equips \mathcal O with the G-action induced by evaluation (a MulSemiringAction, the norm being preserved), with a \mathbb Z_q-algebra structure intToOO coming from \mathbb Z_q \to \mathbb Q_q \to \overline{\mathbb Q_q}, and records that the action commutes with \mathbb Z_q, that \mathcal O^{G} = \mathbb Z_q (Algebra.IsInvariant) and that stabilisers are open. Preliminary instances give the Krull-topology facts used for this: a fixing subgroup of a finite-dimensional intermediate field has finite index, \mathrm{Aut}_K(L) is compact for L/K algebraic, acts continuously on the discrete L, and is invariant when L/K is Galois. From the identification of the maximal ideal of \mathcal O over that of \mathbb Z_q one obtains exists_frob_local: some \sigma \in G satisfies \sigma x - x^{q} \in \mathfrak m for all x \in \mathcal O.

For a finite intermediate field K_w it defines R_w = \mathcal O \cap K_w, G_w = \mathrm{Gal}(\overline{\mathbb Q_q}/K_w), their compatibilities, and surjectivity of the stabiliser map G_w \to \mathrm{Aut}_{R_w/\mathfrak m_w}(\mathcal O/\mathfrak m). On \bar\kappa = \mathcal O/\mathfrak m, of characteristic q, kM q M is the subfield \{y : y^{q^M} = y\} (finite for M > 0); each g \in G acts on it as y \mapsto y^{q^{n}} for some n, and residue_mem_kM places the residue of every x \in R_w in kM q (N!), N = [K_w : \mathbb Q_q], via a monic \mathbb Z_q-lift of the minimal polynomial. Transport lemmas move these data to the place padicPlace q of \overline{\mathbb Q}: the decomposition-subgroup homomorphism rD, the criterion for lying in the pulled-back inertia subgroup, and the statement that \sigma as above is a Frobenius at that place. Finally, any two elements of G commute on \bar\kappa; an element acting trivially on the residues of R_w fixes elements of K_w fixed by all w congruent to the identity modulo \mathfrak m; and consequently, for such y, every g \in G satisfies g y = \varphi_0^{\,j} y for some j, where \varphi_0 raises residues to the q-th power.

Relation to Mathlib

IsArithFrobAt, Ideal.Quotient.stabilizerHom and Algebra.IsInvariant are Mathlib's; ContinuousSMulDiscrete and the predicates ValuationSubring.IsFrobeniusAt and ValuationSubring.inertiaSubgroupIn are the project's own notions, and padicPlace, padicEmbedding, localGaloisToGlobal come from the project's completion bridge.

Where it is used

These are the local ingredients at an auxiliary prime q used when comparing Frobenius and inertia at q inside the global Galois group of \overline{\mathbb Q}: the degree bound on residues and the surjectivity onto the residue automorphism group give that, on elements of a finite level fixed by the relevant inertia, every local automorphism acts as a power of Frobenius. This underlies the ramification computations in the Selmer-group part of the argument.

References

  1. J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer, 1979
  2. J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_ExtCitation_LocalLevelResidues.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ExtEndgame_ProductionDatum
import Definitions.Def_EllipticCurve_FrobeniusTrace
import Definitions.Def_Deformations_Frobenius

set_option autoImplicit false

open ExtCitation
open scoped NNReal

namespace ExtCitation.LocalLevel

theorem index_op_s17 {G : Type*} [Group G] (H : Subgroup G) :
    H.op.index = H.index := by
  trans (H.comap (MulEquiv.inv' G).symm.toMonoidHom).index
  · congr 1
    ext; simp
  · exact Subgroup.index_comap_of_surjective _ (MulEquiv.inv' G).symm.surjective

instance finiteIndex_op_s17 {G : Type*} [Group G] (H : Subgroup G) [H.FiniteIndex] :
    H.op.FiniteIndex := ⟨by rw [index_op_s17]; exact Subgroup.FiniteIndex.index_ne_zero⟩

lemma totallyBounded_s17 {G : Type*} [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (H : ∀ s ∈ nhds (1 : G), ∃ H : Subgroup G, H.FiniteIndex ∧ ↑H ⊆ s) :
    letI := IsTopologicalGroup.rightUniformSpace G
    TotallyBounded (Set.univ : Set G) := by
  letI := IsTopologicalGroup.rightUniformSpace G
  rintro s ⟨t, ht1, hts⟩
  obtain ⟨H, hH, hHs⟩ := H _ ht1
  have : Finite (Gᵐᵒᵖ ⧸ H.op) := Subgroup.finite_quotient_of_finiteIndex
  refine ⟨Set.range (MulOpposite.unop ∘ Quotient.out : Gᵐᵒᵖ ⧸ H.op → G),
    Set.finite_range _, fun x _ ↦
      Set.mem_iUnion₂_of_mem ⟨QuotientGroup.mk (.op x), rfl⟩ (hts (hHs ?_))⟩
  dsimp only
  rw [Function.comp_apply, SetLike.mem_coe, ← MulOpposite.unop_op (x⁻¹),
    ← MulOpposite.unop_mul, ← Subgroup.mem_op, MulOpposite.op_inv, ← QuotientGroup.eq]
  simp

instance finiteIndex_fixingSubgroup_s17 {K L : Type*} [Field K] [Field L] [Algebra K L]
    (E : IntermediateField K L) [FiniteDimensional K E] : E.fixingSubgroup.FiniteIndex := by
  let f : (L ≃ₐ[K] L) ⧸ E.fixingSubgroup → E →ₐ[K] L := Quotient.lift
    (fun f ↦ f.toAlgHom.comp E.val)
    (by rintro _ τ ⟨σ, rfl⟩; ext x; exact DFunLike.congr_arg τ (σ.2 x))
  have : Function.Injective f := by
    rintro ⟨σ⟩ ⟨τ⟩ (H : σ.toAlgHom.comp E.val = τ.toAlgHom.comp E.val)
    refine Quotient.sound ⟨⟨.op (τ⁻¹ * σ), fun x ↦ ?_⟩, by simp⟩
    simpa [AlgEquiv.aut_inv, AlgEquiv.symm_apply_eq] using DFunLike.congr_fun H x
  have := Finite.of_injective _ this
  exact Subgroup.finiteIndex_of_finite_quotient

open IntermediateField in
instance compactSpace_gal {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] :
    CompactSpace (L ≃ₐ[K] L) := by
  classical
  letI := IsTopologicalGroup.rightUniformSpace (L ≃ₐ[K] L)
  rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]
  refine ⟨totallyBounded_s17 fun s hs ↦ ?_, ?_⟩
  · obtain ⟨E, hE, H⟩ := (krullTopology_mem_nhds_one_iff _ _ _).mp hs
    refine ⟨_, inferInstance, H⟩
  · rintro f hf -
    have := hf.1
    have (x : L) :
        ∃ σ₀ : L ≃ₐ[K] L, ∃ t ∈ f, ∀ σ ∈ t, ∀ τ : L ≃ₐ[K] L, σ (τ x) = σ₀ (τ x) := by
      have : FiniteDimensional K K⟮x⟯ :=
        adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral _)
      obtain ⟨t, htf, H⟩ := ((Filter.HasBasis.cauchy_iff
        (by exact (galGroupBasis K L).nhds_one_hasBasis.comap _)).mp hf).2 _ (by
            exact ⟨_, ⟨normalClosure K K⟮x⟯ L, inferInstanceAs (FiniteDimensional K _), rfl⟩, rfl⟩)
      obtain ⟨σ, hσ⟩ := f.nonempty_of_mem htf
      refine ⟨σ, t, htf, fun τ hτ τ₀ ↦ ?_⟩
      have : σ (τ.symm (τ (τ₀ x))) = τ (τ₀ x) := H τ hτ σ hσ ⟨τ (τ₀ x), by
        refine SetLike.le_def.mp (le_iSup _ (τ.toAlgHom.comp <| τ₀.toAlgHom.comp (val _))) ?_
        exact ⟨⟨_, subset_adjoin _ _ (by simp)⟩, rfl⟩⟩
      simpa using this.symm
    choose σ₀ t htf H using this
    have H' (s σ hσ) := H s σ hσ .refl
    dsimp at H'
    let F : L ≃ₐ[K] L :=
    { toFun x := σ₀ x x
      invFun x := (σ₀ x).symm x
      left_inv x := by
        obtain ⟨σ, hσ₁, hσ₂⟩ := f.nonempty_of_mem (f.inter_mem (htf x) (htf (σ₀ x x)))
        dsimp
        have H' := H' _ _ hσ₁
        have : σ x = (σ₀ (σ₀ x x) x) := by simpa using H _ _ hσ₂ (σ₀ x).symm
        rw [← H', AlgEquiv.symm_apply_eq, H', ← this, H']
      right_inv x := by
        obtain ⟨σ, hσ₁, hσ₂⟩ := f.nonempty_of_mem (f.inter_mem (htf x) (htf ((σ₀ x).symm x)))
        dsimp
        replace H := H _ _ hσ₁ σ.symm
        simp only [AlgEquiv.apply_symm_apply, ← AlgEquiv.symm_apply_eq, AlgEquiv.symm_symm] at H
        rw [← H' _ _ hσ₂, H]
      map_mul' x y := by
        obtain ⟨σ, hσx, hσy, hσxy⟩ :=
          f.nonempty_of_mem (f.inter_mem (htf x) (f.inter_mem (htf y) (htf (x * y))))
        rw [← H' _ _ hσxy, ← H' _ _ hσx, ← H' _ _ hσy, map_mul]
      map_add' x y := by
        obtain ⟨σ, hσx, hσy, hσxy⟩ :=
          f.nonempty_of_mem (f.inter_mem (htf x) (f.inter_mem (htf y) (htf (x + y))))
        rw [← H' _ _ hσxy, ← H' _ _ hσx, ← H' _ _ hσy, map_add]
      commutes' := by simp }
    refine ⟨F, Set.mem_univ _, ?_⟩
    rw [((galGroupBasis K L).nhds_hasBasis F).ge_iff]
    rintro _ ⟨_, ⟨E, hE, rfl⟩, rfl⟩
    simp only [Set.image_mul_left]
    have ⟨s, hs⟩ := E.toSubmodule.fg_iff_finiteDimensional.mpr hE
    refine f.mem_of_superset ((Filter.biInter_finset_mem s).mpr fun i _ ↦ htf i) ?_
    rintro σ hσ ⟨x, hx⟩
    change F.symm (σ x) = x
    induction hs.ge hx using Submodule.span_induction with
    | zero | add | smul => simp_all
    | mem x h =>
      rw [AlgEquiv.symm_apply_eq]
      simp [F, ← H' _ _ (Set.mem_iInter₂.mp hσ _ h)]

open scoped IntermediateField in
instance continuousSMulDiscrete_gal {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] :
    ContinuousSMulDiscrete (L ≃ₐ[K] L) L := by
  constructor
  intro x y
  rw [isOpen_iff_forall_mem_open]
  rintro σ (hσ : _ = _)
  have : FiniteDimensional K K⟮x⟯ := IntermediateField.adjoin.finiteDimensional
      (Algebra.IsAlgebraic.isAlgebraic (R := K) x).isIntegral
  refine ⟨_, ?_, K⟮x⟯.fixingSubgroup_isOpen.smul σ, 1, one_mem _, by simp⟩
  rintro _ ⟨τ, hτ, rfl⟩
  have := (mem_fixingSubgroup_iff _).mp hτ x (IntermediateField.mem_adjoin_simple_self K x)
  simp only [smul_eq_mul, Set.mem_setOf_eq, mul_smul, this, hσ]

instance isInvariant_gal {K L : Type*} [Field K] [Field L] [Algebra K L] [IsGalois K L] :
    Algebra.IsInvariant K L (L ≃ₐ[K] L) :=
  ⟨fun _ H ↦ (InfiniteGalois.fixedField_fixingSubgroup
    (⊥ : IntermediateField K L)).le fun _ ↦ H _⟩

section Local

variable (q : ℕ) [Fact q.Prime]

abbrev OO : Type := ↥(padicIntegers q)

abbrev GG : Type := PadicAlgCl q ≃ₐ[ℚ_[q]] PadicAlgCl q

noncomputable instance smulOO : SMul (GG q) (OO q) :=
  ⟨fun g x => ⟨g (x : PadicAlgCl q), by
    rw [mem_padicIntegers_iff, nnnorm_padicAlgCl_algEquiv]; exact (mem_padicIntegers_iff q).mp x.2⟩⟩

@[simp] theorem coe_smul_OO (g : GG q) (x : OO q) : ((g • x : OO q) : PadicAlgCl q) = g (x : PadicAlgCl q) := rfl

noncomputable instance actOO : MulSemiringAction (GG q) (OO q) where
  one_smul x := Subtype.ext rfl
  mul_smul g h x := Subtype.ext rfl
  smul_zero g := Subtype.ext (map_zero g)
  smul_add g x y := Subtype.ext (map_add g _ _)
  smul_one g := Subtype.ext (map_one g)
  smul_mul g x y := Subtype.ext (map_mul g _ _)

noncomputable def intToOO : ℤ_[q] →+* OO q :=
  ((algebraMap ℚ_[q] (PadicAlgCl q)).comp PadicInt.Coe.ringHom).codRestrict (padicIntegers q) (fun x => by
    show algebraMap ℚ_[q] (PadicAlgCl q) (x : ℚ_[q]) ∈ padicIntegers q
    rw [mem_padicIntegers_iff, ← NNReal.coe_le_coe, coe_nnnorm, NNReal.coe_one]
    change ‖((x : ℚ_[q]) : PadicAlgCl q)‖ ≤ 1
    rw [PadicAlgCl.norm_extends]
    exact x.2)

noncomputable instance algOO : Algebra ℤ_[q] (OO q) := (intToOO q).toAlgebra

theorem algebraMap_OO_coe (x : ℤ_[q]) :
    ((algebraMap ℤ_[q] (OO q) x : OO q) : PadicAlgCl q) = algebraMap ℚ_[q] (PadicAlgCl q) (x : ℚ_[q]) := rfl

instance smulCommOO : SMulCommClass (GG q) ℤ_[q] (OO q) where
  smul_comm g r x := by
    apply Subtype.ext
    rw [Algebra.smul_def, Algebra.smul_def]
    change g ((algebraMap ℤ_[q] (OO q) r : PadicAlgCl q) * (x : PadicAlgCl q))
      = (algebraMap ℤ_[q] (OO q) r : PadicAlgCl q) * g (x : PadicAlgCl q)
    rw [map_mul, algebraMap_OO_coe, AlgEquiv.commutes]

instance isInvariantOO : Algebra.IsInvariant ℤ_[q] (OO q) (GG q) where
  isInvariant b hb := by
    haveI : IsGalois ℚ_[q] (PadicAlgCl q) := IsAlgClosure.isGalois ℚ_[q] (PadicAlgCl q)
    have hb' : ∀ g : GG q, g • (b : PadicAlgCl q) = b := fun g => congrArg Subtype.val (hb g)
    obtain ⟨x, hx⟩ := Algebra.IsInvariant.isInvariant (A := ℚ_[q]) (G := GG q) (b : PadicAlgCl q) hb'
    have hx1 : ‖x‖ ≤ 1 := by
      rw [← PadicAlgCl.norm_extends]
      change ‖algebraMap ℚ_[q] (PadicAlgCl q) x‖ ≤ 1
      rw [hx]
      have := (mem_padicIntegers_iff q).mp b.2
      exact_mod_cast this
    exact ⟨⟨x, hx1⟩, Subtype.ext hx⟩

instance csdOO : ContinuousSMulDiscrete (GG q) (OO q) := by
  rw [continuousSMulDiscrete_iff_isOpen_stabilizer]
  intro x
  have : (MulAction.stabilizer (GG q) x : Set (GG q)) = MulAction.stabilizer (GG q) (x : PadicAlgCl q) := by
    ext g
    simp only [SetLike.mem_coe, MulAction.mem_stabilizer_iff]
    exact ⟨fun h => congrArg Subtype.val h, fun h => Subtype.ext h⟩
  rw [this]
  exact ContinuousSMulDiscrete.isOpen_stabilizer (GG q) (x : PadicAlgCl q)

theorem natCast_mem_nonunits : ((q : ℕ) : PadicAlgCl q) ∈ (padicIntegers q).nonunits := by
  have hq : Valued.v ((q : ℕ) : PadicAlgCl q) = 1 / (q : ℝ≥0) := PadicAlgCl.valuation_p q
  have hq2 : (2 : ℕ) ≤ q := (Fact.out : q.Prime).two_le
  rw [ValuationSubring.mem_nonunits_iff, ← (Valuation.isEquiv_valuation_valuationSubring _).lt_one_iff_lt_one]
  change Valued.v ((q : ℕ) : PadicAlgCl q) < 1
  rw [hq, div_lt_one (by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_two hq2)]
  exact_mod_cast Nat.lt_of_lt_of_le Nat.one_lt_two hq2

theorem under_maximalIdeal_eq :
    (IsLocalRing.maximalIdeal (OO q)).under ℤ_[q] = IsLocalRing.maximalIdeal ℤ_[q] := by
  set P := (IsLocalRing.maximalIdeal (OO q)).under ℤ_[q] with hPdef
  have hqP : ((q : ℕ) : ℤ_[q]) ∈ P := by
    change ((q : ℕ) : ℤ_[q]) ∈ Ideal.comap (algebraMap ℤ_[q] (OO q)) (IsLocalRing.maximalIdeal (OO q))
    rw [Ideal.mem_comap, ← ValuationSubring.coe_mem_nonunits_iff, map_natCast]
    have : (((q : ℕ) : OO q) : PadicAlgCl q) = ((q : ℕ) : PadicAlgCl q) := by simp
    rw [this]
    exact natCast_mem_nonunits q
  have hP0 : P ≠ ⊥ := fun h => by
    have h0 : ((q : ℕ) : ℤ_[q]) = 0 := by simpa [h] using hqP
    exact (Nat.cast_ne_zero.mpr (Fact.out : q.Prime).ne_zero) h0
  haveI : P.IsPrime := Ideal.IsPrime.under ℤ_[q] (IsLocalRing.maximalIdeal (OO q))
  exact IsLocalRing.eq_maximalIdeal (Ideal.IsPrime.isMaximal ‹P.IsPrime› hP0)

theorem exists_frob_local : ∃ σ : GG q, ∀ x : OO q,
    ((σ • x - x ^ q : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits := by
  haveI : Algebra.IsIntegral ℚ_[q] (PadicAlgCl q) := ⟨fun x => (Algebra.IsAlgebraic.isAlgebraic x).isIntegral⟩
  let Q := IsLocalRing.maximalIdeal (OO q)
  have hP : Q.under ℤ_[q] = IsLocalRing.maximalIdeal ℤ_[q] := under_maximalIdeal_eq q
  haveI : Finite (ℤ_[q] ⧸ Q.under ℤ_[q]) := by
    rw [hP]
    exact Finite.of_equiv _ (PadicInt.residueField (p := q)).toEquiv.symm
  have hcard : Nat.card (ℤ_[q] ⧸ Q.under ℤ_[q]) = q := by
    rw [Nat.card_congr ((Ideal.quotEquivOfEq hP).toEquiv.trans (PadicInt.residueField (p := q)).toEquiv), Nat.card_zmod]
  obtain ⟨σ, hσ⟩ := IsArithFrobAt.exists_of_isInvariant_of_profinite ℤ_[q] (GG q) Q
  refine ⟨σ, fun x => ?_⟩
  have hx := hσ x
  rw [hcard] at hx
  exact ValuationSubring.coe_mem_nonunits_iff.mpr hx

end Local

theorem mem_nonunits_comap {K L : Type*} [Field K] [Field L] {B : ValuationSubring L} {f : K →+* L} {x : K} :
    x ∈ (B.comap f).nonunits ↔ f x ∈ B.nonunits := by
  rw [ValuationSubring.mem_nonunits_iff_or, ValuationSubring.mem_nonunits_iff_or, ValuationSubring.mem_comap, map_inv₀]
  constructor
  · rintro (rfl | h)
    · exact Or.inl (map_zero f)
    · exact Or.inr h
  · rintro (h | h)
    · exact Or.inl ((map_eq_zero f).mp h)
    · exact Or.inr h

theorem mem_nonunits_padicPlace_iff (q : ℕ) [Fact q.Prime] {x : AlgebraicClosure ℚ} :
    x ∈ (padicPlace q).nonunits ↔ padicEmbedding q x ∈ (padicIntegers q).nonunits := by
  rw [padicPlace, mem_nonunits_comap]
  rfl

theorem coe_decomp_smul {K L : Type*} [Field K] [Field L] [Algebra K L] (A : ValuationSubring L)
    (d : A.decompositionSubgroup K) (a : A) : ((d • a : A) : L) = (d : L ≃ₐ[K] L) a := rfl

section LevelW

variable (q : ℕ) [Fact q.Prime]
variable (Kw : IntermediateField ℚ_[q] (PadicAlgCl q)) [FiniteDimensional ℚ_[q] Kw]

noncomputable abbrev Rw : ValuationSubring Kw := (padicIntegers q).comap (algebraMap Kw (PadicAlgCl q))

noncomputable abbrev Gw : Subgroup (GG q) := Kw.fixingSubgroup

noncomputable def RwToOO : Rw q Kw →+* OO q :=
  ((algebraMap Kw (PadicAlgCl q)).comp (Rw q Kw).subtype).codRestrict (padicIntegers q) (fun x => x.2)

noncomputable instance algRwOO : Algebra (Rw q Kw) (OO q) := (RwToOO q Kw).toAlgebra

theorem algebraMap_Rw_coe (x : Rw q Kw) :
    ((algebraMap (Rw q Kw) (OO q) x : OO q) : PadicAlgCl q) = ((x : Kw) : PadicAlgCl q) := rfl

instance smulCommRw : SMulCommClass (Gw q Kw) (Rw q Kw) (OO q) where
  smul_comm g r x := by
    apply Subtype.ext
    rw [Algebra.smul_def, Algebra.smul_def]
    change (g : GG q) ((algebraMap (Rw q Kw) (OO q) r : PadicAlgCl q) * (x : PadicAlgCl q))
      = (algebraMap (Rw q Kw) (OO q) r : PadicAlgCl q) * (g : GG q) (x : PadicAlgCl q)
    rw [map_mul, algebraMap_Rw_coe]
    congr 1
    exact (IntermediateField.mem_fixingSubgroup_iff Kw (g : GG q)).mp g.2 _ (r : Kw).2

instance isInvariantRw : Algebra.IsInvariant (Rw q Kw) (OO q) (Gw q Kw) where
  isInvariant b hb := by
    haveI : IsGalois ℚ_[q] (PadicAlgCl q) := IsAlgClosure.isGalois ℚ_[q] (PadicAlgCl q)
    have hb' : (b : PadicAlgCl q) ∈ IntermediateField.fixedField (Gw q Kw) := by
      rw [IntermediateField.mem_fixedField_iff]
      intro g hg
      exact congrArg Subtype.val (hb ⟨g, hg⟩)
    rw [InfiniteGalois.fixedField_fixingSubgroup] at hb'
    refine ⟨⟨⟨(b : PadicAlgCl q), hb'⟩, ?_⟩, Subtype.ext rfl⟩
    show algebraMap Kw (PadicAlgCl q) ⟨(b : PadicAlgCl q), hb'⟩ ∈ padicIntegers q
    exact b.2

instance csdRw : ContinuousSMulDiscrete (Gw q Kw) (OO q) := by
  rw [continuousSMulDiscrete_iff_isOpen_stabilizer]
  intro x
  have : (MulAction.stabilizer (Gw q Kw) x : Set (Gw q Kw))
      = Subtype.val ⁻¹' (MulAction.stabilizer (GG q) x : Set (GG q)) := by
    ext g
    simp only [SetLike.mem_coe, MulAction.mem_stabilizer_iff, Set.mem_preimage]
    rfl
  rw [this]
  exact (ContinuousSMulDiscrete.isOpen_stabilizer (GG q) x).preimage continuous_subtype_val

instance compactGw : CompactSpace (Gw q Kw) :=
  isCompact_iff_compactSpace.mp (Kw.fixingSubgroup_isClosed.isCompact)

theorem stabilizerHom_surjective_Gw :
    Function.Surjective (Ideal.Quotient.stabilizerHom (IsLocalRing.maximalIdeal (OO q))
      ((IsLocalRing.maximalIdeal (OO q)).under (Rw q Kw)) (Gw q Kw)) := by
  haveI : Algebra.IsIntegral ℚ_[q] (PadicAlgCl q) := ⟨fun x => (Algebra.IsAlgebraic.isAlgebraic x).isIntegral⟩
  letI : TopologicalSpace (OO q) := ⊥
  haveI : DiscreteTopology (OO q) := ⟨rfl⟩
  exact Ideal.Quotient.stabilizerHom_surjective_of_profinite (G := Gw q Kw)
    ((IsLocalRing.maximalIdeal (OO q)).under (Rw q Kw)) (IsLocalRing.maximalIdeal (OO q))

end LevelW

section Residues

variable (q : ℕ) [Fact q.Prime]

abbrev kbar : Type := IsLocalRing.ResidueField (OO q)

theorem natCast_residue_eq_zero : ((q : ℕ) : kbar q) = 0 := by
  rw [← map_natCast (IsLocalRing.residue (OO q)), IsLocalRing.residue_eq_zero_iff]
  rw [← ValuationSubring.coe_mem_nonunits_iff]
  have : (((q : ℕ) : OO q) : PadicAlgCl q) = ((q : ℕ) : PadicAlgCl q) := by simp
  rw [this]
  exact natCast_mem_nonunits q

instance charP_kbar : CharP (kbar q) q :=
  (CharP.charP_iff_prime_eq_zero (Fact.out : q.Prime)).mpr (natCast_residue_eq_zero q)

noncomputable instance algZModKbar : Algebra (ZMod q) (kbar q) := ZMod.algebra (kbar q) q

theorem algebraMap_toZMod (z : ℤ_[q]) :
    algebraMap (ZMod q) (kbar q) (PadicInt.toZMod z) = IsLocalRing.residue (OO q) (algebraMap ℤ_[q] (OO q) z) := by
  have hspec := PadicInt.toZMod_spec z
  rw [PadicInt.maximalIdeal_eq_span_p, Ideal.mem_span_singleton] at hspec
  obtain ⟨w, hw⟩ := hspec
  have hz : z = (ZMod.cast (PadicInt.toZMod z) : ℤ_[q]) + (q : ℤ_[q]) * w := by rw [← hw]; ring
  conv_rhs => rw [hz]
  rw [map_add, map_add, map_mul, map_mul, map_natCast, map_natCast, natCast_residue_eq_zero, zero_mul, add_zero,
    ZMod.cast_eq_val, map_natCast, map_natCast]
  change ZMod.cast (PadicInt.toZMod z) = ((PadicInt.toZMod z).val : kbar q)
  rw [ZMod.cast_eq_val]

noncomputable def kM (M : ℕ) : IntermediateField (ZMod q) (kbar q) where
  carrier := {y | y ^ (q ^ M) = y}
  mul_mem' {a b} ha hb := by
    simp only [Set.mem_setOf_eq] at ha hb ⊢
    rw [mul_pow, ha, hb]
  one_mem' := by simp only [Set.mem_setOf_eq, one_pow]
  add_mem' {a b} ha hb := by
    simp only [Set.mem_setOf_eq] at ha hb ⊢
    rw [add_pow_char_pow, ha, hb]
  zero_mem' := by
    simp only [Set.mem_setOf_eq]
    exact zero_pow (pow_ne_zero _ (Fact.out : q.Prime).ne_zero)
  algebraMap_mem' a := by
    simp only [Set.mem_setOf_eq]
    rw [← map_pow, ZMod.pow_card_pow]
  inv_mem' a ha := by
    simp only [Set.mem_setOf_eq] at ha ⊢
    rw [inv_pow, ha]

theorem mem_kM_iff {M : ℕ} {y : kbar q} : y ∈ kM q M ↔ y ^ (q ^ M) = y := Iff.rfl

theorem finite_kM (M : ℕ) (hM : 0 < M) : Finite (kM q M) := by
  classical
  have h1 : 1 < q ^ M := Nat.one_lt_pow hM.ne' (Fact.out : q.Prime).one_lt
  · have hne : (Polynomial.X ^ (q ^ M) - Polynomial.X : Polynomial (kbar q)) ≠ 0 :=
      FiniteField.X_pow_card_sub_X_ne_zero (kbar q) h1
    have hsub : ((kM q M) : Set (kbar q)) ⊆ ((Polynomial.X ^ (q ^ M) - Polynomial.X : Polynomial (kbar q)).roots.toFinset : Set (kbar q)) := by
      intro y hy
      rw [SetLike.mem_coe, mem_kM_iff] at hy
      simp only [Finset.mem_coe, Multiset.mem_toFinset, Polynomial.mem_roots hne, Polynomial.IsRoot.def,
        Polynomial.eval_sub, Polynomial.eval_pow, Polynomial.eval_X, hy, sub_self]
    exact Set.Finite.to_subtype (Set.Finite.subset (Finset.finite_toSet _) hsub)

noncomputable def resAut (M : ℕ) (g : GG q) : (kM q M) ≃ₐ[ZMod q] (kM q M) where
  toFun y := ⟨g • (y : kbar q), by
    have hy := y.2; rw [mem_kM_iff] at hy ⊢; rw [← smul_pow', hy]⟩
  invFun y := ⟨g⁻¹ • (y : kbar q), by
    have hy := y.2; rw [mem_kM_iff] at hy ⊢; rw [← smul_pow', hy]⟩
  left_inv y := Subtype.ext (inv_smul_smul g (y : kbar q))
  right_inv y := Subtype.ext (smul_inv_smul g (y : kbar q))
  map_mul' a b := Subtype.ext (smul_mul' g (a : kbar q) (b : kbar q))
  map_add' a b := Subtype.ext (smul_add g (a : kbar q) (b : kbar q))
  commutes' a := Subtype.ext (by
    change g • (algebraMap (ZMod q) (kbar q) a) = algebraMap (ZMod q) (kbar q) a
    have : algebraMap (ZMod q) (kbar q) a = ((a.val : ℕ) : kbar q) := by
      change ZMod.cast a = _; rw [ZMod.cast_eq_val]
    rw [this]
    exact map_natCast (MulSemiringAction.toRingHom (GG q) (kbar q) g) a.val)

theorem coe_resAut (M : ℕ) (g : GG q) (y : kM q M) : ((resAut q M g y : kM q M) : kbar q) = g • (y : kbar q) := rfl

theorem exists_smul_eq_pow (M : ℕ) (hM : 0 < M) (g : GG q) :
    ∃ n : ℕ, ∀ y : kbar q, y ∈ kM q M → g • y = y ^ (q ^ n) := by
  haveI : Finite (kM q M) := finite_kM q M hM
  haveI : Algebra.IsAlgebraic (ZMod q) (kM q M) := Algebra.IsAlgebraic.of_finite (ZMod q) (kM q M)
  obtain ⟨n, hn⟩ := (FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow (ZMod q) (kM q M)).2 (resAut q M g)
  refine ⟨n, fun y hy => ?_⟩
  have := congrArg (fun e : (kM q M) ≃ₐ[ZMod q] (kM q M) => ((e ⟨y, hy⟩ : kM q M) : kbar q)) hn
  simp only [coe_resAut] at this
  rw [← this, AlgEquiv.coe_pow, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate, ZMod.card]
  rfl

theorem pow_pow_mul_eq {R : Type*} [Monoid R] {x : R} {a : ℕ} (h : x ^ (q ^ a) = x) (b : ℕ) : x ^ (q ^ (a * b)) = x := by
  induction b with
  | zero => simp
  | succ b ih => rw [Nat.mul_succ, pow_add, pow_mul, ih, h]

end Residues

section DegreeBound

variable (q : ℕ) [Fact q.Prime]
variable (Kw : IntermediateField ℚ_[q] (PadicAlgCl q)) [FiniteDimensional ℚ_[q] Kw]

theorem exists_monic_lift (x : Kw) (hx : x ∈ Rw q Kw) :
    ∃ P : Polynomial ℤ_[q], P.Monic ∧ P.map PadicInt.Coe.ringHom = minpoly ℚ_[q] x := by
  have hint : IsIntegral ℚ_[q] x := IsIntegral.of_finite ℚ_[q] x
  have hx1 : spectralNorm ℚ_[q] (PadicAlgCl q) (x : PadicAlgCl q) ≤ 1 := by
    have : ‖(x : PadicAlgCl q)‖₊ ≤ 1 := (mem_padicIntegers_iff q).mp hx
    have h' : ‖(x : PadicAlgCl q)‖ ≤ 1 := by exact_mod_cast this
    exact h'
  have hmin : minpoly ℚ_[q] (x : PadicAlgCl q) = minpoly ℚ_[q] x :=
    minpoly.algebraMap_eq (algebraMap Kw (PadicAlgCl q)).injective x
  have hlifts : minpoly ℚ_[q] x ∈ Polynomial.lifts (PadicInt.Coe.ringHom (p := q)) := by
    refine (Polynomial.lifts_iff_coeff_lifts _).mpr fun i => ?_
    have hci : ‖(minpoly ℚ_[q] x).coeff i‖ ≤ 1 := by
      rw [← hmin]
      have := (ciSup_le_iff (spectralValueTerms_bddAbove (minpoly ℚ_[q] (x : PadicAlgCl q)))).mp hx1 i
      simp only [spectralValueTerms] at this
      split_ifs at this with h
      · conv_rhs at this => rw [← Real.one_rpow (1 / (↑(minpoly ℚ_[q] (x : PadicAlgCl q)).natDegree - ↑i) : ℝ)]
        rw [Real.rpow_le_rpow_iff (by positivity) (by positivity) (by
          rw [one_div_pos, sub_pos]; exact_mod_cast h)] at this
        exact this
      · obtain h | h := (le_of_not_gt h).eq_or_lt
        · have hmon' : (minpoly ℚ_[q] (x : PadicAlgCl q)).Monic := by rw [hmin]; exact minpoly.monic hint
          rw [← h, hmon'.coeff_natDegree, norm_one]
        · rw [Polynomial.coeff_eq_zero_of_natDegree_lt h, norm_zero]; exact zero_le_one
    exact ⟨⟨_, hci⟩, rfl⟩
  obtain ⟨P, hP, -, hmon⟩ := Polynomial.lifts_and_degree_eq_and_monic hlifts (minpoly.monic hint)
  exact ⟨P, hmon, hP⟩

theorem residue_mem_kM (x : Rw q Kw) :
    IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x) ∈ kM q (Module.finrank ℚ_[q] Kw).factorial := by
  classical
  obtain ⟨P, hmon, hP⟩ := exists_monic_lift q Kw (x : Kw) x.2
  set X : OO q := algebraMap (Rw q Kw) (OO q) x with hXdef
  set xb : kbar q := IsLocalRing.residue (OO q) X with hxbdef

  have h1 : Polynomial.eval₂ (algebraMap ℤ_[q] (OO q)) X P = 0 := by
    apply Subtype.val_injective
    rw [show ((Polynomial.eval₂ (algebraMap ℤ_[q] (OO q)) X P : OO q) : PadicAlgCl q)
        = Polynomial.eval₂ ((padicIntegers q).subtype.comp (algebraMap ℤ_[q] (OO q))) (X : PadicAlgCl q) P from
        Polynomial.hom_eval₂ P (algebraMap ℤ_[q] (OO q)) (padicIntegers q).subtype X]
    have hcomp : (padicIntegers q).subtype.comp (algebraMap ℤ_[q] (OO q))
        = (algebraMap ℚ_[q] (PadicAlgCl q)).comp PadicInt.Coe.ringHom := by
      ext z; rfl
    rw [hcomp, ← Polynomial.eval₂_map, hP, ZeroMemClass.coe_zero]
    change Polynomial.eval₂ (algebraMap ℚ_[q] (PadicAlgCl q)) (algebraMap Kw (PadicAlgCl q) (x : Kw)) (minpoly ℚ_[q] (x : Kw)) = 0
    rw [← Polynomial.aeval_def, Polynomial.aeval_algebraMap_apply, minpoly.aeval, map_zero]

  set Pb : Polynomial (ZMod q) := P.map (PadicInt.toZMod (p := q)) with hPbdef
  have h2 : Polynomial.aeval xb Pb = 0 := by
    rw [Polynomial.aeval_def, hPbdef, Polynomial.eval₂_map]
    have hcomp : (algebraMap (ZMod q) (kbar q)).comp (PadicInt.toZMod (p := q))
        = (IsLocalRing.residue (OO q)).comp (algebraMap ℤ_[q] (OO q)) := by
      ext z; exact algebraMap_toZMod q z
    rw [hcomp, hxbdef, ← Polynomial.hom_eval₂, h1, map_zero]
  have hPbmon : Pb.Monic := hmon.map _
  have hPbdeg : Pb.natDegree ≤ Module.finrank ℚ_[q] Kw := by
    rw [hPbdef, hmon.natDegree_map]
    have : P.natDegree = (minpoly ℚ_[q] (x : Kw)).natDegree := by rw [← hP, hmon.natDegree_map]
    rw [this]
    exact minpoly.natDegree_le (x : Kw)

  have hxbint : IsIntegral (ZMod q) xb := ⟨Pb, hPbmon, h2⟩
  let E := IntermediateField.adjoin (ZMod q) ({xb} : Set (kbar q))
  haveI : FiniteDimensional (ZMod q) E := IntermediateField.adjoin.finiteDimensional hxbint
  have hd : Module.finrank (ZMod q) E ≤ Module.finrank ℚ_[q] Kw := by
    rw [IntermediateField.adjoin.finrank hxbint]
    exact (Polynomial.natDegree_le_natDegree (minpoly.min (ZMod q) xb hPbmon h2)).trans hPbdeg
  have hdpos : 0 < Module.finrank (ZMod q) E := Module.finrank_pos
  haveI : Finite E := Module.finite_of_finite (ZMod q)
  letI : Fintype E := Fintype.ofFinite E
  have hcard : Fintype.card E = q ^ Module.finrank (ZMod q) E := by
    rw [Module.card_eq_pow_finrank (K := ZMod q) (V := E), ZMod.card]
  have hfermat : xb ^ (q ^ Module.finrank (ZMod q) E) = xb := by
    have := FiniteField.pow_card (⟨xb, IntermediateField.mem_adjoin_simple_self (ZMod q) xb⟩ : E)
    rw [hcard] at this
    exact congrArg Subtype.val this

  rw [mem_kM_iff]
  obtain ⟨c, hc⟩ := Nat.dvd_factorial hdpos hd
  rw [hc]
  exact pow_pow_mul_eq q hfermat c

end DegreeBound

section Transport

variable (q : ℕ) [Fact q.Prime]

noncomputable abbrev rD : GG q →* ↥((padicPlace q).decompositionSubgroup ℚ) :=
  (localGaloisToGlobal q).codRestrict _ (localGaloisToGlobal_mem_decompositionSubgroup q)

theorem rD_smul_residue_eq_pow (w : GG q) (e : ℕ)
    (hw : ∀ x : OO q, ((w • x - x ^ e : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits)
    (a : ↥(padicPlace q)) :
    rD q w • IsLocalRing.residue _ a = (IsLocalRing.residue _ a) ^ e := by
  rw [← map_pow, ← IsLocalRing.ResidueField.residue_smul, ← sub_eq_zero, ← map_sub, IsLocalRing.residue_eq_zero_iff,
    ← ValuationSubring.coe_mem_nonunits_iff, mem_nonunits_padicPlace_iff]
  let x : OO q := ⟨padicEmbedding q (a : AlgebraicClosure ℚ), a.2⟩
  have key := hw x
  have hcoe : padicEmbedding q (((rD q w • a - a ^ e : ↥(padicPlace q))) : AlgebraicClosure ℚ)
      = ((w • x - x ^ e : OO q) : PadicAlgCl q) := by
    simp only [AddSubgroupClass.coe_sub, SubmonoidClass.coe_pow, map_sub, map_pow, coe_decomp_smul, coe_smul_OO,
      MonoidHom.codRestrict_apply, padicEmbedding_localGaloisToGlobal, x]
  rw [hcoe]
  exact key

theorem isFrobeniusAt_of_local (σ : GG q)
    (hσ : ∀ x : OO q, ((σ • x - x ^ q : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits) :
    (padicPlace q).IsFrobeniusAt (localGaloisToGlobal q σ) q :=
  ⟨localGaloisToGlobal_mem_decompositionSubgroup q σ, fun y => by
    obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective y
    exact rD_smul_residue_eq_pow q σ q hσ a⟩

theorem rD_pow_smul (ψ : GG q) (hψ : (padicPlace q).IsFrobeniusAt (localGaloisToGlobal q ψ) q)
    (k : ℕ) (y : IsLocalRing.ResidueField ↥(padicPlace q)) : rD q (ψ ^ k) • y = y ^ (q ^ k) := by
  induction k generalizing y with
  | zero => rw [pow_zero, map_one, one_smul, pow_zero, pow_one]
  | succ k ih =>
    rw [pow_succ, map_mul, mul_smul, (show rD q ψ • y = y ^ q from hψ.smul_residue_eq y), smul_pow', ih, ← pow_mul, ← pow_succ]

theorem mem_inertiaPullback_iff_nat (g : GG q) :
    g ∈ ((padicPlace q).inertiaSubgroupIn ℚ).comap (localGaloisToGlobal q) ↔
      ∀ x : IsLocalRing.ResidueField ↥(padicPlace q), rD q g • x = x := by
  rw [Subgroup.mem_comap, ValuationSubring.inertiaSubgroupIn, Subgroup.mem_map]
  constructor
  · rintro ⟨τ, hτ, hτg⟩
    intro x
    have hmem : rD q g = τ := by
      apply Subtype.ext; exact hτg.symm
    rw [hmem]
    rw [ValuationSubring.inertiaSubgroup, MonoidHom.mem_ker] at hτ
    have := congrArg (fun φ => (φ : IsLocalRing.ResidueField ↥(padicPlace q) ≃+* _) x) hτ
    simpa using this
  · intro h
    refine ⟨rD q g, ?_, rfl⟩
    rw [ValuationSubring.inertiaSubgroup, MonoidHom.mem_ker]
    apply RingEquiv.ext
    intro x
    simpa using h x

theorem pow_smul_kbar (φ₀ : GG q) (hφ₀res : ∀ z : kbar q, φ₀ • z = z ^ q) (k : ℕ) (z : kbar q) :
    (φ₀ ^ k) • z = z ^ (q ^ k) := by
  induction k generalizing z with
  | zero => rw [pow_zero, one_smul, pow_zero, pow_one]
  | succ k ih => rw [pow_succ, mul_smul, hφ₀res, smul_pow', ih, ← pow_mul, ← pow_succ]

end Transport

section ResidueMap

variable (q : ℕ) [Fact q.Prime] (Kw : IntermediateField ℚ_[q] (PadicAlgCl q))

noncomputable abbrev resw (x : Rw q Kw) : kbar q := IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x)

theorem resw_def (x : Rw q Kw) : resw q Kw x = IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x) := rfl

end ResidueMap

section Commute

variable (q : ℕ) [Fact q.Prime]

theorem exists_mem_kM (z : kbar q) : ∃ M : ℕ, 0 < M ∧ z ∈ kM q M := by
  obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective z

  have hxint : IsIntegral ℚ_[q] (x : PadicAlgCl q) := (Algebra.IsAlgebraic.isAlgebraic (x : PadicAlgCl q)).isIntegral
  let Kw : IntermediateField ℚ_[q] (PadicAlgCl q) := IntermediateField.adjoin ℚ_[q] {(x : PadicAlgCl q)}
  haveI : FiniteDimensional ℚ_[q] Kw := IntermediateField.adjoin.finiteDimensional hxint
  have hxK : (x : PadicAlgCl q) ∈ Kw := IntermediateField.mem_adjoin_simple_self ℚ_[q] _
  let xr : Rw q Kw := ⟨⟨(x : PadicAlgCl q), hxK⟩, show algebraMap Kw (PadicAlgCl q) ⟨(x : PadicAlgCl q), hxK⟩ ∈ padicIntegers q from x.2⟩
  refine ⟨(Module.finrank ℚ_[q] Kw).factorial, Nat.factorial_pos _, ?_⟩
  have := residue_mem_kM q Kw xr
  convert this using 2
  exact Subtype.ext rfl

theorem smul_smul_comm_kbar (g h : GG q) (z : kbar q) : g • (h • z) = h • (g • z) := by
  obtain ⟨M, hM, hz⟩ := exists_mem_kM q z
  obtain ⟨a, ha⟩ := exists_smul_eq_pow q M hM g
  obtain ⟨b, hb⟩ := exists_smul_eq_pow q M hM h
  have hzg : g • z ∈ kM q M := by rw [mem_kM_iff] at hz ⊢; rw [← smul_pow', hz]
  have hzh : h • z ∈ kM q M := by rw [mem_kM_iff] at hz ⊢; rw [← smul_pow', hz]
  rw [ha _ hzh, hb _ hz, hb _ hzg, ha _ hz, ← pow_mul, ← pow_mul, mul_comm]

theorem commutator_smul_sub_mem (g h : GG q) (x : OO q) :
    (((g * h * g⁻¹ * h⁻¹) • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits := by
  rw [ValuationSubring.coe_mem_nonunits_iff, ← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero, pow_one,
    IsLocalRing.ResidueField.residue_smul]
  set z := IsLocalRing.residue (OO q) x
  rw [mul_smul, mul_smul, mul_smul, smul_smul_comm_kbar q g⁻¹ h⁻¹ z, smul_inv_smul, smul_inv_smul]

end Commute

section MoveLikeFrobenius

variable (q : ℕ) [Fact q.Prime]

theorem mem_inertiaPullback_of_smul_sub_mem (w : GG q)
    (hw : ∀ x : OO q, ((w • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits) :
    w ∈ ((padicPlace q).inertiaSubgroupIn ℚ).comap (localGaloisToGlobal q) := by
  refine (mem_inertiaPullback_iff_nat q w).mpr fun y => ?_
  obtain ⟨a, rfl⟩ := IsLocalRing.residue_surjective y
  rw [rD_smul_residue_eq_pow q _ 1 hw a, pow_one]

variable (Kw : IntermediateField ℚ_[q] (PadicAlgCl q)) [FiniteDimensional ℚ_[q] Kw]

theorem apply_eq_of_trivial_on_residues (h : GG q)
    (hh : ∀ x : Rw q Kw, h • IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x)
      = IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x))
    (y : PadicAlgCl q) (hy : y ∈ Kw)
    (hI : ∀ w : GG q, (∀ x : OO q, ((w • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits) → w y = y) :
    h y = y := by
  classical
  let Q := IsLocalRing.maximalIdeal (OO q)
  let σbar : (OO q ⧸ Q) ≃ₐ[Rw q Kw ⧸ Q.under (Rw q Kw)] (OO q ⧸ Q) :=
    { MulSemiringAction.toRingEquiv (GG q) (kbar q) h with
      commutes' := fun r => by
        obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
        exact hh r }
  obtain ⟨u, hu⟩ := stabilizerHom_surjective_Gw q Kw σbar
  set uG : GG q := ((u : Gw q Kw) : GG q) with huGdef
  have hu' : ∀ bb : OO q, IsLocalRing.residue (OO q) (uG • bb) = h • IsLocalRing.residue (OO q) bb := by
    intro bb
    exact congrArg (fun e => e (Ideal.Quotient.mk Q bb)) hu

  have hw : ∀ x : OO q, (((h⁻¹ * uG) • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits := by
    intro x
    rw [ValuationSubring.coe_mem_nonunits_iff, ← IsLocalRing.residue_eq_zero_iff, map_sub, sub_eq_zero, pow_one,
      IsLocalRing.ResidueField.residue_smul, mul_smul, ← IsLocalRing.ResidueField.residue_smul, hu', inv_smul_smul]
  have hwy : (h⁻¹ * uG) y = y := hI _ hw
  have huy : uG y = y := (IntermediateField.mem_fixingSubgroup_iff Kw uG).mp u.1.2 y hy

  have : h = uG * (h⁻¹ * uG)⁻¹ := by group
  rw [this, AlgEquiv.mul_apply]
  have hw' : (h⁻¹ * uG)⁻¹ y = y := by
    rw [AlgEquiv.aut_inv, AlgEquiv.symm_apply_eq]; exact hwy.symm
  rw [hw', huy]

theorem exists_apply_eq_frob_pow_apply (φ₀ : GG q) (hφ₀res : ∀ z : kbar q, φ₀ • z = z ^ q)
    (y : PadicAlgCl q) (hy : y ∈ Kw)
    (hI : ∀ w : GG q, (∀ x : OO q, ((w • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits) → w y = y)
    (g : GG q) : ∃ j : ℕ, g y = (φ₀ ^ j) y := by
  set N : ℕ := Module.finrank ℚ_[q] Kw with hNdef
  obtain ⟨n, hn⟩ := exists_smul_eq_pow q N.factorial (Nat.factorial_pos N) g
  refine ⟨n, ?_⟩
  have hφ₀n : ∀ z : kbar q, (φ₀ ^ n) • z = z ^ (q ^ n) := pow_smul_kbar q φ₀ hφ₀res n
  have hh : ∀ x : Rw q Kw,
      ((φ₀ ^ n)⁻¹ * g) • IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x)
        = IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x) := by
    intro x
    have hx := hn _ (residue_mem_kM q Kw x)
    rw [mul_smul, hx, ← hφ₀n, inv_smul_smul]
  have := apply_eq_of_trivial_on_residues q Kw ((φ₀ ^ n)⁻¹ * g) hh y hy hI
  rw [AlgEquiv.mul_apply] at this

  rw [AlgEquiv.aut_inv, AlgEquiv.symm_apply_eq] at this
  exact this

theorem frob_pow_apply_eq (φ₀ : GG q) (j : ℕ)
    (hj : ∀ x : Rw q Kw, (φ₀ ^ j) • IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x)
      = IsLocalRing.residue (OO q) (algebraMap (Rw q Kw) (OO q) x))
    (y : PadicAlgCl q) (hy : y ∈ Kw)
    (hI : ∀ w : GG q, (∀ x : OO q, ((w • x - x ^ 1 : OO q) : PadicAlgCl q) ∈ (padicIntegers q).nonunits) → w y = y) :
    (φ₀ ^ j) y = y :=
  apply_eq_of_trivial_on_residues q Kw (φ₀ ^ j) hj y hy hI

end MoveLikeFrobenius

end ExtCitation.LocalLevel

Statements phrased using this module (45)