HepLean Documentation

Mathlib.Algebra.Group.Subgroup.Finite

Subgroups #

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

Tags #

subgroup, subgroups

source
instance AddSubgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [AddGroup G] (K : AddSubgroup G) [DecidablePred fun (x : G) => x ∈ K] [Fintype G] :
Fintype ↥K
Equations
  • K.instFintypeSubtypeMemOfDecidablePred = inferInstance
source
instance Subgroup.instFintypeSubtypeMemOfDecidablePred {G : Type u_1} [Group G] (K : Subgroup G) [DecidablePred fun (x : G) => x ∈ K] [Fintype G] :
Fintype ↥K
Equations
  • K.instFintypeSubtypeMemOfDecidablePred = inferInstance
source
instance AddSubgroup.instFiniteSubtypeMem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) [Finite G] :
Finite ↥K
Equations
  • ⋯ = ⋯
source
instance Subgroup.instFiniteSubtypeMem {G : Type u_1} [Group G] (K : Subgroup G) [Finite G] :
Finite ↥K
Equations
  • ⋯ = ⋯

Conversion to/from Additive/Multiplicative #

source
theorem AddSubgroup.list_sum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {l : List G} :
(∀ x ∈ l, x ∈ K) → l.sum ∈ K

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

source
theorem Subgroup.list_prod_mem {G : Type u_1} [Group G] (K : Subgroup G) {l : List G} :
(∀ x ∈ l, x ∈ K) → l.prod ∈ K

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

source
theorem AddSubgroup.multiset_sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) (g : Multiset G) :
(∀ a ∈ g, a ∈ K) → g.sum ∈ K

Sum of a multiset of elements in an AddSubgroup of an AddCommGroup is in the AddSubgroup.

source
theorem Subgroup.multiset_prod_mem {G : Type u_3} [CommGroup G] (K : Subgroup G) (g : Multiset G) :
(∀ a ∈ g, a ∈ K) → g.prod ∈ K

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

source
theorem AddSubgroup.multiset_noncommSum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (g : Multiset G) (comm : {x : G | x ∈ g}.Pairwise AddCommute) :
(∀ a ∈ g, a ∈ K) → g.noncommSum comm ∈ K
source
theorem Subgroup.multiset_noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) (g : Multiset G) (comm : {x : G | x ∈ g}.Pairwise Commute) :
(∀ a ∈ g, a ∈ K) → g.noncommProd comm ∈ K
source
theorem AddSubgroup.sum_mem {G : Type u_3} [AddCommGroup G] (K : AddSubgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) :
∑ c ∈ t, f c ∈ K

Sum of elements in an AddSubgroup of an AddCommGroup indexed by a Finset is in the AddSubgroup.

source
theorem Subgroup.prod_mem {G : Type u_3} [CommGroup G] (K : Subgroup G) {ι : Type u_4} {t : Finset ι} {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) :
∏ c ∈ t, f c ∈ K

Product of elements of a subgroup of a CommGroup indexed by a Finset is in the subgroup.

source
theorem AddSubgroup.noncommSum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise fun (a b : ι) => AddCommute (f a) (f b)) :
(∀ c ∈ t, f c ∈ K) → t.noncommSum f comm ∈ K
source
theorem Subgroup.noncommProd_mem {G : Type u_1} [Group G] (K : Subgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise fun (a b : ι) => Commute (f a) (f b)) :
(∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K
source
@[simp]
theorem AddSubgroup.val_list_sum {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (l : List ↥H) :
↑l.sum = (List.map Subtype.val l).sum
source
@[simp]
theorem Subgroup.val_list_prod {G : Type u_1} [Group G] (H : Subgroup G) (l : List ↥H) :
↑l.prod = (List.map Subtype.val l).prod
source
@[simp]
theorem AddSubgroup.val_multiset_sum {G : Type u_3} [AddCommGroup G] (H : AddSubgroup G) (m : Multiset ↥H) :
↑m.sum = (Multiset.map Subtype.val m).sum
source
@[simp]
theorem Subgroup.val_multiset_prod {G : Type u_3} [CommGroup G] (H : Subgroup G) (m : Multiset ↥H) :
↑m.prod = (Multiset.map Subtype.val m).prod
source
@[simp]
theorem AddSubgroup.val_finset_sum {ι : Type u_3} {G : Type u_4} [AddCommGroup G] (H : AddSubgroup G) (f : ι → ↥H) (s : Finset ι) :
↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
source
@[simp]
theorem Subgroup.val_finset_prod {ι : Type u_3} {G : Type u_4} [CommGroup G] (H : Subgroup G) (f : ι → ↥H) (s : Finset ι) :
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
source
instance AddSubgroup.fintypeBot {G : Type u_1} [AddGroup G] :
Fintype ↥⊥
Equations
  • AddSubgroup.fintypeBot = { elems := {0}, complete := ⋯ }
source
theorem AddSubgroup.fintypeBot.proof_1 {G : Type u_1} [AddGroup G] :
∀ (x : ↥⊥), x ∈ {0}
source
instance Subgroup.fintypeBot {G : Type u_1} [Group G] :
Fintype ↥⊥
Equations
  • Subgroup.fintypeBot = { elems := {1}, complete := ⋯ }
source
theorem AddSubgroup.card_bot {G : Type u_1} [AddGroup G] :
Nat.card ↥⊥ = 1
source
theorem Subgroup.card_bot {G : Type u_1} [Group G] :
Nat.card ↥⊥ = 1
source
theorem AddSubgroup.card_top {G : Type u_1} [AddGroup G] :
Nat.card ↥⊤ = Nat.card G
source
theorem Subgroup.card_top {G : Type u_1} [Group G] :
Nat.card ↥⊤ = Nat.card G
source
theorem AddSubgroup.eq_of_le_of_card_ge {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [Finite ↥K] (hle : H ≤ K) (hcard : Nat.card ↥K ≤ Nat.card ↥H) :
H = K
source
theorem Subgroup.eq_of_le_of_card_ge {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite ↥K] (hle : H ≤ K) (hcard : Nat.card ↥K ≤ Nat.card ↥H) :
H = K
source
theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite G] (h : Nat.card G ≤ Nat.card ↥H) :
H = ⊤
source
theorem Subgroup.eq_top_of_le_card {G : Type u_1} [Group G] (H : Subgroup G) [Finite G] (h : Nat.card G ≤ Nat.card ↥H) :
H = ⊤
source
theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] (h : Nat.card ↥H = Nat.card G) :
H = ⊤
source
theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] (h : Nat.card ↥H = Nat.card G) :
H = ⊤
source
@[simp]
theorem AddSubgroup.card_eq_iff_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] :
Nat.card ↥H = Nat.card G ↔ H = ⊤
source
@[simp]
theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] :
Nat.card ↥H = Nat.card G ↔ H = ⊤
source
theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] (h : Nat.card ↥H ≤ 1) :
H = ⊥
source
theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] (h : Nat.card ↥H ≤ 1) :
H = ⊥
source
theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (h : Nat.card ↥H = 1) :
H = ⊥
source
theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) (h : Nat.card ↥H = 1) :
H = ⊥
source
theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] :
Nat.card ↥H ≤ 1 ↔ H = ⊥
source
theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] :
Nat.card ↥H ≤ 1 ↔ H = ⊥
source
theorem AddSubgroup.eq_bot_iff_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
H = ⊥ ↔ Nat.card ↥H = 1
source
theorem Subgroup.eq_bot_iff_card {G : Type u_1} [Group G] (H : Subgroup G) :
H = ⊥ ↔ Nat.card ↥H = 1
source
theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite ↥H] :
1 < Nat.card ↥H ↔ H ≠ ⊥
source
theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) [Finite ↥H] :
1 < Nat.card ↥H ↔ H ≠ ⊥
source
theorem AddSubgroup.card_le_card_addGroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Finite G] :
Nat.card ↥H ≤ Nat.card G
source
theorem Subgroup.card_le_card_group {G : Type u_1} [Group G] (H : Subgroup G) [Finite G] :
Nat.card ↥H ≤ Nat.card G
source
theorem AddSubgroup.card_le_of_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [Finite ↥K] (h : H ≤ K) :
Nat.card ↥H ≤ Nat.card ↥K
source
theorem Subgroup.card_le_of_le {G : Type u_1} [Group G] {H : Subgroup G} {K : Subgroup G} [Finite ↥K] (h : H ≤ K) :
Nat.card ↥H ≤ Nat.card ↥K
source
theorem AddSubgroup.pi_mem_of_single_mem_aux {η : Type u_3} {f : η → Type u_4} [(i : η) → AddGroup (f i)] [DecidableEq η] (I : Finset η) {H : AddSubgroup ((i : η) → f i)} (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 0) (h2 : ∀ i ∈ I, Pi.single i (x i) ∈ H) :
x ∈ H
source
theorem Subgroup.pi_mem_of_mulSingle_mem_aux {η : Type u_3} {f : η → Type u_4} [(i : η) → Group (f i)] [DecidableEq η] (I : Finset η) {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i) (h1 : ∀ i ∉ I, x i = 1) (h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) :
x ∈ H
source
theorem AddSubgroup.pi_mem_of_single_mem {η : Type u_3} {f : η → Type u_4} [(i : η) → AddGroup (f i)] [Finite η] [DecidableEq η] {H : AddSubgroup ((i : η) → f i)} (x : (i : η) → f i) (h : ∀ (i : η), Pi.single i (x i) ∈ H) :
x ∈ H
source
theorem Subgroup.pi_mem_of_mulSingle_mem {η : Type u_3} {f : η → Type u_4} [(i : η) → Group (f i)] [Finite η] [DecidableEq η] {H : Subgroup ((i : η) → f i)} (x : (i : η) → f i) (h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H) :
x ∈ H
source
theorem AddSubgroup.pi_le_iff {η : Type u_3} {f : η → Type u_4} [(i : η) → AddGroup (f i)] [DecidableEq η] [Finite η] {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} :
AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.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.pi_le_iff {η : Type u_3} {f : η → Type u_4} [(i : η) → Group (f i)] [DecidableEq η] [Finite η] {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} :
Subgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), Subgroup.map (MonoidHom.mulSingle f i) (H i) ≤ J

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

source
theorem Subgroup.mem_normalizer_fintype {G : Type u_1} [Group G] {S : Set G} [Finite ↑S] {x : G} (h : ∀ n ∈ S, x * n * x⁻¹ ∈ S) :
x ∈ Subgroup.setNormalizer S
source
instance AddMonoidHom.decidableMemRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) [Fintype G] [DecidableEq N] :
DecidablePred fun (x : N) => x ∈ f.range
Equations
  • f.decidableMemRange x = Fintype.decidableExistsFintype
source
instance MonoidHom.decidableMemRange {G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) [Fintype G] [DecidableEq N] :
DecidablePred fun (x : N) => x ∈ f.range
Equations
  • f.decidableMemRange x = Fintype.decidableExistsFintype
source
instance AddMonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] [Fintype M] [DecidableEq N] (f : M →+ N) :
Fintype ↥(AddMonoidHom.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
instance MonoidHom.fintypeMrange {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] [Fintype M] [DecidableEq N] (f : M →* N) :
Fintype ↥(MonoidHom.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
instance AddMonoidHom.fintypeRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] [Fintype G] [DecidableEq 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
source
instance MonoidHom.fintypeRange {G : Type u_1} [Group G] {N : Type u_3} [Group N] [Fintype G] [DecidableEq 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