AbsoluteGaloisRestriction.lean

1 import Mathlib.FieldTheory.AbsoluteGaloisGroup
2 import Mathlib.FieldTheory.Normal.Basic
3 
4 /-! Restriction from the actual absolute Galois group of Q to a normal extension,
5 using a chosen embedding into the fixed algebraic closure. Surjectivity follows
6 from extension of field automorphisms. Finite extensions give continuous maps
7 for the existing Krull topologies. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.AbsoluteGaloisRestriction
11 
12 variable (L : Type*) [Field L] [Algebra ℚ L] [Normal ℚ L]
13 
14 /-- A chosen Q-embedding into Mathlib's fixed algebraic closure of Q. -/
15 def embedding : L →ₐ[ℚ] AlgebraicClosure ℚ := IsAlgClosed.lift
16 
17 /-- Restriction along the chosen embedding, as an actual group homomorphism. -/
18 def restriction : Field.absoluteGaloisGroup ℚ →* Gal(L/ℚ) := by
19   let : Algebra L (AlgebraicClosure ℚ) := (embedding L).toAlgebra
20   exact AlgEquiv.restrictNormalHom L
21 
22 /-- The restricted automorphism acts on every embedded field element as the
23 original absolute automorphism. -/
24 theorem restriction_commutes (σ : Field.absoluteGaloisGroup ℚ) (x : L) :
25     embedding L (restriction L σ x) = (show Gal(AlgebraicClosure ℚ/ℚ) from σ) (embedding L x) := by
26   let : Algebra L (AlgebraicClosure ℚ) := (embedding L).toAlgebra
27   exact AlgEquiv.restrictNormal_commutes σ L x
28 
29 /-- Every automorphism of the normal extension extends to the algebraic closure. -/
30 theorem restriction_surjective : Function.Surjective (restriction L) := by
31   let : Algebra L (AlgebraicClosure ℚ) := (embedding L).toAlgebra
32   exact AlgEquiv.restrictNormalHom_surjective (AlgebraicClosure ℚ)
33 
34 /-- Restriction is the identity exactly when the absolute automorphism fixes
35 all elements of the chosen embedded field. -/
36 theorem restriction_eq_one_iff (σ : Field.absoluteGaloisGroup ℚ) :
37     restriction L σ = 1 ↔ ∀ x : L, (show Gal(AlgebraicClosure ℚ/ℚ) from σ) (embedding L x) = embedding L x := by
38   constructor
39   · intro h x
40     simpa [h] using (restriction_commutes L σ x).symm
41   · intro h
42     ext x
43     apply (embedding L).injective
44     exact (restriction_commutes L σ x).trans (h x)
45 
46 /-- The restriction homomorphism is continuous when the extension is finite. -/
47 theorem restriction_continuous [FiniteDimensional ℚ L] : Continuous (restriction L) := by
48   change Continuous (show Gal(AlgebraicClosure ℚ/ℚ) → Gal(L/ℚ) from restriction L)
49   let F : IntermediateField ℚ (AlgebraicClosure ℚ) := (embedding L).fieldRange
50   let : FiniteDimensional ℚ F := Module.Finite.equiv (embedding L).equivFieldRange.toLinearEquiv
51   apply continuous_of_continuousAt_one (restriction L) (continuousAt_def.mpr ?_)
52   intro N hN
53   have h1 : (1 : Gal(L/ℚ)) ∈ N := by simpa using mem_of_mem_nhds hN
54   apply mem_nhds_iff.mpr
55   refine ⟨(F.fixingSubgroup : Set Gal(AlgebraicClosure ℚ/ℚ)), ?_,
56     F.fixingSubgroup_isOpen, ?_⟩
57   · intro σ hσ
58     have heq : restriction L σ = 1 := (restriction_eq_one_iff L σ).mpr (by
59       intro x
60       exact hσ ⟨embedding L x, ⟨x, rfl⟩⟩)
61     change restriction L σ ∈ N
62     rw [heq]
63     exact h1
64   · exact F.fixingSubgroup.one_mem
65 
66 /-- The finite normal extension defines an open kernel in the actual absolute
67 Galois group, so it is a continuous finite quotient. -/
68 theorem restriction_kernel_isOpen [FiniteDimensional ℚ L] :
69     IsOpen ((restriction L).ker : Set (Field.absoluteGaloisGroup ℚ)) := by
70   exact (isOpen_discrete ({1} : Set Gal(L/ℚ))).preimage (restriction_continuous L)
71 
72 /-- Restriction packaged with its proved continuity. -/
73 def continuousRestriction [FiniteDimensional ℚ L] :
74     Field.absoluteGaloisGroup ℚ →ₜ* Gal(L/ℚ) :=
75   ⟨restriction L, restriction_continuous L⟩
76 
77 end PaperX.AbsoluteGaloisRestriction

Back to source controls