HenselianGaloisResidue.lean

1 import PaperXI.ValuationResidueEmbedding
2 import Mathlib.FieldTheory.Galois.IsGaloisGroup
3 
4 /-! Derive residue-automorphism lifting in a finite Galois extension with invariant
5 Henselian valuation and finite residue field. No surjectivity is assumed. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.HenselianGaloisResidue
9 open IsLocalRing
10 variable (K : Type*) {L : Type*} [Field K] [Field L] [Algebra K L]
11 variable (A : ValuationSubring L)
12 variable (stable : ∀ g : L ≃ₐ[K] L, g ∈ A.decompositionSubgroup K)
13 def decompositionMap : (L ≃ₐ[K] L) →* A.decompositionSubgroup K where
14   toFun g := ⟨g, stable g⟩
15   map_one' := rfl
16   map_mul' _ _ := rfl
17 def residueAction : (L ≃ₐ[K] L) →* RingAut (ResidueField A) :=
18   (MulSemiringAction.toRingAut (A.decompositionSubgroup K) (ResidueField A)).comp
19     (decompositionMap K A stable)
20 @[simp] theorem residueAction_residue (g : L ≃ₐ[K] L) (x : A) :
21     residueAction K A stable g (residue A x) =
22       residue A ((decompositionMap K A stable g) • x) := by rfl
23 theorem fixes_base (g : L ≃ₐ[K] L)
24     (x : ResidueField (A.comap (algebraMap K L))) :
25     residueAction K A stable g
26       (ValuationResidueEmbedding.residueMap A (algebraMap K L) x) =
27       ValuationResidueEmbedding.residueMap A (algebraMap K L) x := by
28   obtain ⟨x, rfl⟩ := residue_surjective x
29   rw [ValuationResidueEmbedding.residueMap_residue, residueAction_residue]
30   congr 1
31   apply Subtype.ext
32   exact g.commutes x.val
33 variable [FiniteDimensional K L] [IsGalois K L]
34 variable [HenselianLocalRing A] [Fintype (ResidueField A)]
35 theorem fixed_iff_base (z : ResidueField A) :
36     (∀ g, residueAction K A stable g z = z) ↔
37       z ∈ Set.range (ValuationResidueEmbedding.residueMap A (algebraMap K L)) := by
38   constructor
39   · intro hz
40     let a := HenselianResidueLift.lift (ResidueField A) A (RingHom.id _) z
41     have ha : ∀ g : L ≃ₐ[K] L, g (a : L) = (a : L) := by
42       intro g
43       have hh : (decompositionMap K A stable g) • a = a := by
44         apply (HenselianResidueLift.automorphism_fix_iff (ResidueField A) A (RingHom.id _)
45           (MulSemiringAction.toRingAut (A.decompositionSubgroup K) A
46             (decompositionMap K A stable g)) z).mpr
47         change residue A ((decompositionMap K A stable g) • a) = z
48         rw [← residueAction_residue]
49         simpa only [a, HenselianResidueLift.residue_lift, RingHom.id_apply] using hz g
50       exact congrArg (fun x : A => (x : L)) hh
51     obtain ⟨b, hb⟩ := IntermediateField.mem_bot.mp ((IsGalois.mem_bot_iff_fixed (a : L)).mpr ha)
52     apply (ValuationResidueEmbedding.mem_range_iff A (algebraMap K L) z).mpr
53     refine ⟨b, hb ▸ a.property, ?_⟩
54     have he : (⟨algebraMap K L b, hb ▸ a.property⟩ : A) = a := Subtype.ext hb
55     rw [he]
56     exact HenselianResidueLift.residue_lift (ResidueField A) A (RingHom.id _) z
57   · rintro ⟨x, rfl⟩ g
58     exact fixes_base K A stable g x
59 theorem lift_automorphism (σ : RingAut (ResidueField A))
60     (hσ : ∀ x : ResidueField (A.comap (algebraMap K L)),
61       σ (ValuationResidueEmbedding.residueMap A (algebraMap K L) x) =
62         ValuationResidueEmbedding.residueMap A (algebraMap K L) x) :
63     ∃ g : L ≃ₐ[K] L, residueAction K A stable g = σ := by
64   let : MulSemiringAction (L ≃ₐ[K] L) (ResidueField A) :=
65     MulSemiringAction.compHom _ (residueAction K A stable)
66   let τ : ResidueField A ≃ₐ[FixedPoints.subfield (L ≃ₐ[K] L) (ResidueField A)]
67       ResidueField A := AlgEquiv.ofRingEquiv (f := σ) (by
68     intro x
69     obtain ⟨b, hb⟩ := (fixed_iff_base K A stable x.val).mp x.property
70     change σ x.val = x.val
71     rw [← hb]
72     exact hσ b)
73   obtain ⟨g, hg⟩ := FixedPoints.toAlgAut_surjective (L ≃ₐ[K] L) (ResidueField A) τ
74   exact ⟨g, RingEquiv.ext (fun x => AlgEquiv.congr_fun hg x)⟩
75 end PaperXI.HenselianGaloisResidue

Back to source controls