mathlib3 documentation

group_theory.subgroup.finite

Subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides some result on multiplicative and additive subgroups in the finite context.

Tags #

subgroup, subgroups

source
@[protected, instance]
def subgroup.fintype {G : Type u_1} [group G] (K : subgroup G) [d : decidable_pred (λ (_x : G), _x ∈ K)] [fintype G] :
fintype ↥K
Equations
source
@[protected, instance]
def add_subgroup.fintype {G : Type u_1} [add_group G] (K : add_subgroup G) [d : decidable_pred (λ (_x : G), _x ∈ K)] [fintype G] :
fintype ↥K
Equations
source
@[protected, instance]
def subgroup.finite {G : Type u_1} [group G] (K : subgroup G) [finite G] :
finite ↥K
source
@[protected, instance]
def add_subgroup.finite {G : Type u_1} [add_group G] (K : add_subgroup G) [finite G] :
finite ↥K

Conversion to/from additive/multiplicative #

source
@[protected]
theorem subgroup.list_prod_mem {G : Type u_1} [group G] (K : subgroup G) {l : list G} :
(∀ (x : G), x ∈ l → x ∈ K) → l.prod ∈ K

Product of a list of elements in a subgroup is in the subgroup.

source
@[protected]
theorem add_subgroup.list_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {l : list G} :
(∀ (x : G), x ∈ l → x ∈ K) → l.sum ∈ K

Sum of a list of elements in an add_subgroup is in the add_subgroup.

source
@[protected]
theorem add_subgroup.multiset_sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) (g : multiset G) :
(∀ (a : G), a ∈ g → a ∈ K) → g.sum ∈ K

Sum of a multiset of elements in an add_subgroup of an add_comm_group is in the add_subgroup.

source
@[protected]
theorem subgroup.multiset_prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) (g : multiset G) :
(∀ (a : G), a ∈ g → a ∈ K) → g.prod ∈ K

Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.

source
theorem subgroup.multiset_noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) (g : multiset G) (comm : {x : G | x ∈ g}.pairwise commute) :
(∀ (a : G), a ∈ g → a ∈ K) → g.noncomm_prod comm ∈ K
source
theorem add_subgroup.multiset_noncomm_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) (g : multiset G) (comm : {x : G | x ∈ g}.pairwise add_commute) :
(∀ (a : G), a ∈ g → a ∈ K) → g.noncomm_sum comm ∈ K
source
@[protected]
theorem add_subgroup.sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (h : ∀ (c : ι), c ∈ t → f c ∈ K) :
t.sum (λ (c : ι), f c) ∈ K

Sum of elements in an add_subgroup of an add_comm_group indexed by a finset is in the add_subgroup.

source
@[protected]
theorem subgroup.prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (h : ∀ (c : ι), c ∈ t → f c ∈ K) :
t.prod (λ (c : ι), f c) ∈ K

Product of elements of a subgroup of a comm_group indexed by a finset is in the subgroup.

source
theorem add_subgroup.noncomm_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (comm : ↑t.pairwise (λ (a b : ι), add_commute (f a) (f b))) :
(∀ (c : ι), c ∈ t → f c ∈ K) → t.noncomm_sum f comm ∈ K
source
theorem subgroup.noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (comm : ↑t.pairwise (λ (a b : ι), commute (f a) (f b))) :
(∀ (c : ι), c ∈ t → f c ∈ K) → t.noncomm_prod f comm ∈ K
source
@[simp, norm_cast]
theorem add_subgroup.coe_list_sum {G : Type u_1} [add_group G] (H : add_subgroup G) (l : list ↥H) :
↑(l.sum) = (list.map coe l).sum
source
@[simp, norm_cast]
theorem subgroup.coe_list_prod {G : Type u_1} [group G] (H : subgroup G) (l : list ↥H) :
↑(l.prod) = (list.map coe l).prod
source
@[simp, norm_cast]
theorem subgroup.coe_multiset_prod {G : Type u_1} [comm_group G] (H : subgroup G) (m : multiset ↥H) :
↑(m.prod) = (multiset.map coe m).prod
source
@[simp, norm_cast]
theorem add_subgroup.coe_multiset_sum {G : Type u_1} [add_comm_group G] (H : add_subgroup G) (m : multiset ↥H) :
↑(m.sum) = (multiset.map coe m).sum
source
@[simp, norm_cast]
theorem add_subgroup.coe_finset_sum {ι : Type u_1} {G : Type u_2} [add_comm_group G] (H : add_subgroup G) (f : ι → ↥H) (s : finset ι) :
↑(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ↑(f i))
source
@[simp, norm_cast]
theorem subgroup.coe_finset_prod {ι : Type u_1} {G : Type u_2} [comm_group G] (H : subgroup G) (f : ι → ↥H) (s : finset ι) :
↑(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ↑(f i))
source
@[protected, instance]
def subgroup.fintype_bot {G : Type u_1} [group G] :
fintype ↥⊥
Equations
source
@[protected, instance]
def add_subgroup.fintype_bot {G : Type u_1} [add_group G] :
fintype ↥⊥
Equations
source
@[simp]
theorem subgroup.card_bot {G : Type u_1} [group G] {_x : fintype ↥⊥} :
fintype.card ↥⊥ = 1
source
@[simp]
theorem add_subgroup.card_bot {G : Type u_1} [add_group G] {_x : fintype ↥⊥} :
fintype.card ↥⊥ = 1
source
theorem subgroup.eq_top_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] [fintype G] (h : fintype.card ↥H = fintype.card G) :
H = ⊤
source
theorem add_subgroup.eq_top_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] [fintype G] (h : fintype.card ↥H = fintype.card G) :
H = ⊤
source
theorem subgroup.eq_top_of_le_card {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] [fintype G] (h : fintype.card G ≤ fintype.card ↥H) :
H = ⊤
source
theorem add_subgroup.eq_top_of_le_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] [fintype G] (h : fintype.card G ≤ fintype.card ↥H) :
H = ⊤
source
theorem subgroup.eq_bot_of_card_le {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] (h : fintype.card ↥H ≤ 1) :
H = ⊥
source
theorem add_subgroup.eq_bot_of_card_le {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] (h : fintype.card ↥H ≤ 1) :
H = ⊥
source
theorem add_subgroup.eq_bot_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] (h : fintype.card ↥H = 1) :
H = ⊥
source
theorem subgroup.eq_bot_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] (h : fintype.card ↥H = 1) :
H = ⊥
source
theorem add_subgroup.card_nonpos_iff_eq_bot {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] :
fintype.card ↥H ≤ 1 ↔ H = ⊥
source
theorem subgroup.card_le_one_iff_eq_bot {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] :
fintype.card ↥H ≤ 1 ↔ H = ⊥
source
theorem add_subgroup.pos_card_iff_ne_bot {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] :
1 < fintype.card ↥H ↔ H ≠ ⊥
source
theorem subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] :
1 < fintype.card ↥H ↔ H ≠ ⊥
source
theorem subgroup.pi_mem_of_mul_single_mem_aux {η : Type u_3} {f : η → Type u_4} [Π (i : η), group (f i)] [decidable_eq η] (I : finset η) {H : subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h1 : ∀ (i : η), i ∉ I → x i = 1) (h2 : ∀ (i : η), i ∈ I → pi.mul_single i (x i) ∈ H) :
x ∈ H
source
theorem add_subgroup.pi_mem_of_single_mem_aux {η : Type u_3} {f : η → Type u_4} [Π (i : η), add_group (f i)] [decidable_eq η] (I : finset η) {H : add_subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h1 : ∀ (i : η), i ∉ I → x i = 0) (h2 : ∀ (i : η), i ∈ I → pi.single i (x i) ∈ H) :
x ∈ H
source
theorem add_subgroup.pi_mem_of_single_mem {η : Type u_3} {f : η → Type u_4} [Π (i : η), add_group (f i)] [finite η] [decidable_eq η] {H : add_subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h : ∀ (i : η), pi.single i (x i) ∈ H) :
x ∈ H
source
theorem subgroup.pi_mem_of_mul_single_mem {η : Type u_3} {f : η → Type u_4} [Π (i : η), group (f i)] [finite η] [decidable_eq η] {H : subgroup (Π (i : η), f i)} (x : Π (i : η), f i) (h : ∀ (i : η), pi.mul_single i (x i) ∈ H) :
x ∈ H
source
theorem subgroup.pi_le_iff {η : Type u_3} {f : η → Type u_4} [Π (i : η), group (f i)] [decidable_eq η] [finite η] {H : Π (i : η), subgroup (f i)} {J : subgroup (Π (i : η), f i)} :
subgroup.pi set.univ H ≤ J ↔ ∀ (i : η), subgroup.map (monoid_hom.single f i) (H i) ≤ J

For finite index types, the subgroup.pi is generated by the embeddings of the groups.

source
theorem add_subgroup.pi_le_iff {η : Type u_3} {f : η → Type u_4} [Π (i : η), add_group (f i)] [decidable_eq η] [finite η] {H : Π (i : η), add_subgroup (f i)} {J : add_subgroup (Π (i : η), f i)} :
add_subgroup.pi set.univ H ≤ J ↔ ∀ (i : η), add_subgroup.map (add_monoid_hom.single f i) (H i) ≤ J

For finite index types, the subgroup.pi is generated by the embeddings of the additive groups.

source
theorem subgroup.mem_normalizer_fintype {G : Type u_1} [group G] {S : set G} [finite ↥S] {x : G} (h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S) :
x ∈ subgroup.set_normalizer S
source
@[protected, instance]
def add_monoid_hom.decidable_mem_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) [fintype G] [decidable_eq N] :
decidable_pred (λ (_x : N), _x ∈ f.range)
Equations
source
@[protected, instance]
def monoid_hom.decidable_mem_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) [fintype G] [decidable_eq N] :
decidable_pred (λ (_x : N), _x ∈ f.range)
Equations
source
@[protected, instance]
def add_monoid_hom.fintype_mrange {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] [fintype M] [decidable_eq N] (f : M →+ N) :
fintype ↥(add_monoid_hom.mrange f)

The range of a finite additive monoid under an additive monoid homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations
source
@[protected, instance]
def monoid_hom.fintype_mrange {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] [fintype M] [decidable_eq N] (f : M →* N) :
fintype ↥(monoid_hom.mrange f)

The range of a finite monoid under a monoid homomorphism is finite. Note: this instance can form a diamond with subtype.fintype in the presence of fintype N.

Equations
source
@[protected, instance]
def monoid_hom.fintype_range {G : Type u_1} [group G] {N : Type u_3} [group N] [fintype G] [decidable_eq N] (f : G →* N) :
fintype ↥(f.range)

The range of a finite group under a group homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations
source
@[protected, instance]
def add_monoid_hom.fintype_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] [fintype G] [decidable_eq N] (f : G →+ N) :
fintype ↥(f.range)

The range of a finite additive group under an additive group homomorphism is finite.

Note: this instance can form a diamond with subtype.fintype or subgroup.fintype in the presence of fintype N.

Equations