Skip to content

Commit c4d75f4

Browse files
xroblotxroblot
committed
1st commit
1 parent 95b694b commit c4d75f4

4 files changed

Lines changed: 223 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6288,6 +6288,7 @@ public import Mathlib.RingTheory.Ideal.Colon
62886288
public import Mathlib.RingTheory.Ideal.Cotangent
62896289
public import Mathlib.RingTheory.Ideal.CotangentBaseChange
62906290
public import Mathlib.RingTheory.Ideal.Defs
6291+
public import Mathlib.RingTheory.Ideal.Galois
62916292
public import Mathlib.RingTheory.Ideal.GoingDown
62926293
public import Mathlib.RingTheory.Ideal.GoingUp
62936294
public import Mathlib.RingTheory.Ideal.Height

‎Mathlib/FieldTheory/Normal/Defs.lean‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,6 +193,22 @@ lemma AlgEquiv.restrictNormalHom_apply (L : IntermediateField F K₁) [Normal F
193193
(σ : Gal(K₁/F)) (x : L) : restrictNormalHom L σ x = σ x :=
194194
AlgEquiv.restrictNormal_commutes σ L x
195195

196+
theorem AlgEquiv.algebraMap_restrictNormalHom_smul (x : E) (g : Gal(K₁/F)) [Normal F E] :
197+
algebraMap E K₁ (AlgEquiv.restrictNormalHom E g • x) = g • (algebraMap E K₁ x) := by
198+
rw [AlgEquiv.smul_def, AlgEquiv.smul_def]
199+
exact AlgEquiv.restrictNormal_commutes _ _ _
200+
201+
theorem AlgEquiv.algebraMap_restrictNormalHom_smul' {A B : Type*} [CommRing A] [CommRing B]
202+
[Algebra A B] [MulSemiringAction Gal(K₁/F) B] [Algebra B K₁] [SMulDistribClass Gal(K₁/F) B K₁]
203+
[FaithfulSMul B K₁] [Algebra A K₁] [IsScalarTower A B K₁] [Algebra A E] [Normal F E]
204+
[MulSemiringAction Gal(E/F) A] [SMulDistribClass Gal(E/F) A E] [IsScalarTower A E K₁] (x : A)
205+
(g : Gal(K₁/F)) :
206+
algebraMap A B (AlgEquiv.restrictNormalHom E g • x) = g • (algebraMap A B x) := by
207+
apply FaithfulSMul.algebraMap_injective B K₁
208+
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A E K₁, algebraMap.smul',
209+
algebraMap_restrictNormalHom_smul, ← IsScalarTower.algebraMap_apply, algebraMap.smul',
210+
← IsScalarTower.algebraMap_apply]
211+
196212
variable (F K₁)
197213

198214
/-- If `K₁/E/F` is a tower of fields with `E/F` normal then `AlgHom.restrictNormal'` is an

‎Mathlib/RingTheory/Ideal/Galois.lean‎

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
1+
/-
2+
Copyright (c) 2026 Xavier Roblot. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Xavier Roblot
5+
-/
6+
module
7+
8+
public import Mathlib.NumberTheory.RamificationInertia.Galois
9+
10+
/-!
11+
12+
# Galois action on ideals
13+
14+
Let `L/K` be a Galois extension and let `G = Gal(L/K)` act on a ring `B` (e.g. the ring of
15+
integers of `L`). This file collects results on the action of `G` on ideals of `B`.
16+
17+
## Main definitions
18+
19+
* `Ideal.stabilizerMapOfLiesOver`: For `F/K` a Galois subextension of `L/K`, the natural group
20+
homomorphism from the decomposition group of `P` in `Gal(L/K)` to the decomposition group
21+
of `p` in `Gal(F/K)` induced by the restriction.
22+
* `Ideal.inertiaMapOfLiesOver`: For `F/K` a Galois subextension of `L/K`, the natural group
23+
homomorphism from the inertia group of `P` in `Gal(L/K)` to the inertia group
24+
of `p` in `Gal(F/K)` induced by the restriction.
25+
26+
## Main results
27+
28+
* `Ideal.stabilizerMapOfLiesOver_surjective`: The map `stabilizerMapOfLiesOver` is surjective.
29+
* `Ideal.stabilizerMapOfLiesOver_ker`: The kernel of `stabilizerMapOfLiesOver` is the
30+
fixing subgroup of `E` intersected with the decomposition group of `P`.
31+
* `Ideal.inertiaMapOfLiesOver_surjective`: The map `inertiaMapOfLiesOver` is surjective.
32+
* `Ideal.inertiaMapOfLiesOver_ker`: The kernel of `inertiaMapOfLiesOver` is the fixing
33+
subgroup of `E` intersected with the inertia group of `P`.
34+
35+
-/
36+
37+
@[expose] public section
38+
39+
open Pointwise
40+
41+
namespace Ideal
42+
43+
open MulAction AlgEquiv
44+
45+
variable (K L : Type*) [Field K] [Field L] [Algebra K L] (F : Type*) [Field F]
46+
[Algebra K F] [Algebra F L] [IsScalarTower K F L]
47+
48+
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra B L] [Algebra A L]
49+
[Algebra A F] [FaithfulSMul B L] [IsScalarTower A B L] [IsScalarTower A F L]
50+
[MulSemiringAction Gal(L/K) B] [SMulDistribClass Gal(L/K) B L] [MulSemiringAction Gal(F/K) A]
51+
[SMulDistribClass Gal(F/K) A F]
52+
53+
variable (P : Ideal B) (p : Ideal A) [P.LiesOver p]
54+
55+
theorem restrictScalars_smul [MulSemiringAction Gal(L/F) B] [SMulDistribClass Gal(L/F) B L]
56+
(σ : Gal(L/F)) : restrictScalars K σ • P = σ • P := by
57+
ext x
58+
have : (restrictScalars K σ)⁻¹ • x = σ⁻¹ • x := by
59+
apply FaithfulSMul.algebraMap_injective B L
60+
rw [algebraMap.smul', algebraMap.smul', AlgEquiv.smul_def, AlgEquiv.smul_def, coe_inv,
61+
coe_inv, restrictScalars_symm_apply]
62+
rw [mem_pointwise_smul_iff_inv_smul_mem, mem_pointwise_smul_iff_inv_smul_mem, this]
63+
64+
variable [Normal K F]
65+
66+
theorem comap_smul_eq_restrictNormalHom_smul_comap (g : Gal(L/K)) :
67+
Ideal.comap (algebraMap A B) (g • P) =
68+
AlgEquiv.restrictNormalHom F g • Ideal.comap (algebraMap A B) P := by
69+
ext x
70+
rw [mem_comap, mem_pointwise_smul_iff_inv_smul_mem, mem_pointwise_smul_iff_inv_smul_mem,
71+
mem_comap, ← map_inv, AlgEquiv.algebraMap_restrictNormalHom_smul']
72+
73+
theorem smul_liesOver_of_restrictNormalHom_mem_stabilizer (σ : Gal(L/K))
74+
(hσ : restrictNormalHom F σ ∈ stabilizer Gal(F/K) p) :
75+
(σ • P).LiesOver p := by
76+
rw [liesOver_iff, under_def, Ideal.comap_smul_eq_restrictNormalHom_smul_comap K L F, ← under_def,
77+
← over_def P p, hσ]
78+
79+
/--
80+
The natural group homomorphism from the decomposition group of `P` in `Gal(L/K)` to the
81+
decomposition group of `p` in `Gal(F/K)`, induced by the restriction homomorphism
82+
`AlgEquiv.restrictNormalHom F : Gal(L/K) →* Gal(F/K)`.
83+
-/
84+
@[simps! apply_coe]
85+
noncomputable def stabilizerMapOfLiesOver :
86+
stabilizer Gal(L/K) P →* stabilizer Gal(F/K) p :=
87+
((AlgEquiv.restrictNormalHom F).restrict _).codRestrict _
88+
(fun ⟨g, hg⟩ ↦ by
89+
have := congr_arg (Ideal.comap (algebraMap A B)) hg
90+
rwa [comap_smul_eq_restrictNormalHom_smul_comap K L F, ← under_def, ← over_def P p] at this)
91+
92+
theorem stabilizerMapOfLiesOver_surjective [IsFractionRing A F] [IsFractionRing B L]
93+
[IsGalois F L] [IsIntegrallyClosed A] [Algebra.IsIntegral A B]
94+
[P.IsPrime] [IsGalois K L] [FiniteDimensional F L] [MulSemiringAction Gal(L/F) B]
95+
[SMulDistribClass Gal(L/F) B L] :
96+
Function.Surjective (Ideal.stabilizerMapOfLiesOver K L F P p) := by
97+
have : IsGaloisGroup Gal(L/F) A B := .of_isFractionRing _ _ _ F L
98+
intro ⟨g, hg⟩
99+
obtain ⟨σ, rfl⟩ := AlgEquiv.restrictNormalHom_surjective L g
100+
have : (σ⁻¹ • P).LiesOver p := by
101+
apply smul_liesOver_of_restrictNormalHom_mem_stabilizer K L F P p
102+
rwa [map_inv, ← Subgroup.inv_mem_iff]
103+
obtain ⟨τ, hτ⟩ := Ideal.exists_smul_eq_of_isGaloisGroup p P (σ⁻¹ • P) Gal(L/F)
104+
refine ⟨⟨σ * τ.restrictScalars K, ?_⟩, ?_⟩
105+
· rw [mem_stabilizer_iff, mul_smul, restrictScalars_smul, hτ, smul_inv_smul]
106+
· simp only [Subtype.ext_iff, stabilizerMapOfLiesOver_apply_coe, map_mul, mul_eq_left,
107+
AlgEquiv.ext_iff, one_apply]
108+
intro _
109+
apply FaithfulSMul.algebraMap_injective F L
110+
simp [restrictNormalHom]
111+
112+
set_option backward.isDefEq.respectTransparency false in
113+
theorem stabilizerMapOfLiesOver_ker (E : IntermediateField K L) [Normal K E]
114+
[Algebra A E] [MulSemiringAction Gal(E/K) A] [SMulDistribClass Gal(E/K) A E]
115+
[IsScalarTower A E L] :
116+
(Ideal.stabilizerMapOfLiesOver K L E P p).ker =
117+
E.fixingSubgroup.subgroupOf (stabilizer Gal(L/K) P) := by
118+
unfold stabilizerMapOfLiesOver
119+
rw [MonoidHom.ker_codRestrict, MonoidHom.ker_restrict, IntermediateField.restrictNormalHom_ker]
120+
121+
/--
122+
The natural group homomorphism from the inertia group of `P` in `Gal(L/K)` to the inertia group
123+
of `p` in `Gal(F/K)`, induced by the restriction homomorphism
124+
`AlgEquiv.restrictNormalHom F : Gal(L/K) →* Gal(F/K)`.
125+
-/
126+
@[simps! apply_coe]
127+
noncomputable def inertiaMapOfLiesOver :
128+
inertia Gal(L/K) P →* inertia Gal(F/K) p :=
129+
((AlgEquiv.restrictNormalHom F).restrict _).codRestrict _
130+
(fun ⟨g, hg⟩ ↦ fun x ↦ by
131+
rw [over_def P p, under_def, MonoidHom.restrict_apply, Submodule.mem_toAddSubgroup, mem_comap,
132+
map_sub, algebraMap_restrictNormalHom_smul']
133+
exact hg (algebraMap A B x))
134+
135+
attribute [instance] Ideal.Quotient.field
136+
137+
set_option backward.isDefEq.respectTransparency false in
138+
theorem inertiaMapOfLiesOver_surjective {R : Type*} [CommRing R] [IsIntegrallyClosed R]
139+
[Algebra R K] [Algebra R B] [Algebra R L] [Algebra R A] [Algebra.IsIntegral R B]
140+
[IsFractionRing R K] [IsScalarTower R A B] [IsFractionRing A F] [IsFractionRing B L]
141+
[IsScalarTower R K L] [IsScalarTower R B L] [IsGalois F L] [IsGalois K L]
142+
[IsIntegrallyClosed A] [Algebra.IsIntegral A B] (p₀ : Ideal R) [P.IsMaximal] [P.LiesOver p₀]
143+
[FiniteDimensional F L] [MulSemiringAction Gal(L/F) B] [SMulDistribClass Gal(L/F) B L] :
144+
Function.Surjective (Ideal.inertiaMapOfLiesOver K L F P p) := by
145+
have : IsGaloisGroup Gal(L/K) R B := .of_isFractionRing _ _ _ K L
146+
have : IsGaloisGroup Gal(L/F) A B := .of_isFractionRing _ _ _ F L
147+
have : p.IsMaximal := IsMaximal.of_isMaximal_liesOver P p
148+
have : p₀.IsMaximal := IsMaximal.of_isMaximal_liesOver P p₀
149+
intro ⟨g, hg⟩
150+
obtain ⟨σ, hσ⟩ := stabilizerMapOfLiesOver_surjective K L F P p ⟨g, inertia_le_stabilizer _ hg⟩
151+
have hσ' : restrictNormalHom F σ.val = g := by simpa using congr_arg Subtype.val hσ
152+
have : p.LiesOver p₀ := LiesOver.tower_bot P p p₀
153+
let σ' : Gal((B ⧸ P) / (A ⧸ p)) := by
154+
refine AlgEquiv.ofRingEquiv
155+
(f := ((IsFractionRing.stabilizerHom _ p₀ P (R ⧸ p₀) (B ⧸ P) σ)).toRingEquiv) fun q ↦ ?_
156+
refine Quotient.inductionOn' q fun x ↦ ?_
157+
have := IsFractionRing.stabilizerHom_algebraMap_mk Gal(L/K) p₀ P (R ⧸ p₀) (B ⧸ P) σ
158+
(algebraMap A B x)
159+
simp only [Algebra.algebraMap_self, RingHomCompTriple.comp_apply] at this
160+
rw [show Quotient.mk'' x = Quotient.mk p x by rfl, Quotient.algebraMap_mk_of_liesOver,
161+
coe_ringEquiv', this, Quotient.mk_eq_mk_iff_sub_mem,
162+
show σ.val • (algebraMap A B) x = algebraMap A B (g • x) by
163+
rw [← hσ', algebraMap_restrictNormalHom_smul'],
164+
← map_sub, ← Ideal.mem_comap, ← under_def, ← over_def P p]
165+
exact hg x
166+
obtain ⟨⟨τ, hτ⟩, hτ'⟩ := IsFractionRing.stabilizerHom_surjective Gal(L/F) p P (A ⧸ p) (B ⧸ P) σ'⁻¹
167+
refine ⟨⟨σ.val * τ.restrictScalars K, fun x ↦ ?_⟩, ?_⟩
168+
· suffices τ • x - σ⁻¹ • x ∈ P by
169+
rw [Submodule.mem_toAddSubgroup, ← smul_mem_pointwise_smul_iff (a := σ⁻¹), smul_sub, mul_smul,
170+
← subgroup_smul_def, inv_smul_smul]
171+
convert this using 2
172+
· exact mem_stabilizer_iff.mp <| (Subgroup.inv_mem_iff _).mpr σ.prop
173+
· apply FaithfulSMul.algebraMap_injective B L
174+
rw [algebraMap.smul', algebraMap.smul', AlgEquiv.smul_def, AlgEquiv.smul_def,
175+
restrictScalars_apply]
176+
rw [← Quotient.mk_eq_mk_iff_sub_mem]
177+
have := IsFractionRing.stabilizerHom_algebraMap_mk Gal(L/K) p₀ P (R ⧸ p₀) (B ⧸ P) σ⁻¹ x
178+
simp only [map_inv, Algebra.algebraMap_self, RingHomCompTriple.comp_apply,
179+
← subgroup_smul_def] at this
180+
rw [← this]
181+
have := IsFractionRing.stabilizerHom_algebraMap_mk Gal(L/F) p P (A ⧸ p) (B ⧸ P) ⟨τ, hτ⟩ x
182+
simp only [Algebra.algebraMap_self, RingHomCompTriple.comp_apply] at this
183+
rw [← this]
184+
exact AlgEquiv.congr_fun hτ' x
185+
· simp only [Subtype.ext_iff, inertiaMapOfLiesOver_apply_coe, map_mul, hσ', mul_eq_left,
186+
AlgEquiv.ext_iff, one_apply]
187+
intro _
188+
apply FaithfulSMul.algebraMap_injective F L
189+
simp [restrictNormalHom]
190+
191+
set_option backward.isDefEq.respectTransparency false in
192+
theorem inertiaMapOfLiesOver_ker (E : IntermediateField K L) [Normal K E] [Algebra A E]
193+
[MulSemiringAction Gal(E/K) A] [SMulDistribClass Gal(E/K) A E] [IsScalarTower A E L] :
194+
(Ideal.inertiaMapOfLiesOver K L E P p).ker =
195+
E.fixingSubgroup.subgroupOf (inertia Gal(L/K) P) := by
196+
unfold inertiaMapOfLiesOver
197+
rw [MonoidHom.ker_codRestrict, MonoidHom.ker_restrict, IntermediateField.restrictNormalHom_ker]
198+
199+
end Ideal

‎Mathlib/RingTheory/Invariant/Basic.lean‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -353,6 +353,13 @@ variable [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L]
353353
noncomputable def IsFractionRing.stabilizerHom : MulAction.stabilizer G Q →* Gal(L/K) :=
354354
MonoidHom.comp (IsFractionRing.fieldEquivOfAlgEquivHom K L) (Ideal.Quotient.stabilizerHom Q P G)
355355

356+
omit [Finite G] [Q.IsPrime] [Algebra.IsInvariant A B G] in
357+
@[simp]
358+
theorem IsFractionRing.stabilizerHom_algebraMap_mk (g : MulAction.stabilizer G Q) (x : B) :
359+
IsFractionRing.stabilizerHom G P Q K L g (algebraMap (B ⧸ Q) L x) =
360+
algebraMap (B ⧸ Q) L (g.val • x : B) := by
361+
simp [IsFractionRing.stabilizerHom, MulAction.subgroup_smul_def]
362+
356363
/-- This theorem will be made redundant by `IsFractionRing.stabilizerHom_surjective`. -/
357364
private theorem fixed_of_fixed2 (f : Gal(L/K)) (x : L)
358365
(hx : ∀ g : MulAction.stabilizer G Q, IsFractionRing.stabilizerHom G P Q K L g x = x) :

0 commit comments

Comments
 (0)