LiftedResidueFrobenius.lean

1 import PaperXI.LiftedFullResidue
2 import PaperXI.FiniteResidueBaseChange
3 
4 /-! Frobenius lifting and the exact degree quotient with the actual base residue.
5 The degree-one lift is derived from finite Galois residue surjectivity. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.LiftedResidueFrobenius
9 open IsLocalRing PaperXI.LiftedResidueDegree PaperXI.FiniteResidueBaseChange
10 open PaperXI.ResidueWeil PaperXI.ResidueDegreeBaseChange
11 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
12 variable (A : ValuationSubring L) [Fintype (ResidueField A)]
13 
14 instance baseFinite : Finite (BaseResidue K A) :=
15   Finite.of_injective (ValuationResidueEmbedding.residueMap A (algebraMap K L))
16     (ValuationResidueEmbedding.residueMap_injective A (algebraMap K L))
17 local instance baseFintype : Fintype (BaseResidue K A) := Fintype.ofFinite _
18 
19 /-- The actual inverse q-power residue automorphism, q=the full base residue size. -/
20 def frobenius : RingAut (ResidueField A) := geometric (BaseResidue K A) (ResidueField A)
21 
22 @[simp] theorem frobenius_inverse_power (x : ResidueField A) :
23     frobenius K A x ^ Fintype.card (BaseResidue K A) = x :=
24   geometric_inverse_power (BaseResidue K A) (ResidueField A) x
25 
26 variable [FiniteDimensional K L] [IsGalois K L] [HenselianLocalRing A]
27 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
28 
29 /-- A lift of geometric residue Frobenius is a theorem, not an extra input. -/
30 theorem frobenius_in_range :
31     frobenius K A ∈ (HenselianGaloisResidue.residueAction K A stable).range := by
32   obtain ⟨g, hg⟩ := residueAut_surjective K A stable
33     (FiniteField.frobeniusAlgEquivOfAlgebraic (BaseResidue K A) (ResidueField A)).symm
34   exact ⟨g, RingEquiv.ext (fun x => AlgEquiv.congr_fun hg x)⟩
35 
36 include stable in
37 /-- The same existence statement in the literal valuation decomposition subgroup. -/
38 theorem decomposition_frobenius_lift :
39     frobenius K A ∈
40       (MulSemiringAction.toRingAut (A.decompositionSubgroup K) (ResidueField A)).range := by
41   obtain ⟨g, hg⟩ := frobenius_in_range K A stable
42   exact ⟨HenselianGaloisResidue.decompositionMap K A stable g, hg⟩
43 
44 /-- No finite-order reduction of the integer degree. -/
45 theorem full_degree : Function.Surjective
46     (degree (HenselianGaloisResidue.residueAction K A stable) (frobenius K A)) :=
47   degree_surjective _ _ (frobenius_in_range K A stable)
48 
49 /-- The quotient is the actual cyclic quotient of the integer-degree pullback. -/
50 def cyclicQuotient (n : ℕ) :
51     Pullback (HenselianGaloisResidue.residueAction K A stable) (frobenius K A) ⧸
52       periodSubgroup (HenselianGaloisResidue.residueAction K A stable) (frobenius K A) n
53       ≃* Multiplicative (ZMod n) :=
54   quotientEquiv _ _ n (frobenius_in_range K A stable)
55 
56 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
57 
58 /-- Its order equals the derived lifted-field degree, with no assumed index equality. -/
59 theorem quotient_order :
60     Nat.card (Pullback (HenselianGaloisResidue.residueAction K A stable) (frobenius K A) ⧸
61       periodSubgroup (HenselianGaloisResidue.residueAction K A stable) (frobenius K A)
62         (Module.finrank (BaseResidue K A) s)) = Module.finrank K (field K A s) := by
63   have hn : NeZero (Module.finrank (BaseResidue K A) s) := ⟨Module.finrank_pos.ne'⟩
64   rw [quotient_card _ _ _ (frobenius_in_range K A stable)]
65   exact (LiftedResidueDegree.degree K A stable s).symm
66 
67 end PaperXI.LiftedResidueFrobenius

Back to source controls