HenselianWeilAttachment.lean

1 import PaperXI.HenselianLiftTower
2 import PaperXI.ValuationFixingField
3 import PaperXI.UnramifiedValuation
4 
5 /-! Replace the previous residue stabilizer by the decomposition group over an
6 actual, constructed finite intermediate field. This does not assert its full
7 local-field unramified classification or an absolute Weil identification. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.HenselianWeilAttachment
11 open IsLocalRing PaperXI.ResidueWeil PaperXI.FiniteResidueBaseChange
12 open PaperXI.ResidueDegreeBaseChange
13 variable (k k' K : Type*) {L : Type*} [Field k] [Fintype k] [Field k'] [Fintype k']
14   [Algebra k k'] [Field K] [Field L] [Algebra K L]
15 variable (A : ValuationSubring L) [HenselianLocalRing A]
16   [Algebra k (ResidueField A)] [Algebra k' (ResidueField A)]
17   [Algebra.IsAlgebraic k (ResidueField A)] [Algebra.IsAlgebraic k' (ResidueField A)]
18 
19 abbrev liftedField := HenselianFieldLift.field k' K A (algebraMap k' (ResidueField A))
20 
21 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
22 /-- The actual field fixer equals the residue-field fixer from v0.29. -/
23 theorem field_fixing_eq :
24     HenselianFieldLift.fixing k' K A (algebraMap k' (ResidueField A)) =
25       UnramifiedValuation.fixingGroup k' K A := by
26   ext g
27   exact HenselianFieldLift.fixing_iff_residue k' K A (algebraMap k' (ResidueField A)) g
28 
29 /-- Actual decomposition group over the constructed field, not a renamed residue subgroup. -/
30 def decompositionEquiv : A.decompositionSubgroup (liftedField k' K A) ≃*
31     UnramifiedValuation.fixingGroup k' K A :=
32   (ValuationFixingField.decompositionEquiv K A (liftedField k' K A)).trans
33     (MulEquiv.subgroupCongr (field_fixing_eq k' K A))
34 
35 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
36 /-- The underlying valuation-ring automorphisms agree. -/
37 theorem ring_action (g : A.decompositionSubgroup (liftedField k' K A)) (x : A) :
38     (decompositionEquiv k' K A g).val • x = g • x := rfl
39 
40 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
41 /-- So do the actual residue actions. -/
42 theorem residue_action (g : A.decompositionSubgroup (liftedField k' K A)) (x : ResidueField A) :
43     (decompositionEquiv k' K A g).val • x = g • x := by
44   obtain ⟨a,rfl⟩ := residue_surjective x
45   rw [← ResidueField.residue_smul, ← ResidueField.residue_smul]
46   rfl
47 
48 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
49 /-- Residue action homomorphisms commute with the actual decomposition equivalence. -/
50 theorem residue_hom (g : A.decompositionSubgroup (liftedField k' K A)) :
51     ValuationConductor.residue A (UnramifiedValuation.fixingGroup k' K A)
52       (decompositionEquiv k' K A g) =
53     ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A)) g := by
54   apply RingEquiv.ext
55   exact residue_action k' K A g
56 
57 /-- Isomorphism of the two pullbacks with the same geometric residue Frobenius. -/
58 def pullbackEquiv :
59     Pullback (ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A)))
60       (geometric k' (ResidueField A)) ≃*
61     Pullback (ValuationConductor.residue A (UnramifiedValuation.fixingGroup k' K A))
62       (geometric k' (ResidueField A)) where
63   toFun w := ⟨(decompositionEquiv k' K A w.val.1, w.val.2), by
64     change ValuationConductor.residue A (UnramifiedValuation.fixingGroup k' K A)
65       (decompositionEquiv k' K A w.val.1) = _
66     rw [residue_hom]; exact w.property⟩
67   invFun w := ⟨((decompositionEquiv k' K A).symm w.val.1, w.val.2), by
68     change ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A))
69       ((decompositionEquiv k' K A).symm w.val.1) = _
70     rw [← residue_hom k' K A, (decompositionEquiv k' K A).apply_symm_apply]
71     exact w.property⟩
72   left_inv w := by
73     apply Subtype.ext
74     exact Prod.ext ((decompositionEquiv k' K A).symm_apply_apply _) rfl
75   right_inv w := by
76     apply Subtype.ext
77     exact Prod.ext ((decompositionEquiv k' K A).apply_symm_apply _) rfl
78   map_mul' a b := by
79     apply Subtype.ext
80     exact Prod.ext ((decompositionEquiv k' K A).map_mul _ _) rfl
81 
82 /-- Final source-facing bridge: an actual field-base decomposition pullback is
83 isomorphic to the original integer-degree subgroup. -/
84 def sourceEquiv :
85     Pullback (ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A)))
86       (geometric k' (ResidueField A)) ≃*
87     periodSubgroup (ValuationConductor.residue A (A.decompositionSubgroup K))
88       (geometric k (ResidueField A)) (Module.finrank k k') :=
89   (pullbackEquiv k' K A).trans (UnramifiedValuation.degreeSubgroupEquiv k k' K A)
90 
91 /-- The literal inclusion for the newly constructed field base. -/
92 def embedding :
93     Pullback (ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A)))
94       (geometric k' (ResidueField A)) →*
95     Pullback (ValuationConductor.residue A (A.decompositionSubgroup K))
96       (geometric k (ResidueField A)) :=
97   (UnramifiedValuation.embedding k k' K A).comp (pullbackEquiv k' K A).toMonoidHom
98 
99 /-- This is an actual injection, not a comparison of group cardinalities. -/
100 theorem embedding_injective : Function.Injective (embedding k k' K A) :=
101   (UnramifiedValuation.embedding_injective k k' K A).comp (pullbackEquiv k' K A).injective
102 
103 /-- Integer Frobenius degree scales by the residue-field degree. -/
104 theorem degree_formula
105     (w : Pullback (ValuationConductor.residue A (A.decompositionSubgroup (liftedField k' K A)))
106       (geometric k' (ResidueField A))) :
107     Multiplicative.toAdd (embedding k k' K A w).val.2 =
108       (Module.finrank k k' : ℤ) * Multiplicative.toAdd w.val.2 := rfl
109 
110 /-- The embedded group has exactly the required degree-divisible range. -/
111 theorem embedding_range : (embedding k k' K A).range =
112     periodSubgroup (ValuationConductor.residue A (A.decompositionSubgroup K))
113       (geometric k (ResidueField A)) (Module.finrank k k') := by
114   ext w
115   constructor
116   · rintro ⟨v,rfl⟩
117     change UnramifiedValuation.embedding k k' K A (pullbackEquiv k' K A v) ∈ _
118     rw [← UnramifiedValuation.embedding_range k k' K A]
119     exact ⟨_,rfl⟩
120   · intro h
121     rw [← UnramifiedValuation.embedding_range k k' K A] at h
122     obtain ⟨v,rfl⟩ := h
123     refine ⟨(pullbackEquiv k' K A).symm v, ?_⟩
124     change UnramifiedValuation.embedding k k' K A (pullbackEquiv k' K A
125       ((pullbackEquiv k' K A).symm v)) = _
126     rw [(pullbackEquiv k' K A).apply_symm_apply]
127 
128 omit [Algebra.IsAlgebraic k' (ResidueField A)] in
129 /-- Field fixing by a base pullback element is exactly degree divisibility. -/
130 theorem fixes_liftedField_iff
131     (w : Pullback (ValuationConductor.residue A (A.decompositionSubgroup K))
132       (geometric k (ResidueField A))) :
133     (∀ x ∈ liftedField k' K A, w.val.1.val x = x) ↔
134       (Module.finrank k k' : ℤ) ∣ Multiplicative.toAdd w.val.2 := by
135   rw [← IntermediateField.mem_fixingSubgroup_iff]
136   change w.val.1 ∈ HenselianFieldLift.fixing k' K A (algebraMap k' (ResidueField A)) ↔ _
137   rw [field_fixing_eq]
138   exact FiniteResidueSubgroup.projection_mem_iff k k' (ResidueField A) _ w
139 
140 end PaperXI.HenselianWeilAttachment

Back to source controls