ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S2

source

def SpecialSubgroups.D (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

SpecialSubgroups.D F = { carrier := {x : Matrix.SpecialLinearGroup (Fin 2) F | ∃ (δ : Fˣ), SpecialMatrices.d δ = x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source

def SpecialSubgroups.D_iso_units (F : Type u_1) [Field F] :

↥(D F) ≃* Fˣ

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SpecialSubgroups.S (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

SpecialSubgroups.S F = { carrier := {x : Matrix.SpecialLinearGroup (Fin 2) F | ∃ (σ : F), SpecialMatrices.s σ = x}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source

def SpecialSubgroups.S_iso_F (F : Type u_1) [Field F] :

↥(S F) ≃* Multiplicative F

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem SpecialSubgroups.D_meet_S_eq_bot {F : Type u_1} [Field F] :

D F ⊓ S F = ⊥

source

def SpecialSubgroups.L (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem SpecialSubgroups.S_le_L {F : Type u} [Field F] :

S F ≤ L F

source

theorem SpecialSubgroups.normal_S_subgroupOf_L {F : Type u_1} [Field F] :

((S F).subgroupOf (L F)).Normal

source

instance SpecialSubgroups.group_L_quot_S_subgroupOf_L {F : Type u} [Field F] :

Group (↥(L F) ⧸ (S F).subgroupOf (L F))

Equations

SpecialSubgroups.group_L_quot_S_subgroupOf_L = QuotientGroup.Quotient.group ((SpecialSubgroups.S F).subgroupOf (SpecialSubgroups.L F))

source

def SpecialSubgroups.prod_iso_join_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) (hHK : H ⊓ K = ⊥) [hH : H.Normal] [hK : K.Normal] :

↥H × ↥K ≃* ↥(H ⊔ K)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem SpecialSubgroups.L_eq_D_join_S {F : Type u} [Field F] :

L F = D F ⊔ S F

source

def SpecialSubgroups.L_quot_S_subgroupOf_L_iso_D {F : Type u} [Field F] :

↥(L F) ⧸ (S F).subgroupOf (L F) ≃* ↥(D F)

Equations

SpecialSubgroups.L_quot_S_subgroupOf_L_iso_D = sorry

Instances For

source

def SpecialSubgroups.DW (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem SpecialSubgroups.D_leq_DW {F : Type u} [Field F] :

D F ≤ DW F

source

theorem SpecialSubgroups.Dw_leq_DW {F : Type u} [Field F] :

↑(D F) * {SpecialMatrices.w } ⊆ ↑(DW F)

source

def SpecialSubgroups.Z (R : Type u) [CommRing R] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) R)

Equations

SpecialSubgroups.Z R = Subgroup.closure {-1}

Instances For

source

theorem SpecialSubgroups.get_entries {F : Type u} [Field F] (x : Matrix.SpecialLinearGroup (Fin 2) F) :

∃ (α : F) (β : F) (γ : F) (δ : F), α = ↑x 0 0 ∧ β = ↑x 0 1 ∧ γ = ↑x 1 0 ∧ δ = ↑x 1 1 ∧ ↑x = !![α, β; γ, δ]

source

theorem SpecialSubgroups.neg_one_mem_Z {F : Type u} [Field F] :

-1 ∈ Z F

source

theorem SpecialSubgroups.Odd.neg_one_zpow {α : Type u_1} [Group α] [HasDistribNeg α] {n : ℤ} (h : Odd n) :

(-1) ^ n = -1

source

theorem SpecialSubgroups.closure_neg_one_eq (R : Type u) [CommRing R] :

↑(Subgroup.closure {-1}) = {1, -1}

source

@[simp]

theorem SpecialSubgroups.neg_one_neq_one_of_two_ne_zero {F : Type u} [Field F] [NeZero 2] :

1 ≠ -1

source

theorem SpecialSubgroups.Field.one_eq_neg_one_of_two_eq_zero {F : Type u} [Field F] (two_eq_zero : 2 = 0) :

1 = -1

source

theorem SpecialSubgroups.SpecialLinearGroup.neg_one_eq_one_of_two_eq_zero {F : Type u} [Field F] (two_eq_zero : 2 = 0) :

1 = -1

source

@[simp]

theorem SpecialSubgroups.set_Z_eq (R : Type u) [CommRing R] :

↑(Z R) = {1, -1}

source

@[simp]

theorem SpecialSubgroups.Z_carrier_eq (R : Type u) [CommRing R] :

(Z R).carrier = {1, -1}

source

@[simp]

theorem SpecialSubgroups.mem_Z_iff (R : Type u) [CommRing R] {x : Matrix.SpecialLinearGroup (Fin 2) R} :

x ∈ Z R ↔ x = 1 ∨ x = -1

source

instance SpecialSubgroups.instFiniteSubtypeSpecialLinearGroupFinOfNatNatMemSubgroupZ {F : Type u} [Field F] :

Finite ↥(Z F)

source

theorem SpecialSubgroups.center_SL2_F_eq_Z (R : Type u_1) [CommRing R] [NoZeroDivisors R] :

Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) R) = Z R

source

instance SpecialSubgroups.instFiniteSubtypeSpecialLinearGroupFinOfNatNatMemSubgroupCenter_classificationOfSubgroups {F : Type u} [Field F] :

Finite ↥(Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F))

source

theorem SpecialSubgroups.card_Z_eq_two_of_two_ne_zero {F : Type u} [Field F] [NeZero 2] :

Nat.card ↥(Z F) = 2

source

theorem SpecialSubgroups.card_Z_eq_one_of_two_eq_zero {F : Type u} [Field F] (two_eq_zero : 2 = 0) :

Nat.card ↥(Z F) = 1

source

theorem SpecialSubgroups.card_Z_le_two {F : Type u} [Field F] :

Nat.card ↥(Z F) ≤ 2

source

theorem SpecialSubgroups.orderOf_neg_one_eq_two {F : Type u} [Field F] [NeZero 2] :

orderOf (-1) = 2

source

theorem SpecialSubgroups.exists_unique_orderOf_eq_two {F : Type u} [Field F] [NeZero 2] :

∃! x : Matrix.SpecialLinearGroup (Fin 2) F, orderOf x = 2

source

theorem SpecialSubgroups.IsCyclic_Z {F : Type u} [Field F] :

IsCyclic ↥(Z F)

source

theorem SpecialSubgroups.IsPGroup.p_dvd_card_center {H : Type u_1} {p : ℕ} (hp : Nat.Prime p) [Group H] [Finite H] [Nontrivial H] (hH : IsPGroup p H) :

p ∣ Nat.card ↥(Subgroup.center H)

source

def SpecialSubgroups.SZ (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def SpecialSubgroups.SZ' (F : Type u_1) [Field F] :

Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)

Equations

SpecialSubgroups.SZ' F = { carrier := ↑(SpecialSubgroups.S F) * ↑(SpecialSubgroups.Z F), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source

theorem SpecialSubgroups.SZ_eq_SZ' {F : Type u_1} [Field F] :

SZ' F = SZ F

source

theorem SpecialSubgroups.S_mul_Z_subset_SZ {F : Type u} [Field F] :

↑(S F) * ↑(Z F) ⊆ ↑(SZ F)

source

theorem SpecialSubgroups.S_join_Z_eq_SZ {F : Type u} [Field F] :

S F ⊔ Z F = SZ F

source

theorem SpecialSubgroups.IsCommutative_iff {G : Type u_1} [Group G] (H : Subgroup G) :

H.IsCommutative ↔ ∀ (x y : ↥H), x * y = y * x

source

theorem SpecialSubgroups.IsCommutative_D {F : Type u} [Field F] :

(D F).IsCommutative

source

theorem SpecialSubgroups.IsCommutative_S (F : Type u_1) [Field F] :

(S F).IsCommutative

source

theorem SpecialSubgroups.IsCommutative_SZ (F : Type u_1) [Field F] :

(SZ F).IsCommutative

source

theorem SpecialSubgroups.val_eq_neg_one {F : Type u} [Field F] {a : Fˣ} :

↑a = -1 ↔ a = -1

source

theorem SpecialSubgroups.ex_of_card_D_gt_two {F : Type u} [Field F] {D₀ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) F)} (hD₀ : 2 < Nat.card ↥D₀) (D₀_leq_D : D₀ ≤ D F) :

∃ (δ : Fˣ), ↑δ ≠ 1 ∧ ↑δ ≠ -1 ∧ SpecialMatrices.d δ ∈ D₀

source

theorem SpecialSubgroups.mem_D_iff {F : Type u} [Field F] {x : Matrix.SpecialLinearGroup (Fin 2) F} :

x ∈ D F ↔ ∃ (δ : Fˣ), SpecialMatrices.d δ = x

source

theorem SpecialSubgroups.mem_D_w_iff {F : Type u} [Field F] {x : Matrix.SpecialLinearGroup (Fin 2) F} :

x ∈ ↑(D F) * {SpecialMatrices.w } ↔ ∃ (δ : Fˣ), SpecialMatrices.d δ * SpecialMatrices.w = x

Documentation

ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S2_SpecialSubgroups