RestrictionEmbeddingConjugacy.lean

1 import PaperX.AbsoluteGaloisRestriction
2 import Mathlib.FieldTheory.Galois.Infinite
3 
4 /-! Comparison between restriction along the chosen embedding of a normal
5 extension and canonical restriction to a normal subfield of Qbar. The two
6 restriction maps differ by one fixed inner automorphism of the subfield's
7 Galois group, so their conjugacy coverage conditions agree. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.RestrictionEmbeddingConjugacy
11 
12 abbrev Qbar := AlgebraicClosure ℚ
13 abbrev GQ := Gal(Qbar/ℚ)
14 
15 variable (L : IntermediateField ℚ Qbar) [Normal ℚ L]
16 
17 /-- A chosen embedding of a normal subfield differs from its inclusion by an
18 actual automorphism of that subfield. -/
19 def embeddingAutomorphism : Gal(L/ℚ) :=
20   (AbsoluteGaloisRestriction.embedding L).restrictNormal' L
21 
22 theorem embeddingAutomorphism_commutes (x : L) :
23     algebraMap L Qbar (embeddingAutomorphism L x) =
24       AbsoluteGaloisRestriction.embedding L x := by
25   exact (AbsoluteGaloisRestriction.embedding L).restrictNormal_commutes L x
26 
27 /-- Chosen and canonical restriction are intertwined by the fixed comparison
28 automorphism of the normal subfield. -/
29 theorem restriction_intertwines (σ : GQ) :
30     embeddingAutomorphism L * AbsoluteGaloisRestriction.restriction L σ =
31       AlgEquiv.restrictNormalHom L σ * embeddingAutomorphism L := by
32   ext x
33   change algebraMap L Qbar
34       (embeddingAutomorphism L (AbsoluteGaloisRestriction.restriction L σ x)) =
35     algebraMap L Qbar (AlgEquiv.restrictNormalHom L σ (embeddingAutomorphism L x))
36   rw [embeddingAutomorphism_commutes]
37   erw [AbsoluteGaloisRestriction.restriction_commutes]
38   change σ (AbsoluteGaloisRestriction.embedding L x) =
39     algebraMap L Qbar (σ.restrictNormal L (embeddingAutomorphism L x))
40   rw [AlgEquiv.restrictNormal_commutes, embeddingAutomorphism_commutes]
41 
42 /-- One fixed inner automorphism converts chosen restriction into canonical
43 restriction for every absolute Galois element. -/
44 theorem restriction_conjugate (σ : GQ) :
45     embeddingAutomorphism L * AbsoluteGaloisRestriction.restriction L σ *
46         (embeddingAutomorphism L)⁻¹ = AlgEquiv.restrictNormalHom L σ := by
47   rw [restriction_intertwines, mul_assoc, mul_inv_cancel, mul_one]
48 
49 /-- The two restrictions define the same conjugacy class. -/
50 theorem restriction_isConj (σ : GQ) :
51     IsConj (AbsoluteGaloisRestriction.restriction L σ)
52       (AlgEquiv.restrictNormalHom L σ) :=
53   isConj_iff.mpr ⟨embeddingAutomorphism L, restriction_conjugate L σ⟩
54 
55 end PaperX.RestrictionEmbeddingConjugacy

Back to source controls