HenselianLiftTower.lean

1 import PaperXI.HenselianFieldLift
2 
3 /-! Completion implies the Hensel hypothesis, and the unique lifts respect
4 finite residue-field towers. Multiplicativity is not additivity. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.HenselianLiftTower
8 open IsLocalRing
9 variable {R : Type*} [CommRing R]
10 
11 /-- The Hensel property is derived for a maximal-ideal-adically complete local ring. -/
12 theorem henselian_of_complete [IsLocalRing R] [IsAdicComplete (maximalIdeal R) R] : HenselianLocalRing R := by
13   constructor
14   intro f hf a ha hd
15   have HH := (inferInstance : HenselianRing R (maximalIdeal R))
16   obtain ⟨b,hb,hba⟩ := HH.is_henselian f hf a ha (hd.map (Ideal.Quotient.mk _))
17   exact ⟨b,hb,hba⟩
18 
19 variable (k k' : Type*) [Field k] [Fintype k] [Field k'] [Fintype k']
20   [Algebra k k'] [HenselianLocalRing R]
21 variable (e : k' →+* ResidueField R)
22 
23 /-- A root of X^q-X is also a root of X^(q^n)-X. -/
24 theorem root_power_tower {S : Type*} [Monoid S] {a : S} {q : ℕ}
25     (h : a^q=a) (n : ℕ) : a^(q^n)=a := by
26   induction n with
27   | zero => simp
28   | succ n ih => rw [pow_succ, pow_mul, ih, h]
29 
30 /-- The actual finite-field size law, rather than a supplied equality of exponents,
31 proves compatibility of the two Hensel sections. -/
32 theorem lift_tower (x : k) :
33     HenselianResidueLift.lift k' R e (algebraMap k k' x) =
34       HenselianResidueLift.lift k R (e.comp (algebraMap k k')) x := by
35   apply HenselianResidueLift.unique_lift k' R e
36   · exact HenselianResidueLift.lift_pow k' R e _
37   · rw [Module.card_eq_pow_finrank (K := k) (V := k')]
38     exact root_power_tower (HenselianResidueLift.lift_pow k R _ x) _
39   · simp
40 
41 omit [Algebra k k'] in
42 /-- A change of the finite field presentation changes no lifted value. -/
43 theorem lift_equiv (a : k ≃+* k') (x : k) :
44     HenselianResidueLift.lift k' R e (a x) =
45       HenselianResidueLift.lift k R (e.comp a.toRingHom) x := by
46   apply HenselianResidueLift.unique_lift k' R e
47   · exact HenselianResidueLift.lift_pow k' R e _
48   · rw [Fintype.card_congr a.toEquiv.symm]
49     exact HenselianResidueLift.lift_pow k R _ x
50   · simp
51 
52 section Valuation
53 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
54   (A : ValuationSubring L) [HenselianLocalRing A]
55   (eA : k' →+* ResidueField A)
56 
57 /-- The concrete generated intermediate fields are nested along finite residue extensions. -/
58 theorem field_tower :
59     HenselianFieldLift.field k K A (eA.comp (algebraMap k k')) ≤
60       HenselianFieldLift.field k' K A eA := by
61   apply IntermediateField.adjoin_le_iff.mpr
62   rintro x ⟨a, rfl⟩
63   have h := congrArg (fun z : A => (z : L)) (lift_tower k k' eA a)
64   change HenselianFieldLift.element k A (eA.comp (algebraMap k k')) a ∈ _
65   change HenselianFieldLift.element k' A eA (algebraMap k k' a) =
66     HenselianFieldLift.element k A (eA.comp (algebraMap k k')) a at h
67   rw [← h]
68   exact HenselianFieldLift.element_mem k' K A eA _
69 
70 end Valuation
71 end PaperXI.HenselianLiftTower

Back to source controls