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

• (_ : Finite ↥K) = (_ : Finite ↥K)

instance Subgroup.instFiniteSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup {G : Type u_1} [Group G] (K : Subgroup G) [Finite G] : Finite ↥K

Equations

• (_ : Finite ↥K) = (_ : Finite ↥K)

Conversion to/from Additive/Multiplicative

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

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

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

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

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 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) : (Finset.prod t fun (c : ι) => f c) ∈ K

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

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]

theorem AddSubgroup.val_list_sum {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (l : List ↥H) : ↑(List.sum l) = List.sum (List.map Subtype.val l)

@[simp]

theorem Subgroup.val_list_prod {G : Type u_1} [Group G] (H : Subgroup G) (l : List ↥H) : ↑(List.prod l) = List.prod (List.map Subtype.val l)

@[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.fintypeBot.proof_1 {G : Type u_1} [AddGroup G] : ∀ (x : ↥⊥), x ∈ {0}

instance AddSubgroup.fintypeBot {G : Type u_1} [AddGroup G] : Fintype ↥⊥

Equations

• AddSubgroup.fintypeBot = { elems := {0}, complete := (_ : ∀ (x : ↥⊥), x ∈ {0}) }

instance Subgroup.fintypeBot {G : Type u_1} [Group G] : Fintype ↥⊥

Equations

• Subgroup.fintypeBot = { elems := {1}, complete := (_ : ∀ (x : ↥⊥), x ∈ {1}) }

abbrev AddSubgroup.card_bot.match_1 {G : Type u_1} [AddGroup G] (motive : ↥⊥ → Prop) : ∀ (x : ↥⊥), (∀ (_y : G) (hy : _y ∈ ⊥), motive { val := _y, property := hy }) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem AddSubgroup.card_bot {G : Type u_1} [AddGroup G] : ∀ {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1

theorem Subgroup.card_bot {G : Type u_1} [Group G] : ∀ {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1

theorem AddSubgroup.card_top {G : Type u_1} [AddGroup G] [Fintype G] : Fintype.card ↥⊤ = Fintype.card G

theorem Subgroup.card_top {G : Type u_1} [Group G] [Fintype G] : Fintype.card ↥⊤ = Fintype.card G

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) : H = ⊤

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 = ⊤

@[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) : 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) : H = ⊤

theorem AddSubgroup.eq_bot_of_card_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype ↥H] (h : Fintype.card ↥H ≤ 1) : H = ⊥

theorem Subgroup.eq_bot_of_card_le {G : Type u_1} [Group G] (H : Subgroup G) [Fintype ↥H] (h : Fintype.card ↥H ≤ 1) : H = ⊥

theorem AddSubgroup.eq_bot_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype ↥H] (h : Fintype.card ↥H = 1) : H = ⊥

theorem Subgroup.eq_bot_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Fintype ↥H] (h : Fintype.card ↥H = 1) : H = ⊥

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 Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [Group G] (H : Subgroup 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 Subgroup.eq_bot_iff_card {G : Type u_1} [Group G] (H : Subgroup 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 Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup 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.

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

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) : 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

• AddMonoidHom.fintypeMrange f = Set.fintypeRange ⇑f

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

• MonoidHom.fintypeMrange f = Set.fintypeRange ⇑f

instance AddMonoidHom.fintypeRange {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] [Fintype G] [DecidableEq N] (f : G →+ N) : Fintype ↥(AddMonoidHom.range f)

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

• AddMonoidHom.fintypeRange f = Set.fintypeRange ⇑f

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.

Equations

• MonoidHom.fintypeRange f = Set.fintypeRange ⇑f