mathlib docs: group_theory.sylow

source

theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one {G : Type u} {α : Type v} [group G] [mul_action G α] {a : α} [fintype ↥(mul_action.orbit G a)] :

a ∈ mul_action.fixed_points G α ↔ fintype.card ↥(mul_action.orbit G a) = 1

source

theorem mul_action.card_modeq_card_fixed_points {G : Type u} {α : Type v} [group G] [mul_action G α] [fintype α] [fintype G] [fintype ↥(mul_action.fixed_points G α)] (p : ℕ) {n : ℕ} [hp : fact (nat.prime p)] (h : fintype.card G = p ^ n) :

fintype.card α ≡ fintype.card ↥(mul_action.fixed_points G α) [MOD p]

source

theorem quotient_group.card_preimage_mk {G : Type u} [group G] [fintype G] (s : subgroup G) (t : set (quotient_group.quotient s)) :

fintype.card ↥(quotient_group.mk ⁻¹' t) = (fintype.card ↥s) * fintype.card ↥t

source

def sylow.mk_vector_prod_eq_one {G : Type u} [group G] (n : ℕ) (v : vector G n) :

vector G (n + 1)

Given a vector v of length n, make a vector of length n+1 whose product is 1, by consing the the inverse of the product of v.

Equations

sylow.mk_vector_prod_eq_one n v = (v.to_list.prod)⁻¹ :: v

source

theorem sylow.mk_vector_prod_eq_one_injective {G : Type u} [group G] (n : ℕ) :

function.injective (sylow.mk_vector_prod_eq_one n)

source

def sylow.vectors_prod_eq_one (G : Type u_1) [group G] (n : ℕ) :

set (vector G n)

The type of vectors with terms from G, length n, and product equal to 1:G.

Equations

sylow.vectors_prod_eq_one G n = {v : vector G n | v.to_list.prod = 1}

source

theorem sylow.mem_vectors_prod_eq_one {G : Type u} [group G] {n : ℕ} (v : vector G n) :

v ∈ sylow.vectors_prod_eq_one G n ↔ v.to_list.prod = 1

source

theorem sylow.mem_vectors_prod_eq_one_iff {G : Type u} [group G] {n : ℕ} (v : vector G (n + 1)) :

v ∈ sylow.vectors_prod_eq_one G (n + 1) ↔ v ∈ set.range (sylow.mk_vector_prod_eq_one n)

source

def sylow.rotate_vectors_prod_eq_one (G : Type u_1) [group G] (n : ℕ) (m : multiplicative (zmod n)) (v : ↥(sylow.vectors_prod_eq_one G n)) :

↥(sylow.vectors_prod_eq_one G n)

The rotation action of zmod n (viewed as multiplicative group) on vectors_prod_eq_one G n, where G is a multiplicative group.

Equations

sylow.rotate_vectors_prod_eq_one G n m v = ⟨⟨v.val.to_list.rotate (zmod.val m), _⟩, _⟩

source

@[instance]

def sylow.rotate_vectors_prod_eq_one.mul_action {G : Type u} [group G] (n : ℕ) [fact (0 < n)] :

mul_action (multiplicative (zmod n)) ↥(sylow.vectors_prod_eq_one G n)

Equations

sylow.rotate_vectors_prod_eq_one.mul_action n = {to_has_scalar := {smul := sylow.rotate_vectors_prod_eq_one G n}, one_smul := _, mul_smul := _}

source

theorem sylow.one_mem_vectors_prod_eq_one {G : Type u} [group G] (n : ℕ) :

vector.repeat 1 n ∈ sylow.vectors_prod_eq_one G n

source

theorem sylow.one_mem_fixed_points_rotate {G : Type u} [group G] (n : ℕ) [fact (0 < n)] :

⟨vector.repeat 1 n, _⟩ ∈ mul_action.fixed_points (multiplicative (zmod n)) ↥(sylow.vectors_prod_eq_one G n)

source

theorem sylow.exists_prime_order_of_dvd_card {G : Type u} [group G] [fintype G] (p : ℕ) [hp : fact (nat.prime p)] (hdvd : p ∣ fintype.card G) :

∃ (x : G), order_of x = p

Cauchy's theorem

source

theorem sylow.mem_fixed_points_mul_left_cosets_iff_mem_normalizer {G : Type u} [group G] {H : subgroup G} [fintype ↥↑H] {x : G} :

↑x ∈ mul_action.fixed_points ↥H (quotient_group.quotient H) ↔ x ∈ H.normalizer

source

def sylow.fixed_points_mul_left_cosets_equiv_quotient {G : Type u} [group G] (H : subgroup G) [fintype ↥↑H] :

↥(mul_action.fixed_points ↥H (quotient_group.quotient H)) ≃ quotient_group.quotient (subgroup.comap H.normalizer.subtype H)

Equations

sylow.fixed_points_mul_left_cosets_equiv_quotient H = equiv.subtype_quotient_equiv_quotient_subtype ↑(H.normalizer) (mul_action.fixed_points ↥H (quotient (id {r := λ (x y : G), x⁻¹ * y ∈ H, iseqv := _}))) _ _

source

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ℕ) {n : ℕ} [hp : fact (nat.prime p)] (hdvd : p ^ n ∣ fintype.card G) :

∃ (H : subgroup G), fintype.card ↥H = p ^ n