def Subgroup.noncenter {G : Type u_1} [Group G] (H : Subgroup G) : Set G

Equations

• H.noncenter = {x : G | x ∈ H.carrier \ ↑(Subgroup.center G)}

def noncenter_MaximalAbelianSubgroups {F : Type u_1} [Field F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) : Set (Set (Matrix.SpecialLinearGroup (Fin 2) F))

Equations

• noncenter_MaximalAbelianSubgroups G = {x : Set (Matrix.SpecialLinearGroup (Fin 2) F) | ∃ K ∈ MaximalAbelianSubgroups G, K.noncenter = x}

def ConjClassOfSet {G : Type u_1} [Group G] (A : Subgroup G) : Set (Subgroup G)

Equations

• ConjClassOfSet A = {x : Subgroup G | ∃ (x_1 : G), MulAut.conj x_1 • A = x}

def noncenter_ConjClassOfSet {G : Type u_1} [Group G] (A : Subgroup G) : Set (Set G)

Equations

• noncenter_ConjClassOfSet A = {x : Set G | ∃ (x_1 : G), MulAut.conj x_1 • A.noncenter = x}

instance instSetoidElemSetSpecialLinearGroupFinOfNatNatNoncenter_MaximalAbelianSubgroups {F : Type u_1} [Field F] {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)} : Setoid ↑(noncenter_MaximalAbelianSubgroups G)

Equations

• instSetoidElemSetSpecialLinearGroupFinOfNatNatNoncenter_MaximalAbelianSubgroups = { r := fun (Aᵢ Aⱼ : ↑(noncenter_MaximalAbelianSubgroups G)) => IsConj ↑Aᵢ ↑Aⱼ, iseqv := ⋯ }

def noncenter_C {F : Type u_1} [Field F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] : Set (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

• noncenter_C A G = ⋃ x ∈ G, MulAut.conj x • A.noncenter

theorem card_noncenter_C_eq_card_A_mul_card_noncenter_ConjClass {F : Type u_1} [Field F] (G A : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] : Nat.card ↑(noncenter_C A G) = Nat.card ↑A.noncenter * Nat.card ↑(noncenter_ConjClassOfSet A)

theorem subgroup_sdiff_center_eq_union_noncenter_C {F : Type u_1} [Field F] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] : G.carrier \ ↑(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)) = ⋃ A ∈ MaximalAbelianSubgroups G, noncenter_C A G

theorem card_noncenter_ConjClassOfSet_eq_card_ConjClassOfSet {G : Type u_1} [Group G] (A : Subgroup G) : Nat.card ↑(ConjClassOfSet A) = Nat.card ↑(noncenter_ConjClassOfSet A)

theorem card_ConjClassOfSet_eq_index_normalizer {F : Type u_1} [Field F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) : Nat.card ↑(ConjClassOfSet A) = (A.subgroupOf G).normalizer.index

instance instFintypeElemSubgroupMaximalAbelianSubgroupsOfFiniteSubtypeMem {L : Type u_1} [Group L] {G : Subgroup L} [Finite ↥G] : Fintype ↑(MaximalAbelianSubgroups G)

Equations

• instFintypeElemSubgroupMaximalAbelianSubgroupsOfFiniteSubtypeMem = sorry

theorem normalizer_noncentral_eq {F : Type u_1} [Field F] (A G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] (hA : A ∈ MaximalAbelianSubgroups G) : A.normalizer = Subgroup.setNormalizer A.noncenter

theorem normalizer_Sylow_join_center_eq_normalizer_Sylow {F : Type u_1} [Field F] {p : ℕ} [Fact (Nat.Prime p)] [CharP F p] (G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)) [Finite ↥G] (Q : Sylow p ↥G) : (Subgroup.map G.subtype ↑Q ⊔ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F)).normalizer = (Subgroup.map G.subtype ↑Q).normalizer