Skip to content

Commit 24f997c

Browse files
AlexBrodbeltAlexBrodbelt
committed
proved reverse inclusion for the normalizer of a finite subgroup of the diagonal subgroup
1 parent 4cf3d53 commit 24f997c

2 files changed

Lines changed: 114 additions & 54 deletions

File tree

‎ClassificationOfSubgroups/Ch5_PropertiesOfSLOverAlgClosedField/S5_PropertiesOfNormalizers.lean‎

Lines changed: 109 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ universe u
1313

1414

1515
variable
16-
(F : Type u) [Field F]
16+
{F : Type u} [Field F]
1717
(n : Type u) [Fintype n]
1818
(R : Type u) [CommRing R]
1919
{G : Type u} [Group G]
@@ -76,62 +76,118 @@ lemma normalizer_subgroup_S_le_L [DecidableEq F] { S₀ : Subgroup (SL(2,F)) }
7676
-- contradiction with the assumption that Nat.card S₀ > 1
7777
linarith
7878

79-
#check mul_normal
8079
/-
8180
Proposition 1.7.
8281
(i) N_L (D₀) = ⟨D, W⟩, where D₀ is any subgroup of D with order greater than 2.
8382
-/
8483
lemma normalizer_subgroup_D_eq_DW { D₀ : Subgroup (SL(2,F)) }
85-
(hD₀ : 2 < Nat.card D₀ ) (D₀_leq_D : D₀ ≤ D F) : normalizer D₀ ≤ DW F := by
86-
intro x hx
87-
rw [mem_normalizer_iff] at hx
88-
have ⟨δ', h₀, h₁, hδ'⟩ := ex_of_card_D_gt_two hD₀ D₀_leq_D
89-
specialize hx (d δ')
90-
rw [hx] at hδ'
91-
have mem_D := D₀_leq_D hδ'
92-
rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff] at mem_D
93-
rcases get_entries x with ⟨α, β, γ, δ, hα, hβ, hγ, hδ, x_eq⟩
94-
rcases mem_D with ⟨top_right, bottom_left⟩
95-
simp [d, x_eq] at top_right bottom_left
96-
ring_nf at top_right bottom_left
97-
have top_right_eq : -(α * (δ' : F) * β) + α * β * (δ' : F)⁻¹ = α * β * ((↑δ')⁻¹ - ↑δ') := by ring
98-
have bottom_left_eq : (δ' : F) * γ * δ - (δ' : F)⁻¹ * γ * δ = γ * δ * (↑δ' - (↑δ')⁻¹) := by ring
99-
replace top_right := top_right_eq ▸ top_right
100-
replace bottom_left := bottom_left_eq ▸ bottom_left
101-
have det_eq_one : det (x : Matrix (Fin 2) (Fin 2) F) = 1 := by rw [SpecialLinearGroup.det_coe]
102-
have δ_sub_δ_inv_ne_zero : (δ' : F)⁻¹ - δ' ≠ 0 := by
103-
field_simp
104-
intro h
105-
rw [sub_eq_zero, ← sq] at h
106-
symm at h
107-
rw [sq_eq_one_iff] at h
108-
apply not_or_intro h₀ h₁ h
109-
have δ_inv_neg_δ_ne_zero : (δ') - (δ' : F)⁻¹ ≠ 0 := by
110-
rw [← neg_ne_zero, neg_sub]; exact δ_sub_δ_inv_ne_zero
111-
have α_or_β_eq_zero : α * β = 0 :=
112-
eq_zero_of_ne_zero_of_mul_right_eq_zero δ_sub_δ_inv_ne_zero top_right
113-
have γ_or_δ_eq_zero : γ * δ = 0 :=
114-
eq_zero_of_ne_zero_of_mul_right_eq_zero δ_inv_neg_δ_ne_zero bottom_left
115-
rw [mul_eq_zero] at α_or_β_eq_zero γ_or_δ_eq_zero
116-
rcases α_or_β_eq_zero with (α_eq_zero | β_eq_zero) <;>
117-
rcases γ_or_δ_eq_zero with (γ_eq_zero | δ_eq_zero)
118-
· have det_eq_zero : det (x : Matrix (Fin 2) (Fin 2) F) = 0 := by
119-
rw [det_fin_two, ← hα, ← hγ, α_eq_zero, γ_eq_zero, mul_zero, zero_mul, sub_zero]
120-
rw [det_eq_zero] at det_eq_one
121-
absurd zero_ne_one det_eq_one
122-
trivial
123-
· apply Dw_leq_DW
124-
rw [mem_D_w_iff, ← SpecialLinearGroup.fin_two_antidiagonal_iff]
125-
simp_rw [← hα, ← hδ, α_eq_zero, δ_eq_zero]
126-
trivial
127-
· apply D_leq_DW
128-
rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff]
129-
simp_rw [← hβ, ← hγ, β_eq_zero, γ_eq_zero]
130-
trivial
131-
· have det_eq_zero : det (x : Matrix (Fin 2) (Fin 2) F) = 0 := by
132-
rw [det_fin_two, ← hβ, ← hδ, β_eq_zero, δ_eq_zero, mul_zero, zero_mul, sub_zero]
133-
rw [det_eq_zero] at det_eq_one
134-
absurd zero_ne_one det_eq_one
135-
trivial
84+
(hD₀ : 2 < Nat.card D₀ ) (D₀_le_D : D₀ ≤ D F) : normalizer D₀ = DW F := by
85+
apply le_antisymm
86+
· intro x hx
87+
rw [mem_normalizer_iff] at hx
88+
have ⟨δ', h₀, h₁, hδ'⟩ := ex_of_card_D_gt_two hD₀ D₀_le_D
89+
specialize hx (d δ')
90+
rw [hx] at hδ'
91+
have mem_D := D₀_le_D hδ'
92+
rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff] at mem_D
93+
rcases get_entries x with ⟨α, β, γ, δ, hα, hβ, hγ, hδ, x_eq⟩
94+
rcases mem_D with ⟨top_right, bottom_left⟩
95+
simp [d, x_eq] at top_right bottom_left
96+
ring_nf at top_right bottom_left
97+
have top_right_eq :
98+
-(α * (δ' : F) * β) + α * β * (δ' : F)⁻¹ = α * β * ((↑δ')⁻¹ - ↑δ') := by ring
99+
have bottom_left_eq :
100+
(δ' : F) * γ * δ - (δ' : F)⁻¹ * γ * δ = γ * δ * (↑δ' - (↑δ')⁻¹) := by ring
101+
replace top_right := top_right_eq ▸ top_right
102+
replace bottom_left := bottom_left_eq ▸ bottom_left
103+
have det_eq_one : det (x : Matrix (Fin 2) (Fin 2) F) = 1 := SpecialLinearGroup.det_coe _
104+
have δ_sub_δ_inv_ne_zero : (δ' : F)⁻¹ - δ' ≠ 0 := by
105+
field_simp
106+
intro h
107+
rw [sub_eq_zero, ← sq] at h
108+
symm at h
109+
rw [sq_eq_one_iff] at h
110+
apply not_or_intro h₀ h₁ h
111+
have δ_inv_neg_δ_ne_zero : (δ') - (δ' : F)⁻¹ ≠ 0 := by
112+
rw [← neg_ne_zero, neg_sub]; exact δ_sub_δ_inv_ne_zero
113+
have α_or_β_eq_zero : α * β = 0 :=
114+
eq_zero_of_ne_zero_of_mul_right_eq_zero δ_sub_δ_inv_ne_zero top_right
115+
have γ_or_δ_eq_zero : γ * δ = 0 :=
116+
eq_zero_of_ne_zero_of_mul_right_eq_zero δ_inv_neg_δ_ne_zero bottom_left
117+
rw [mul_eq_zero] at α_or_β_eq_zero γ_or_δ_eq_zero
118+
rcases α_or_β_eq_zero with (α_eq_zero | β_eq_zero) <;>
119+
rcases γ_or_δ_eq_zero with (γ_eq_zero | δ_eq_zero)
120+
· have det_eq_zero : det (x : Matrix (Fin 2) (Fin 2) F) = 0 := by
121+
rw [det_fin_two, ← hα, ← hγ, α_eq_zero, γ_eq_zero, mul_zero, zero_mul, sub_zero]
122+
rw [det_eq_zero] at det_eq_one
123+
absurd zero_ne_one det_eq_one
124+
trivial
125+
· apply Dw_leq_DW
126+
rw [mem_D_w_iff, ← SpecialLinearGroup.fin_two_antidiagonal_iff]
127+
simp_rw [← hα, ← hδ, α_eq_zero, δ_eq_zero]
128+
trivial
129+
· apply D_leq_DW
130+
rw [mem_D_iff, ← SpecialLinearGroup.fin_two_diagonal_iff]
131+
simp_rw [← hβ, ← hγ, β_eq_zero, γ_eq_zero]
132+
trivial
133+
· have det_eq_zero : det (x : Matrix (Fin 2) (Fin 2) F) = 0 := by
134+
rw [det_fin_two, ← hβ, ← hδ, β_eq_zero, δ_eq_zero, mul_zero, zero_mul, sub_zero]
135+
rw [det_eq_zero] at det_eq_one
136+
absurd zero_ne_one det_eq_one
137+
trivial
138+
· intro x hx
139+
simp [DW] at hx
140+
rcases hx with (hx | hx)
141+
· obtain ⟨δ, rfl⟩ := hx
142+
simp [mem_normalizer_iff]
143+
intro y
144+
constructor
145+
· intro y_mem_D₀
146+
have y_mem_D := D₀_le_D y_mem_D₀
147+
rw [mem_D_iff] at y_mem_D
148+
obtain ⟨δ₀, rfl⟩ := y_mem_D
149+
simpa
150+
· intro conj_mem_D₀
151+
obtain ⟨δ₀, hδ₀⟩ := D₀_le_D conj_mem_D₀
152+
have y_eq_conj : y = d δ * y * d δ⁻¹ := by
153+
suffices y = d δ₀ by simp [this]
154+
rw [← mul_left_inj (d δ⁻¹), ← mul_right_inj (d δ)]
155+
group at hδ₀ ⊢
156+
rw [← hδ₀]
157+
simp
158+
rwa [y_eq_conj]
159+
· obtain ⟨δ, rfl⟩ := hx
160+
rw [mem_normalizer_iff]
161+
intro y
162+
constructor
163+
· intro y_mem_D₀
164+
group
165+
nth_rewrite 1 [d_eq_inv_d_inv, ← w_mul_d_eq_d_inv_w]
166+
rw [zpow_neg, zpow_neg, zpow_one, zpow_one,
167+
w_inv, mul_neg, neg_mul, inv_d_eq_d_inv,
168+
show -(w * d δ⁻¹ * y * w * d δ⁻¹) = -(w * d δ⁻¹ * y * (w * d δ⁻¹)) by group]
169+
nth_rewrite 2 [w_mul_d_eq_d_inv_w δ⁻¹]
170+
rw [← d_eq_inv_d_inv]
171+
obtain ⟨δ₀, rfl⟩ := D₀_le_D y_mem_D₀
172+
rw [show -(w * d δ⁻¹ * d δ₀ * (d δ * w)) = -(w * ((d δ⁻¹ * d δ₀) * d δ) * w) by group,
173+
d_mul_d_eq_d_mul, d_mul_d_eq_d_mul, inv_mul_cancel_comm,
174+
w_mul_d_eq_d_inv_w, inv_d_eq_d_inv]
175+
rw [show -(d δ₀⁻¹ * w * w) = -(d δ₀⁻¹ * (w * w)) by group, w_mul_w_eq_neg_one,
176+
mul_neg, mul_one, neg_d_eq_d_neg, neg_d_eq_d_neg, neg_neg, ← inv_d_eq_d_inv]
177+
exact Subgroup.inv_mem D₀ y_mem_D₀
178+
· intro conj_mem_D₀
179+
obtain ⟨δ₀, hδ₀⟩ := D₀_le_D conj_mem_D₀
180+
rw [eq_mul_inv_iff_mul_eq, ← inv_mul_eq_iff_eq_mul] at hδ₀
181+
rw [_root_.mul_inv_rev, w_inv, inv_d_eq_d_inv, ← mul_assoc (d δ₀),
182+
d_mul_d_eq_d_mul, mul_assoc, ← mul_assoc (d δ⁻¹), d_mul_d_eq_d_mul, ← mul_assoc δ⁻¹,
183+
inv_mul_cancel_comm, neg_mul, ← mul_assoc, w_mul_d_eq_d_inv_w, mul_assoc,
184+
w_mul_w_eq_neg_one, mul_neg_one, neg_neg, inv_d_eq_d_inv] at hδ₀
185+
rw [← hδ₀] at conj_mem_D₀ ⊢
186+
rw [mul_assoc, mul_assoc, ← mul_assoc w, w_mul_d_eq_d_inv_w,
187+
← d_eq_inv_d_inv, _root_.mul_inv_rev, mul_assoc, ← mul_assoc w,
188+
mul_inv_cancel, one_mul, inv_d_eq_d_inv, d_mul_d_eq_d_mul,
189+
d_mul_d_eq_d_mul, ← mul_assoc, mul_inv_cancel_comm] at conj_mem_D₀
190+
rw [← inv_d_eq_d_inv]
191+
exact Subgroup.inv_mem D₀ conj_mem_D₀
136192

137193
#min_imports

‎ClassificationOfSubgroups/Ch6_MaximalAbelianSubgroupClassEquation/S2_MaximalAbelianSubgroup.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S4_PropertiesOfCentralizers
2+
import ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S5_PropertiesOfNormalizers
23
import ClassificationOfSubgroups.Ch6_MaximalAbelianSubgroupClassEquation.S1_ElementaryAbelian
34
import Mathlib.Algebra.Order.Star.Basic
45
import Mathlib.FieldTheory.Finite.Basic
@@ -1661,7 +1662,10 @@ theorem index_normalizer_le_two {p : ℕ} [hp : Fact (Nat.Prime p)]
16611662

16621663

16631664
refine Nat.card_congr ϕ.symm
1664-
1665+
have two_lt_card_A' : 2 < Nat.card A' := by sorry
1666+
have normalizer_A'_le_DW := normalizer_subgroup_D_eq_DW two_lt_card_A' A'_le_D
1667+
have := QuotientGroup.quotientInfEquivProdNormalQuotient (H := A'.normalizer ⊓ G') (N := (D F).subgroupOf (D F).normalizer)
1668+
16651669

16661670

16671671

0 commit comments

Comments
 (0)