def IsMaximalAbelian {L : Type u_1} [Group L] (G : Subgroup L) : Prop

Equations

• IsMaximalAbelian G = Maximal Subgroup.IsCommutative G

def MaximalAbelianSubgroups {L : Type u_1} [Group L] (G : Subgroup L) : Set (Subgroup L)

Equations

• MaximalAbelianSubgroups G = {K : Subgroup L | IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G}

structure MaximalAbelian {G : Type u_1} [Group G] (H : Subgroup G) extends Subgroup G : Type u_1

• carrier : Set G
• mul_mem' {a b : G} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier
• inv_mem' {x : G} : x ∈ self.carrier → x⁻¹ ∈ self.carrier
• is_maximal' : Maximal Subgroup.IsCommutative H

def MaximalAbelianSubgroups' {L : Type u_1} [Group L] (G : Subgroup L) : Type u_1

Equations

• MaximalAbelianSubgroups' G = { K : Subgroup L // IsMaximalAbelian (K.subgroupOf G) ∧ K ≤ G }

theorem mem_centralizer_self {G : Type u_1} [Group G] (x : G) : x ∈ Subgroup.centralizer {x}

theorem inf_IsCommutative_of_IsCommutative_left {G : Type u_1} [Group G] (H K : Subgroup G) (hH : H.IsCommutative) : (H ⊓ K).IsCommutative

theorem IsCommutative_of_IsCommutative_subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) (hH : (H.subgroupOf K).IsCommutative) : (H ⊓ K).IsCommutative

theorem ne_union_left_of_ne {X : Type u_1} (A B : Set X) (not_B_le_A : ¬B ≤ A) : A ⊂ A ∪ B

theorem MaximalAbelianSubgroup.le_centralizer_meet {G : Type u_1} [Group G] (M H : Subgroup G) (hM : M ∈ MaximalAbelianSubgroups H) (x : G) (x_in_M : x ∈ M) : M ≤ Subgroup.centralizer {x} ⊓ H

theorem MaximalAbelianSubgroup.not_le_of_ne {G : Type u_1} [Group G] (A B H : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups H) (hB : B ∈ MaximalAbelianSubgroups H) (A_ne_B : A ≠ B) : ¬B ≤ A

theorem MaximalAbelianSubgroup.le_cen_of_mem {G : Type u_1} [Group G] (A H : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups H) (x : G) (x_in_A : x ∈ A) : A ≤ Subgroup.centralizer {x}

theorem MaximalAbelianSubgroup.lt_cen_meet_G {G : Type u_1} [Group G] (A B H : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups H) (hB : B ∈ MaximalAbelianSubgroups H) (A_ne_B : A ≠ B) (x : G) (x_in_A : x ∈ A) (x_in_B : x ∈ B) : A < Subgroup.centralizer {x} ⊓ H

def MaximalAbelianSubgroup.center_mul {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup G

Equations

• MaximalAbelianSubgroup.center_mul H = { carrier := ↑(Subgroup.center G) * ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem MaximalAbelianSubgroup.center_mul_eq_mul_center {G : Type u_1} [Group G] (H : Subgroup G) : ↑H * ↑(Subgroup.center G) = ↑(Subgroup.center G) * ↑H

theorem MaximalAbelianSubgroup.sup_center_carrier_eq_mul {G : Type u_1} [Group G] (H : Subgroup G) : ↑(H ⊔ Subgroup.center G) = ↑H * ↑(Subgroup.center G)

theorem MaximalAbelianSubgroup.center_mul_subset_center_mul {G : Type u_1} [Group G] (A : Subgroup G) : ↑(Subgroup.center G) * ↑A ⊆ ↑(center_mul A)

theorem MaximalAbelianSubgroup.IsComm_of_center_join_IsComm {G : Type u_1} [Group G] (H : Subgroup G) (hH : H.IsCommutative) : (Subgroup.center G ⊔ H).IsCommutative

theorem MaximalAbelianSubgroup.center_le (G : Type u_1) [Group G] (H A : Subgroup G) (hA : A ∈ MaximalAbelianSubgroups H) (hH : Subgroup.center G ≤ H) : Subgroup.center G ≤ A

theorem MaximalAbelianSubgroup.singleton_of_cen_eq_G (G : Type u_1) [Group G] (H : Subgroup G) (hH : H = Subgroup.center G) : MaximalAbelianSubgroups H = {Subgroup.center G}

theorem MaximalAbelianSubgroup.eq_center_of_card_le_two {F : Type u_1} [Field F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) (hA : A ∈ MaximalAbelianSubgroups G) (card_A_le_two : Nat.card ↥A ≤ 2) : A = Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)

theorem MaximalAbelianSubgroup.centralizer_meet_G_in_MaximalAbelianSubgroups_of_noncentral {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (x : Matrix.SpecialLinearGroup (Fin 2) F) (hx : x ∈ G.carrier \ ↑(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F))) : Subgroup.centralizer {x} ⊓ G ∈ MaximalAbelianSubgroups G

theorem MaximalAbelianSubgroup.center_eq_meet_of_ne_MaximalAbelianSubgroups {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] (A B G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hA : A ∈ MaximalAbelianSubgroups G) (hB : B ∈ MaximalAbelianSubgroups G) (A_ne_B : A ≠ B) (hG : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) : A ⊓ B = Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)

theorem MaximalAbelianSubgroup.IsCyclic_and_card_Coprime_CharP_of_center_eq {F : Type u_1} [Field F] {p : ℕ} (hp : Nat.Prime p) [C : CharP F p] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hA : A ∈ MaximalAbelianSubgroups G) (hG : G = Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) : IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p

theorem MaximalAbelianSubgroup.center_not_mem {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hG : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≠ G) : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ∉ MaximalAbelianSubgroups G

theorem MaximalAbelianSubgroup.eq_centralizer_meet_of_center_lt {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (center_lt : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) < A) (hA : A ∈ MaximalAbelianSubgroups G) : ∃ x ∈ G.carrier \ ↑(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)), A = Subgroup.centralizer {x} ⊓ G

theorem MaximalAbelianSubgroup.Units.coeHom_injective {M : Type u_1} [Monoid M] : Function.Injective ⇑(Units.coeHom M)

theorem MaximalAbelianSubgroup.order_ne_char (F : Type u_1) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (x : Fˣ) : orderOf x ≠ p

theorem MaximalAbelianSubgroup.dvd_pow_totient_sub_one_of_coprime {m p : ℕ} (hp : Nat.Prime p) (h : m.Coprime p) : m ∣ p ^ m.totient - 1

theorem MaximalAbelianSubgroup.coprime_card_fin_subgroup_of_inj_hom_group_iso_units {F : Type u_1} {G : Type u_2} [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] [Group G] (H : Subgroup G) [Finite ↥H] (f : ↥H →* Fˣ) (hf : Function.Injective ⇑f) : (Nat.card ↥H).Coprime p

instance MaximalAbelianSubgroup.TZ_Comm {F : Type u_1} [Field F] : CommGroup ↥(SpecialSubgroups.S F ⊔ SpecialSubgroups.Z F)

Equations

• MaximalAbelianSubgroup.TZ_Comm = ⋯.mpr (let inst := ⋯; Subgroup.IsCommutative.commGroup (SpecialSubgroups.SZ F))

theorem MaximalAbelianSubgroup.conj_ZT_eq_conj_Z_join_T {F : Type u_1} [Field F] (c : Matrix.SpecialLinearGroup (Fin 2) F) : MulAut.conj c • SpecialSubgroups.SZ F = MulAut.conj c • SpecialSubgroups.S F ⊔ SpecialSubgroups.Z F

theorem MaximalAbelianSubgroup.conj_center_eq_center (G : Type u_1) [Group G] (c : G) : MulAut.conj c • Subgroup.center G = Subgroup.center G

theorem MaximalAbelianSubgroup.Z_eq_Z_meet_G (F : Type u_1) [Field F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) : SpecialSubgroups.Z F = SpecialSubgroups.Z F ⊓ G

theorem MaximalAbelianSubgroup.conj_T_join_Z_meet_G_eq_conj_T_meet_G_join_Z {F : Type u_1} [Field F] {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)} (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) (c : Matrix.SpecialLinearGroup (Fin 2) F) : MulAut.conj c • (SpecialSubgroups.S F ⊔ SpecialSubgroups.Z F) ⊓ G = MulAut.conj c • SpecialSubgroups.S F ⊓ G ⊔ SpecialSubgroups.Z F

theorem MaximalAbelianSubgroup.conj_inv_conj_eq (F : Type u_1) [Field F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (c : Matrix.SpecialLinearGroup (Fin 2) F) : MulAut.conj c⁻¹ • (MulAut.conj c • SpecialSubgroups.S F ⊓ G ⊔ SpecialSubgroups.Z F) = SpecialSubgroups.S F ⊓ MulAut.conj c⁻¹ • G ⊔ SpecialSubgroups.Z F

theorem MaximalAbelianSubgroup.IsCyclic_and_card_coprime_CharP_of_IsConj_d {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [hG₀ : Finite ↥G] (A : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (x : Matrix.SpecialLinearGroup (Fin 2) F) (x_not_in_center : x ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) (A_eq_centra : A = Subgroup.centralizer {x} ⊓ G) (δ : Fˣ) (x_IsConj_d : IsConj (SpecialMatrices.d δ) x) : IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p

theorem MaximalAbelianSubgroup.centra_eq_conj_TZ_of_IsConj_t_or_IsConj_neg_t {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (σ : F) (x : Matrix.SpecialLinearGroup (Fin 2) F) (x_IsConj_t_or_neg_t : IsConj (SpecialMatrices.s σ) x ∨ IsConj (-SpecialMatrices.s σ) x) (x_in_G : x ∈ G.carrier) (x_not_in_center : x ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) (hx : Subgroup.centralizer {x} ⊓ G = A) : ∃ (c : Matrix.SpecialLinearGroup (Fin 2) F), MulAut.conj c • SpecialSubgroups.SZ F = Subgroup.centralizer {x}

theorem MaximalAbelianSubgroup.Nat.Prime.three_le_of_ne_two {p : ℕ} (hp : Nat.Prime p) (p_ne_two : p ≠ 2) : 3 ≤ p

theorem MaximalAbelianSubgroup.ne_zero_two_of_char_ne_two (F : Type u_1) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (p_ne_two : p ≠ 2) : NeZero 2

theorem MaximalAbelianSubgroup.card_center_lt_card_center_Sylow (F : Type u_1) [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] (S : Sylow p ↥G) (p_le_card_center_S : p ≤ Nat.card ↥(Subgroup.center ↥↑S)) : ∃ x ∈ Subgroup.map (G.subtype.comp (↑S).subtype) (Subgroup.center ↥↑S), x ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)

theorem MaximalAbelianSubgroup.mul_center_eq_left {F : Type u_1} [Field F] {G : Type u_2} [Group G] (S Q : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (Q_le_S : Q ≤ S) (h' : 1 = -1 ∨ -1 ∉ S) (hSQ : S.carrier * ↑(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) = Q.carrier * ↑(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F))) : S = Q

theorem MaximalAbelianSubgroup.A_eq_Q_join_Z_of_IsConj_s_or_neg_s {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [hG₀ : Finite ↥G] (A : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hA : A ∈ MaximalAbelianSubgroups G) (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) (center_lt_A : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) < A) (x : Matrix.SpecialLinearGroup (Fin 2) F) (x_in_G : x ∈ G.carrier) (x_not_in_center : x ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) (A_eq_centra : A = Subgroup.centralizer {x} ⊓ G) (σ : F) (x_IsConj_t_or_neg_t : IsConj (SpecialMatrices.s σ) x ∨ IsConj (-SpecialMatrices.s σ) x) : ∃ (Q : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)), Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ SpecialSubgroups.Z F ∧ IsElementaryAbelian p Q ∧ ∃ (S : Sylow p ↥G), Q.subgroupOf G = ↑S

theorem MaximalAbelianSubgroup.IsCyclic_and_card_coprime_CharP_or_fin_prod_IsElementaryAbelian_le_T_of_center_ne {F : Type u_1} [Field F] [IsAlgClosed F] [DecidableEq F] {p : ℕ} [hp' : Fact (Nat.Prime p)] [hC : CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [hG₀ : Finite ↥G] (A : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hA : A ∈ MaximalAbelianSubgroups G) (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) (center_ne_G : G ≠ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) : IsCyclic ↥A ∧ (Nat.card ↥A).Coprime p ∨ ∃ (Q : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)), Nontrivial ↥Q ∧ Finite ↥Q ∧ Q ≤ G ∧ A = Q ⊔ SpecialSubgroups.Z F ∧ IsElementaryAbelian p Q ∧ ∃ (S : Sylow p ↥G), Q.subgroupOf G = ↑S

theorem MaximalAbelianSubgroup.index_normalizer_le_two {F : Type u_1} [Field F] {p : ℕ} (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (center_le_G : Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F) ≤ G) (hA : A ∈ MaximalAbelianSubgroups G) (hA' : (Nat.card ↥A).Coprime p) : (A.subgroupOf G).normalizer.index ≤ 2

theorem MaximalAbelianSubgroup.of_index_normalizer_eq_two {F : Type u_1} [Field F] {p : ℕ} (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (hA : A ∈ MaximalAbelianSubgroups G) (hA' : (Nat.card ↥A).Coprime p) (hNA : A.normalizer.index = 2) (x : ↥A) : ∃ y ∈ A.normalizer.carrier \ ↑A, y * ↑x * y⁻¹ = ↑x⁻¹

def MaximalAbelianSubgroup.theorem_2_6_v_a {F : Type u_1} [Field F] {p : ℕ} (hp : Nat.Prime p) (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (Q : Sylow p ↥G) (h : ↑Q ≠ ⊥) : ∃ (K : Subgroup ↥G), IsCyclic ↥K ∧ (↑Q).normalizer = ↑Q ⊓ K

Equations

• ⋯ = ⋯

theorem MaximalAbelianSubgroup.theorem_2_6_v_b {F : Type u_1} [Field F] {p : ℕ} [hp' : Fact (Nat.Prime p)] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) (Q : Sylow p ↥G) (h : ↑Q ≠ ⊥) (K : Subgroup ↥G) (hK : IsCyclic ↥K) (hNG : (↑Q).normalizer = ↑Q ⊔ K) : Nat.card ↥K > Nat.card ↥(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) → Subgroup.map G.subtype K ∈ MaximalAbelianSubgroups G