HenselianResidueLift.lean

1 import Mathlib.RingTheory.Henselian
2 import Mathlib.FieldTheory.Finite.Basic
3 import Mathlib.RingTheory.LocalRing.ResidueField.Instances
4 import Mathlib.Tactic
5 
6 /-! Unique multiplicative lifts of an embedded finite residue field. These are
7 actual Hensel roots in the given local ring, not an assumed ring section. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.HenselianResidueLift
11 open Polynomial IsLocalRing
12 variable (k R : Type*) [Field k] [Fintype k] [CommRing R] [HenselianLocalRing R]
13 variable (e : k →+* ResidueField R)
14 
15 def poly : R[X] := X ^ Fintype.card k - X
16 
17 theorem poly_monic : (poly k R).Monic := by
18   apply Polynomial.monic_X_pow_sub
19   simpa using (Fintype.one_lt_card : 1 < Fintype.card k)
20 
21 include e in
22 theorem card_residue_zero : (Fintype.card k : ResidueField R) = 0 := by
23   rw [← map_natCast e, Nat.cast_card_eq_zero, map_zero]
24 
25 include e in
26 theorem derivative_unit (a : R) : IsUnit ((poly k R).derivative.eval a) := by
27   apply (residue_ne_zero_iff_isUnit _).mp
28   simp [poly, derivative_sub, derivative_X_pow, card_residue_zero k R e]
29 
30 /-- A finite residue element has a root lift of X^Q-X. -/
31 theorem exists_lift (x : k) : ∃ a : R, a ^ Fintype.card k = a ∧ residue R a = e x := by
32   have H := ((HenselianLocalRing.TFAE R).out 1 2).mp (inferInstance : HenselianLocalRing R)
33   have hr : aeval (e x) (poly k R) = 0 := by
34     simp only [poly, map_sub, map_pow, aeval_X]
35     rw [← map_pow, FiniteField.pow_card, sub_self]
36   have hd : aeval (e x) (poly k R).derivative ≠ 0 := by
37     simp [poly, derivative_sub, derivative_X_pow, card_residue_zero k R e]
38   obtain ⟨a, ha, he⟩ := H (poly k R) (poly_monic k R) (e x) hr hd
39   exact ⟨a, by simpa [poly, Polynomial.IsRoot, sub_eq_zero] using ha, he⟩
40 
41 include e in
42 /-- A simple root lift is unique in its residue class, even with nilpotents in R. -/
43 theorem unique_lift {a b : R} (ha : a ^ Fintype.card k = a)
44     (hb : b ^ Fintype.card k = b) (hab : residue R a = residue R b) : a = b := by
45   apply IsLocalRing.eq_of_eval_eq_zero_of_not_isUnit_sub (f := poly k R)
46   · simpa [poly, sub_eq_zero] using ha
47   · simpa [poly, sub_eq_zero] using hb
48   · intro h
49     have hn := (residue_ne_zero_iff_isUnit _).mpr h
50     exact hn (by rw [map_sub, hab, sub_self])
51   · exact derivative_unit k R e a
52 
53 def lift (x : k) : R := (exists_lift k R e x).choose
54 
55 @[simp] theorem lift_pow (x : k) : lift k R e x ^ Fintype.card k = lift k R e x :=
56   (exists_lift k R e x).choose_spec.1
57 
58 @[simp] theorem residue_lift (x : k) : residue R (lift k R e x) = e x :=
59   (exists_lift k R e x).choose_spec.2
60 
61 theorem lift_injective : Function.Injective (lift k R e) := by
62   intro x y h
63   apply e.injective
64   simpa only [residue_lift] using congrArg (residue R) h
65 
66 @[simp] theorem lift_zero : lift k R e 0 = 0 := by
67   apply unique_lift k R e (lift_pow k R e 0)
68   · exact zero_pow (Fintype.card_ne_zero)
69   · simp
70 
71 @[simp] theorem lift_one : lift k R e 1 = 1 := by
72   apply unique_lift k R e (lift_pow k R e 1)
73   · exact one_pow _
74   · simp
75 
76 @[simp] theorem lift_mul (x y : k) : lift k R e (x*y) = lift k R e x * lift k R e y := by
77   apply unique_lift k R e (lift_pow k R e (x*y))
78   · rw [mul_pow, lift_pow, lift_pow]
79   · simp
80 
81 /-- Multiplicative section of the embedded residue field, not an additive section. -/
82 def sectionMonoid : k →*₀ R where
83   toFun := lift k R e
84   map_zero' := lift_zero k R e
85   map_one' := lift_one k R e
86   map_mul' := lift_mul k R e
87 
88 @[simp] theorem lift_nat_pow (x : k) (n : ℕ) : lift k R e (x^n) = lift k R e x ^ n :=
89   (sectionMonoid k R e).map_pow x n
90 
91 theorem lift_unit {x : k} (hx : x ≠ 0) : IsUnit (lift k R e x) := by
92   rw [← residue_ne_zero_iff_isUnit, residue_lift]
93   exact (map_ne_zero_iff e e.injective).mpr hx
94 
95 /-- Automorphisms fix precisely those lifts whose actual residue classes they fix. -/
96 theorem automorphism_fix_iff (σ : R ≃+* R) (x : k) :
97     σ (lift k R e x) = lift k R e x ↔ residue R (σ (lift k R e x)) = e x := by
98   constructor
99   · intro h; rw [h, residue_lift]
100   · intro h
101     apply unique_lift k R e
102     · rw [← map_pow, lift_pow]
103     · exact lift_pow k R e x
104     · rw [residue_lift]; exact h
105 
106 /-- Full transport, including nontrivial residue action. -/
107 theorem automorphism_transport (σ : R ≃+* R) {x y : k}
108     (h : residue R (σ (lift k R e x)) = e y) :
109     σ (lift k R e x) = lift k R e y := by
110   apply unique_lift k R e
111   · rw [← map_pow, lift_pow]
112   · exact lift_pow k R e y
113   · rw [residue_lift]; exact h
114 
115 end PaperXI.HenselianResidueLift

Back to source controls