ResidueExtensionRealization.lean

1 import PaperXI.UnramifiedPolynomial
2 import Mathlib.FieldTheory.PrimitiveElement
3 import Mathlib.Algebra.Polynomial.Lifts
4 
5 /-! Realization of any finite separable extension of the actual base residue field.
6 The monic lift and its ring/field are constructed; no ambient Galois extension,
7 residue embedding into an existing extension, or degree certificate is supplied. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.ResidueExtensionRealization
11 open Polynomial IsLocalRing
12 variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
13 variable (s : Type*) [Field s] [Algebra (ResidueField R) s]
14 variable [FiniteDimensional (ResidueField R) s] [Algebra.IsSeparable (ResidueField R) s]
15 
16 def residueBasis : PowerBasis (ResidueField R) s :=
17   Field.powerBasisOfFiniteOfSeparable (ResidueField R) s
18 
19 def residuePolynomial : (ResidueField R)[X] :=
20   minpoly (ResidueField R) (residueBasis R s).gen
21 
22 theorem residuePolynomial_monic : (residuePolynomial R s).Monic :=
23   minpoly.monic (residueBasis R s).isIntegral_gen
24 
25 theorem residuePolynomial_irreducible : Irreducible (residuePolynomial R s) :=
26   minpoly.irreducible (residueBasis R s).isIntegral_gen
27 
28 theorem residuePolynomial_degree :
29     (residuePolynomial R s).natDegree = Module.finrank (ResidueField R) s := by
30   rw [residuePolynomial, (residueBasis R s).natDegree_minpoly,
31     (residueBasis R s).finrank]
32 
33 theorem exists_monic_lift :
34     ∃ f : R[X], f.map (residue R) = residuePolynomial R s ∧
35       f.natDegree = Module.finrank (ResidueField R) s ∧ f.Monic := by
36   have hl : residuePolynomial R s ∈ Polynomial.lifts (residue R) :=
37     (Polynomial.mem_lifts _).mpr
38       (Polynomial.map_surjective (residue R) residue_surjective (residuePolynomial R s))
39   obtain ⟨f, hf, hd, hm⟩ :=
40     Polynomial.lifts_and_natDegree_eq_and_monic hl (residuePolynomial_monic R s)
41   exact ⟨f, hf, hd.trans (residuePolynomial_degree R s), hm⟩
42 
43 def liftedPolynomial : R[X] := (exists_monic_lift R s).choose
44 
45 theorem liftedPolynomial_map :
46     (liftedPolynomial R s).map (residue R) = residuePolynomial R s :=
47   (exists_monic_lift R s).choose_spec.1
48 
49 theorem liftedPolynomial_degree :
50     (liftedPolynomial R s).natDegree = Module.finrank (ResidueField R) s :=
51   (exists_monic_lift R s).choose_spec.2.1
52 
53 instance monic : Fact (liftedPolynomial R s).Monic :=
54   ⟨(exists_monic_lift R s).choose_spec.2.2⟩
55 
56 instance residueIrreducible :
57     Fact (Irreducible ((liftedPolynomial R s).map (residue R))) :=
58   ⟨by rw [liftedPolynomial_map]; exact residuePolynomial_irreducible R s⟩
59 
60 abbrev ring := AdjoinRoot (liftedPolynomial R s)
61 abbrev field := UnramifiedPolynomial.field (liftedPolynomial R s)
62 
63 /-- The full residue field, not merely an embedded subfield, realizes s. -/
64 def residueEquiv : ResidueField (ring R s) ≃ₐ[ResidueField R] s :=
65   (MonicResidueAlgebra.residueAlgebraEquiv (liftedPolynomial R s)).trans <|
66     (AdjoinRoot.algEquivOfEq (ResidueField R) _ _ (liftedPolynomial_map R s)).trans <|
67       AdjoinRoot.equiv' (residuePolynomial R s) (residueBasis R s)
68         (by change aeval (AdjoinRoot.root (residuePolynomial R s)) (residuePolynomial R s) = 0
69             exact AdjoinRoot.eval₂_root _)
70         (minpoly.aeval _ _)
71 
72 theorem rank :
73     Module.finrank R (ring R s) = Module.finrank (ResidueField R) s := by
74   rw [MonicResidueAlgebra.rank, liftedPolynomial_degree]
75 
76 theorem field_degree :
77     Module.finrank (FractionRing R) (field R s) = Module.finrank (ResidueField R) s := by
78   rw [UnramifiedPolynomial.field_degree, liftedPolynomial_degree]
79 
80 variable [Finite (ResidueField R)]
81 
82 theorem etale : Algebra.Etale R (ring R s) :=
83   UnramifiedPolynomial.etale (liftedPolynomial R s)
84 
85 theorem ramificationIdx_one : (maximalIdeal (ring R s)).ramificationIdx R = 1 :=
86   UnramifiedPolynomial.ramificationIdx_one (liftedPolynomial R s)
87 
88 theorem source :
89     Module.Finite R (ring R s) ∧ Module.Free R (ring R s) ∧
90     IsDiscreteValuationRing (ring R s) ∧ Algebra.Etale R (ring R s) ∧
91     Nonempty (ResidueField (ring R s) ≃ₐ[ResidueField R] s) ∧
92     Module.finrank (FractionRing R) (field R s) = Module.finrank (ResidueField R) s ∧
93     (maximalIdeal (ring R s)).ramificationIdx R = 1 :=
94   ⟨inferInstance, inferInstance, inferInstance, etale R s, ⟨residueEquiv R s⟩,
95     field_degree R s, ramificationIdx_one R s⟩
96 
97 end PaperXI.ResidueExtensionRealization

Back to source controls