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 => x ∈ K] [Fintype G] : Fintype { x // x ∈ 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 => x ∈ K] [Fintype G] : Fintype { x // x ∈ 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 { x // x ∈ K }

Equations

• @AddSubgroup.instFiniteSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup = @AddSubgroup.instFiniteSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup.proof_1

theorem AddSubgroup.instFiniteSubtypeMemAddSubgroupInstMembershipInstSetLikeAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] (K : AddSubgroup G) [Finite G] : Finite { x // x ∈ K }

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

Equations

• @Subgroup.instFiniteSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup = @Subgroup.instFiniteSubtypeMemSubgroupInstMembershipInstSetLikeSubgroup.proof_1

Conversion to/from Additive/Multiplicative

theorem AddSubgroup.list_sum_mem {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {l : List G} : (∀ (x : 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 : 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 ∈ 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 ∈ 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 | x ∈ g} AddCommute) : (∀ (a : G), 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 | x ∈ g} Commute) : (∀ (a : G), 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 : ι), 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 : ι), 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 : ι), 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 : ι), 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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 : ι → { x // x ∈ 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 : ι → { x // x ∈ 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 // x ∈ ⊥ }), x ∈ {0}

instance AddSubgroup.fintypeBot {G : Type u_1} [AddGroup G] : Fintype { x // x ∈ ⊥ }

Equations

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

instance Subgroup.fintypeBot {G : Type u_1} [Group G] : Fintype { x // x ∈ ⊥ }

Equations

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

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

Equations

• AddSubgroup.card_bot.match_1 motive x h_1 = Subtype.casesOn x fun val property => h_1 val property

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

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

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

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

theorem AddSubgroup.eq_top_of_card_eq {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype { x // x ∈ H }] [Fintype G] (h : Fintype.card { x // x ∈ H } = Fintype.card G) : H = ⊤

theorem Subgroup.eq_top_of_card_eq {G : Type u_1} [Group G] (H : Subgroup G) [Fintype { x // x ∈ H }] [Fintype G] (h : Fintype.card { x // x ∈ H } = Fintype.card G) : H = ⊤

@[simp]

theorem AddSubgroup.card_eq_iff_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype { x // x ∈ H }] [Fintype G] : Fintype.card { x // x ∈ H } = Fintype.card G ↔ H = ⊤

@[simp]

theorem Subgroup.card_eq_iff_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [Fintype { x // x ∈ H }] [Fintype G] : Fintype.card { x // x ∈ H } = Fintype.card G ↔ H = ⊤

theorem AddSubgroup.eq_top_of_le_card {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype { x // x ∈ H }] [Fintype G] (h : Fintype.card G ≤ Fintype.card { x // x ∈ H }) : H = ⊤

theorem Subgroup.eq_top_of_le_card {G : Type u_1} [Group G] (H : Subgroup G) [Fintype { x // x ∈ H }] [Fintype G] (h : Fintype.card G ≤ Fintype.card { x // x ∈ H }) : H = ⊤

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

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

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

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

theorem AddSubgroup.card_le_one_iff_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype { x // x ∈ H }] : Fintype.card { x // x ∈ H } ≤ 1 ↔ H = ⊥

theorem Subgroup.card_le_one_iff_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) [Fintype { x // x ∈ H }] : Fintype.card { x // x ∈ H } ≤ 1 ↔ H = ⊥

theorem AddSubgroup.one_lt_card_iff_ne_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype { x // x ∈ H }] : 1 < Fintype.card { x // x ∈ H } ↔ H ≠ ⊥

theorem Subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [Group G] (H : Subgroup G) [Fintype { x // x ∈ H }] : 1 < Fintype.card { x // x ∈ H } ↔ H ≠ ⊥

theorem AddSubgroup.card_le_card_addGroup {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [Fintype G] [Fintype { x // x ∈ H }] : Fintype.card { x // x ∈ H } ≤ Fintype.card G

theorem Subgroup.card_le_card_group {G : Type u_1} [Group G] (H : Subgroup G) [Fintype G] [Fintype { x // x ∈ H }] : Fintype.card { x // x ∈ 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 ∈ I → x i = 0) (h2 : ∀ (i : η), 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 ∈ I → x i = 1) (h2 : ∀ (i : η), 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 : G), 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 => 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 => 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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