LiftedResidueDegree.lean

1 import PaperXI.HenselianGaloisResidue
2 import Mathlib.FieldTheory.Finite.GaloisField
3 
4 /-! Exact degree of the Hensel-generated field in a finite Galois ambient extension.
5 The base is the full residue field of the restricted valuation. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.LiftedResidueDegree
9 open IsLocalRing
10 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
11 variable (A : ValuationSubring L)
12 
13 abbrev BaseResidue := ResidueField (A.comap (algebraMap K L))
14 
15 instance baseResidueAlgebra : Algebra (BaseResidue K A) (ResidueField A) :=
16   (ValuationResidueEmbedding.residueMap A (algebraMap K L)).toAlgebra
17 
18 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
19 
20 def residueAut : (L ≃ₐ[K] L) →* (ResidueField A ≃ₐ[BaseResidue K A] ResidueField A) where
21   toFun g := { (HenselianGaloisResidue.residueAction K A stable g) with
22     commutes' := HenselianGaloisResidue.fixes_base K A stable g }
23   map_one' := by ext x; exact RingEquiv.congr_fun (map_one (HenselianGaloisResidue.residueAction K A stable)) x
24   map_mul' g h := by ext x; exact RingEquiv.congr_fun (map_mul (HenselianGaloisResidue.residueAction K A stable) g h) x
25 
26 @[simp] theorem residueAut_apply (g : L ≃ₐ[K] L) (x : ResidueField A) :
27     residueAut K A stable g x = HenselianGaloisResidue.residueAction K A stable g x := rfl
28 
29 variable [FiniteDimensional K L] [IsGalois K L]
30 variable [HenselianLocalRing A] [Fintype (ResidueField A)]
31 
32 theorem residueAut_surjective : Function.Surjective (residueAut K A stable) := by
33   intro σ
34   obtain ⟨g, hg⟩ := HenselianGaloisResidue.lift_automorphism K A stable σ.toRingEquiv σ.commutes
35   exact ⟨g, AlgEquiv.ext (fun x => RingEquiv.congr_fun hg x)⟩
36 
37 variable (s : IntermediateField (BaseResidue K A) (ResidueField A))
38 local instance subfieldFintype : Fintype s := Fintype.ofFinite s
39 
40 /-- All lifts of the literal residue subfield s, adjoined to K. -/
41 def field : IntermediateField K L :=
42   HenselianFieldLift.field s K A s.val.toRingHom
43 
44 omit [FiniteDimensional K L] [IsGalois K L] in
45 /-- The actual fixing group is the preimage of the residue fixing group. -/
46 theorem fixingSubgroup_eq :
47     (field K A s).fixingSubgroup = s.fixingSubgroup.comap (residueAut K A stable) := by
48   ext g
49   have h := HenselianFieldLift.fixing_iff_residue s K A s.val.toRingHom
50     (HenselianGaloisResidue.decompositionMap K A stable g)
51   change g ∈ (field K A s).fixingSubgroup ↔
52     residueAut K A stable g ∈ s.fixingSubgroup
53   change (g ∈ (field K A s).fixingSubgroup) ↔
54     (∀ x : s, residueAut K A stable g x = x) at h
55   constructor
56   · intro hg
57     rw [IntermediateField.mem_fixingSubgroup_iff]
58     intro x hx
59     exact h.mp hg ⟨x, hx⟩
60   · intro hg
61     apply h.mpr
62     intro x
63     exact (IntermediateField.mem_fixingSubgroup_iff s _).mp hg x x.property
64 
65 include stable in
66 /-- The field degree is derived, rather than supplied as a certificate. -/
67 theorem degree : Module.finrank K (field K A s) = Module.finrank (BaseResidue K A) s := by
68   rw [IntermediateField.finrank_eq_fixingSubgroup_index,
69     fixingSubgroup_eq K A stable s,
70     Subgroup.index_comap_of_surjective _ (residueAut_surjective K A stable),
71     ← IntermediateField.finrank_eq_fixingSubgroup_index]
72 
73 include stable in
74 /-- The generated field is Galois, since a subextension of finite fields is normal. -/
75 theorem galois : IsGalois K (field K A s) := by
76   have hn : (field K A s).fixingSubgroup.Normal := by
77     rw [fixingSubgroup_eq K A stable s]
78     infer_instance
79   have := IsGalois.of_fixedField_normal_subgroup (field K A s).fixingSubgroup
80   rwa [IsGalois.fixedField_fixingSubgroup] at this
81 
82 end PaperXI.LiftedResidueDegree

Back to source controls