Subgroups #
This file provides some result on multiplicative and additive subgroups in the finite context.
Tags #
subgroup, subgroups
instance
AddSubgroup.instFintypeSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
[DecidablePred fun (x : G) => x ∈ K]
[Fintype G]
:
Fintype ↥K
Equations
- AddSubgroup.instFintypeSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup K = let_fun this := inferInstance; this
instance
Subgroup.instFintypeSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup
{G : Type u_1}
[Group G]
(K : Subgroup G)
[DecidablePred fun (x : G) => x ∈ K]
[Fintype G]
:
Fintype ↥K
Equations
- Subgroup.instFintypeSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup K = let_fun this := inferInstance; this
instance
AddSubgroup.instFiniteSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
[Finite G]
:
Finite ↥K
Equations
- ⋯ = ⋯
Conversion to/from Additive/Multiplicative #
Sum of a list of elements in an AddSubgroup is in the AddSubgroup.
theorem
AddSubgroup.multiset_sum_mem
{G : Type u_3}
[AddCommGroup G]
(K : AddSubgroup G)
(g : Multiset G)
:
(∀ a ∈ g, a ∈ K) → Multiset.sum g ∈ K
Sum of a multiset of elements in an AddSubgroup of an AddCommGroup is in
the AddSubgroup.
theorem
Subgroup.multiset_prod_mem
{G : Type u_3}
[CommGroup G]
(K : Subgroup G)
(g : Multiset G)
:
(∀ a ∈ g, a ∈ K) → Multiset.prod g ∈ K
Product of a multiset of elements in a subgroup of a CommGroup is in the subgroup.
theorem
AddSubgroup.multiset_noncommSum_mem
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
(g : Multiset G)
(comm : Set.Pairwise {x : G | x ∈ g} AddCommute)
:
(∀ a ∈ g, a ∈ K) → Multiset.noncommSum g comm ∈ K
theorem
Subgroup.multiset_noncommProd_mem
{G : Type u_1}
[Group G]
(K : Subgroup G)
(g : Multiset G)
(comm : Set.Pairwise {x : G | x ∈ g} Commute)
:
(∀ a ∈ g, a ∈ K) → Multiset.noncommProd g comm ∈ K
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)
:
(Finset.sum t fun (c : ι) => f c) ∈ K
Sum of elements in an AddSubgroup of an AddCommGroup indexed by a Finset
is in the AddSubgroup.
theorem
AddSubgroup.noncommSum_mem
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
{ι : Type u_3}
{t : Finset ι}
{f : ι → G}
(comm : Set.Pairwise ↑t fun (a b : ι) => AddCommute (f a) (f b))
:
(∀ c ∈ t, f c ∈ K) → Finset.noncommSum t f comm ∈ K
theorem
Subgroup.noncommProd_mem
{G : Type u_1}
[Group G]
(K : Subgroup G)
{ι : Type u_3}
{t : Finset ι}
{f : ι → G}
(comm : Set.Pairwise ↑t fun (a b : ι) => Commute (f a) (f b))
:
(∀ c ∈ t, f c ∈ K) → Finset.noncommProd t f comm ∈ K
@[simp]
@[simp]
theorem
AddSubgroup.val_multiset_sum
{G : Type u_3}
[AddCommGroup G]
(H : AddSubgroup G)
(m : Multiset ↥H)
:
↑(Multiset.sum m) = Multiset.sum (Multiset.map Subtype.val m)
@[simp]
theorem
Subgroup.val_multiset_prod
{G : Type u_3}
[CommGroup G]
(H : Subgroup G)
(m : Multiset ↥H)
:
↑(Multiset.prod m) = Multiset.prod (Multiset.map Subtype.val m)
@[simp]
theorem
AddSubgroup.val_finset_sum
{ι : Type u_3}
{G : Type u_4}
[AddCommGroup G]
(H : AddSubgroup G)
(f : ι → ↥H)
(s : Finset ι)
:
↑(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => ↑(f i)
@[simp]
theorem
Subgroup.val_finset_prod
{ι : Type u_3}
{G : Type u_4}
[CommGroup G]
(H : Subgroup G)
(f : ι → ↥H)
(s : Finset ι)
:
↑(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => ↑(f i)
theorem
AddSubgroup.eq_top_of_card_eq
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
[Fintype G]
(h : Fintype.card ↥H = Fintype.card G)
:
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)
:
@[simp]
theorem
AddSubgroup.card_eq_iff_eq_top
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
[Fintype G]
:
Fintype.card ↥H = Fintype.card G ↔ H = ⊤
@[simp]
theorem
Subgroup.card_eq_iff_eq_top
{G : Type u_1}
[Group G]
(H : Subgroup G)
[Fintype ↥H]
[Fintype G]
:
Fintype.card ↥H = Fintype.card G ↔ H = ⊤
theorem
AddSubgroup.eq_top_of_le_card
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
[Fintype G]
(h : Fintype.card G ≤ Fintype.card ↥H)
:
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)
:
theorem
AddSubgroup.eq_bot_of_card_le
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
(h : Fintype.card ↥H ≤ 1)
:
theorem
Subgroup.eq_bot_of_card_le
{G : Type u_1}
[Group G]
(H : Subgroup G)
[Fintype ↥H]
(h : Fintype.card ↥H ≤ 1)
:
theorem
AddSubgroup.eq_bot_of_card_eq
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
(h : Fintype.card ↥H = 1)
:
theorem
Subgroup.eq_bot_of_card_eq
{G : Type u_1}
[Group G]
(H : Subgroup G)
[Fintype ↥H]
(h : Fintype.card ↥H = 1)
:
theorem
AddSubgroup.card_le_one_iff_eq_bot
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
:
Fintype.card ↥H ≤ 1 ↔ H = ⊥
theorem
AddSubgroup.eq_bot_iff_card
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
:
H = ⊥ ↔ Fintype.card ↥H = 1
theorem
AddSubgroup.one_lt_card_iff_ne_bot
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype ↥H]
:
1 < Fintype.card ↥H ↔ H ≠ ⊥
theorem
AddSubgroup.card_le_card_addGroup
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[Fintype G]
[Fintype ↥H]
:
Fintype.card ↥H ≤ Fintype.card G
theorem
Subgroup.card_le_card_group
{G : Type u_1}
[Group G]
(H : Subgroup G)
[Fintype G]
[Fintype ↥H]
:
Fintype.card ↥H ≤ Fintype.card G
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
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
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
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
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.
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.single f i) (H i) ≤ J
For finite index types, the Subgroup.pi is generated by the embeddings of the groups.
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 ∈ AddMonoidHom.range f
Equations
- AddMonoidHom.decidableMemRange f x = Fintype.decidableExistsFintype
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 ∈ MonoidHom.range f
Equations
- MonoidHom.decidableMemRange f x = Fintype.decidableExistsFintype
instance
AddMonoidHom.fintypeMrange
{M : Type u_4}
{N : Type u_5}
[AddMonoid M]
[AddMonoid N]
[Fintype M]
[DecidableEq N]
(f : M →+ N)
:
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
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
instance
AddMonoidHom.fintypeRange
{G : Type u_1}
[AddGroup G]
{N : Type u_3}
[AddGroup N]
[Fintype G]
[DecidableEq N]
(f : G →+ N)
:
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
instance
MonoidHom.fintypeRange
{G : Type u_1}
[Group G]
{N : Type u_3}
[Group N]
[Fintype G]
[DecidableEq N]
(f : G →* N)
:
Fintype ↥(MonoidHom.range f)
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.