HenselianFieldLift.lean

1 import PaperXI.HenselianResidueLift
2 import Mathlib.RingTheory.Valuation.RamificationGroup
3 import Mathlib.FieldTheory.Galois.Basic
4 import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
5 
6 /-! Construct an actual finite intermediate field from finite residue-field
7 Hensel lifts. The fixed-field statement concerns literal automorphisms of L. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.HenselianFieldLift
11 open IsLocalRing
12 variable (k K : Type*) {L : Type*} [Field k] [Fintype k] [Field K] [Field L] [Algebra K L]
13 variable (A : ValuationSubring L) [HenselianLocalRing A]
14 variable (e : k →+* ResidueField A)
15 
16 def element (x : k) : L := (HenselianResidueLift.lift k A e x : A)
17 
18 /-- The lifted residue generators form an actual subfield of L over K. -/
19 def field : IntermediateField K L := IntermediateField.adjoin K (Set.range (element k A e))
20 
21 theorem element_mem (x : k) : element k A e x ∈ field k K A e :=
22   IntermediateField.subset_adjoin K _ ⟨x,rfl⟩
23 
24 theorem element_integral (x : k) : IsIntegral K (element k A e x) := by
25   refine ⟨Polynomial.X ^ Fintype.card k - Polynomial.X, HenselianResidueLift.poly_monic k K, ?_⟩
26   simp only [Polynomial.eval₂_sub, Polynomial.eval₂_pow, Polynomial.eval₂_X]
27   apply sub_eq_zero.mpr
28   exact congrArg (fun z : A => (z : L)) (HenselianResidueLift.lift_pow k A e x)
29 
30 /-- Finiteness is derived from a finite set of integral generators. -/
31 instance finiteDimensional : FiniteDimensional K (field k K A e) := by
32   have : Finite (Set.range (element k A e)) := Set.finite_range _
33   apply IntermediateField.finiteDimensional_adjoin
34   rintro x ⟨a, rfl⟩
35   exact element_integral k K A e a
36 
37 /-- Actual residue class of every generator. -/
38 theorem residue_element (x : k) :
39     residue A (HenselianResidueLift.lift k A e x) = e x :=
40   HenselianResidueLift.residue_lift k A e x
41 
42 /-- The true pointwise field-fixing subgroup inside the valuation decomposition group. -/
43 def fixing : Subgroup (A.decompositionSubgroup K) :=
44   (field k K A e).fixingSubgroup.comap (A.decompositionSubgroup K).subtype
45 
46 /-- Pointwise field fixing is tested on the actual lifted generators. -/
47 theorem mem_fixing_iff (g : A.decompositionSubgroup K) :
48     g ∈ fixing k K A e ↔ ∀ x : k, g.val (element k A e x) = element k A e x := by
49   change g.val ∈ (field k K A e).fixingSubgroup ↔ _
50   rw [IntermediateField.mem_fixingSubgroup_iff]
51   constructor
52   · intro h x; exact h _ (element_mem k K A e x)
53   · intro h x hx
54     apply IntermediateField.adjoin_induction (F := K) (p := fun x _ => g.val x = x)
55       (fun x hx => ?_) (fun x => g.val.commutes x)
56       (fun x y _ _ hx hy => by rw [map_add, hx, hy])
57       (fun x _ hx => by rw [map_inv₀, hx])
58       (fun x y _ _ hx hy => by rw [map_mul, hx, hy]) hx
59     obtain ⟨y, rfl⟩ := hx
60     exact h y
61 
62 /-- Hensel uniqueness identifies the field fixer with the literal residue-field fixer. -/
63 theorem fixing_iff_residue (g : A.decompositionSubgroup K) :
64     g ∈ fixing k K A e ↔ ∀ x : k, g • e x = e x := by
65   rw [mem_fixing_iff]
66   constructor
67   · intro h x
68     have hh : g • HenselianResidueLift.lift k A e x = HenselianResidueLift.lift k A e x := by
69       apply Subtype.ext
70       exact h x
71     have := congrArg (residue A) hh
72     simpa only [ResidueField.residue_smul, HenselianResidueLift.residue_lift] using this
73   · intro h x
74     have hh := (HenselianResidueLift.automorphism_fix_iff k A e
75       (MulSemiringAction.toRingAut (A.decompositionSubgroup K) A g) x).mpr (by
76         change residue A (g • HenselianResidueLift.lift k A e x) = e x
77         rw [ResidueField.residue_smul, HenselianResidueLift.residue_lift, h])
78     exact congrArg (fun z : A => (z : L)) hh
79 
80 /-- All actual inertia automorphisms fix the generated field, not just its residues. -/
81 theorem inertia_le_fixing : A.inertiaSubgroup K ≤ fixing k K A e := by
82   intro g hg
83   apply (fixing_iff_residue k K A e g).mpr
84   intro x
85   change MulSemiringAction.toRingAut (A.decompositionSubgroup K) (ResidueField A) g = 1 at hg
86   exact RingEquiv.congr_fun hg (e x)
87 
88 /-- No finite-dimensionality of L/K is required for this containment. -/
89 theorem contained_in_inertia_fixed : field k K A e ≤
90     IntermediateField.fixedField ((A.inertiaSubgroup K).map (A.decompositionSubgroup K).subtype) := by
91   apply (IntermediateField.le_iff_le _ _).mpr
92   rintro g ⟨h, hh, rfl⟩
93   exact inertia_le_fixing k K A e hh
94 
95 end PaperXI.HenselianFieldLift

Back to source controls