LiftedFullResidue.lean

1 import PaperXI.LiftedResidueDegree
2 
3 /-! The whole residue field of the lifted intermediate field, not merely an
4 embedded copy of the requested finite field. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperXI.LiftedFullResidue
8 open IsLocalRing PaperXI.LiftedResidueDegree
9 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
10 variable (A : ValuationSubring L) [HenselianLocalRing A] [Fintype (ResidueField A)]
11 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
12 local instance subfieldFintype : Fintype s := Fintype.ofFinite s
13 
14 /-- Restrict the valuation to the field actually constructed from Hensel roots. -/
15 def valuation : ValuationSubring (field K A s) := A.comap (field K A s).val.toRingHom
16 
17 def residueMap : ResidueField (valuation K A s) →+* ResidueField A :=
18   ValuationResidueEmbedding.residueMap A (field K A s).val.toRingHom
19 
20 /-- Every requested residue has a representative in the lifted field. -/
21 theorem residueMap_contains (x : s) :
22     (x : ResidueField A) ∈ Set.range (residueMap K A s) := by
23   let a := HenselianResidueLift.lift s A s.val.toRingHom x
24   let e : field K A s := ⟨(a : L), HenselianFieldLift.element_mem s K A s.val.toRingHom x⟩
25   let u : valuation K A s := ⟨e, a.property⟩
26   refine ⟨residue (valuation K A s) u, ?_⟩
27   exact HenselianResidueLift.residue_lift s A s.val.toRingHom x
28 
29 variable [FiniteDimensional K L] [IsGalois K L]
30 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
31 
32 include stable in
33 /-- No extra residues occur: a field element fixed by the field fixer has residue
34 fixed by the entire residue-field fixer, because residue automorphisms lift. -/
35 theorem residueMap_mem (x : ResidueField (valuation K A s)) :
36     residueMap K A s x ∈ s := by
37   suffices h : residueMap K A s x ∈ IntermediateField.fixedField s.fixingSubgroup by
38     simpa only [IsGalois.fixedField_fixingSubgroup] using h
39   rw [IntermediateField.mem_fixedField_iff]
40   intro σ hσ
41   obtain ⟨g, hg⟩ := residueAut_surjective K A stable σ
42   have hgE : g ∈ (field K A s).fixingSubgroup := by
43     rw [fixingSubgroup_eq K A stable s]
44     change residueAut K A stable g ∈ s.fixingSubgroup
45     rw [hg]; exact hσ
46   obtain ⟨u, rfl⟩ := residue_surjective x
47   let a := ValuationResidueEmbedding.inclusion A (field K A s).val.toRingHom u
48   have ha : (HenselianGaloisResidue.decompositionMap K A stable g) • a = a := by
49     apply Subtype.ext
50     exact (IntermediateField.mem_fixingSubgroup_iff (field K A s) g).mp hgE u.val u.val.property
51   change σ (residue A a) = residue A a
52   rw [← hg, residueAut_apply, HenselianGaloisResidue.residueAction_residue, ha]
53 
54 include stable in
55 /-- Exact image of the canonical residue embedding. -/
56 theorem residueMap_range : Set.range (residueMap K A s) = (s : Set (ResidueField A)) := by
57   ext x
58   constructor
59   · rintro ⟨y, rfl⟩; exact residueMap_mem K A s stable y
60   · intro hx; exact residueMap_contains K A s ⟨x, hx⟩
61 
62 /-- The canonical residue map, corestricted to the full target subfield. -/
63 def toSubfield : ResidueField (valuation K A s) →+* s where
64   toFun x := ⟨residueMap K A s x, residueMap_mem K A s stable x⟩
65   map_zero' := Subtype.ext (map_zero _)
66   map_one' := Subtype.ext (map_one _)
67   map_mul' x y := Subtype.ext (map_mul _ x y)
68   map_add' x y := Subtype.ext (map_add _ x y)
69 
70 /-- An actual residue-field isomorphism, preserving the ambient residue embedding. -/
71 def residueEquiv : ResidueField (valuation K A s) ≃+* s :=
72   RingEquiv.ofBijective (toSubfield K A s stable) ⟨(toSubfield K A s stable).injective, by
73     intro x
74     obtain ⟨y, hy⟩ := residueMap_contains K A s x
75     exact ⟨y, Subtype.ext hy⟩⟩
76 
77 @[simp] theorem residueEquiv_val (x : ResidueField (valuation K A s)) :
78     (residueEquiv K A s stable x : ResidueField A) = residueMap K A s x := rfl
79 
80 include stable in
81 theorem residue_card : Nat.card (ResidueField (valuation K A s)) = Nat.card s :=
82   Nat.card_congr (residueEquiv K A s stable).toEquiv
83 
84 /-- The base residue map is also induced by literal restriction of valuations. -/
85 def baseResidueMap : BaseResidue K A →+* ResidueField (valuation K A s) :=
86   ValuationResidueEmbedding.residueMap (valuation K A s) (algebraMap K (field K A s))
87 
88 omit [FiniteDimensional K L] [IsGalois K L] in
89 @[simp] theorem base_composition (x : BaseResidue K A) :
90     residueMap K A s (baseResidueMap K A s x) =
91       ValuationResidueEmbedding.residueMap A (algebraMap K L) x := by
92   obtain ⟨x, rfl⟩ := residue_surjective x
93   rfl
94 
95 instance actualBaseAlgebra : Algebra (BaseResidue K A) (ResidueField (valuation K A s)) :=
96   (baseResidueMap K A s).toAlgebra
97 
98 /-- Full residue identification with its actual base-field structure. -/
99 def residueAlgEquiv : ResidueField (valuation K A s) ≃ₐ[BaseResidue K A] s :=
100   { residueEquiv K A s stable with
101     commutes' := fun x => by
102       apply Subtype.ext
103       change residueMap K A s (baseResidueMap K A s x) =
104         ValuationResidueEmbedding.residueMap A (algebraMap K L) x
105       exact base_composition K A s x }
106 
107 include stable in
108 /-- Both sides now use the actual base residue, not a smaller declared subfield. -/
109 theorem residue_degree :
110     Module.finrank (BaseResidue K A) (ResidueField (valuation K A s)) =
111       Module.finrank K (field K A s) := by
112   rw [(residueAlgEquiv K A s stable).toLinearEquiv.finrank_eq]
113   exact (degree K A stable s).symm
114 
115 end PaperXI.LiftedFullResidue

Back to source controls