Basic results on subgroups

We prove basic results on the definitions of subgroups. The bundled subgroups use bundled monoid homomorphisms.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions

Notation used here:

• G N are Groups

• A is an AddGroup

• H K are Subgroups of G or AddSubgroups of A

• x is an element of type G or type A

• f g : N →* G are group homomorphisms

• s k are sets of elements of type G

Definitions in the file:

• Subgroup.prod H K : the product of subgroups H, K of groups G, N respectively, H × K is a subgroup of G × N

Implementation notes

Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as membership of a subgroup's underlying set.

Tags

subgroup, subgroups

theorem div_mem_comm_iff {G : Type u_1} [Group G] {S : Type u_6} {H : S} [SetLike S G] [SubgroupClass S G] {a b : G} : a / b ∈ H ↔ b / a ∈ H

theorem sub_mem_comm_iff {G : Type u_1} [AddGroup G] {S : Type u_6} {H : S} [SetLike S G] [AddSubgroupClass S G] {a b : G} : a - b ∈ H ↔ b - a ∈ H

theorem Subgroup.div_mem_comm_iff {G : Type u_1} [Group G] (H : Subgroup G) {a b : G} : a / b ∈ H ↔ b / a ∈ H

theorem AddSubgroup.sub_mem_comm_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {a b : G} : a - b ∈ H ↔ b - a ∈ H

def Subgroup.prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : Subgroup (G × N)

Given Subgroups H, K of groups G, N respectively, H × K as a subgroup of G × N.

Equations

• H.prod K = { toSubmonoid := H.prod K.toSubmonoid, inv_mem' := ⋯ }

def AddSubgroup.prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : AddSubgroup (G × N)

Given AddSubgroups H, K of AddGroups A, B respectively, H × K as an AddSubgroup of A × B.

Equations

• H.prod K = { toAddSubmonoid := H.prod K.toAddSubmonoid, neg_mem' := ⋯ }

theorem Subgroup.coe_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : ↑(H.prod K) = ↑H ×ˢ ↑K

theorem AddSubgroup.coe_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ↑(H.prod K) = ↑H ×ˢ ↑K

theorem Subgroup.mem_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K

theorem AddSubgroup.mem_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {p : G × N} : p ∈ H.prod K ↔ p.1 ∈ H ∧ p.2 ∈ K

theorem Subgroup.prod_mono {G : Type u_1} [Group G] {N : Type u_5} [Group N] : Relator.LiftFun (fun (x1 x2 : Subgroup G) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : Subgroup N) => x1 ≤ x2) fun (x1 x2 : Subgroup (G × N)) => x1 ≤ x2) prod prod

theorem AddSubgroup.prod_mono {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : Relator.LiftFun (fun (x1 x2 : AddSubgroup G) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : AddSubgroup N) => x1 ≤ x2) fun (x1 x2 : AddSubgroup (G × N)) => x1 ≤ x2) prod prod

theorem Subgroup.prod_mono_right {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) : Monotone fun (t : Subgroup N) => K.prod t

theorem AddSubgroup.prod_mono_right {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) : Monotone fun (t : AddSubgroup N) => K.prod t

theorem Subgroup.prod_mono_left {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) : Monotone fun (K : Subgroup G) => K.prod H

theorem AddSubgroup.prod_mono_left {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) : Monotone fun (K : AddSubgroup G) => K.prod H

theorem Subgroup.prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) : K.prod ⊤ = comap (MonoidHom.fst G N) K

theorem AddSubgroup.prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) : K.prod ⊤ = comap (AddMonoidHom.fst G N) K

theorem Subgroup.top_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup N) : ⊤.prod H = comap (MonoidHom.snd G N) H

theorem AddSubgroup.top_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup N) : ⊤.prod H = comap (AddMonoidHom.snd G N) H

@[simp]

theorem Subgroup.top_prod_top {G : Type u_1} [Group G] {N : Type u_5} [Group N] : ⊤.prod ⊤ = ⊤

@[simp]

theorem AddSubgroup.top_prod_top {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ⊤.prod ⊤ = ⊤

@[simp]

theorem Subgroup.bot_prod_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] : ⊥.prod ⊥ = ⊥

@[simp]

theorem AddSubgroup.bot_prod_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ⊥.prod ⊥ = ⊥

@[deprecated AddSubgroup.bot_prod_bot (since := "2025-03-11")]

theorem AddSubgroup.bot_sum_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : ⊥.prod ⊥ = ⊥

Alias of AddSubgroup.bot_prod_bot.

theorem Subgroup.le_prod_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : J ≤ H.prod K ↔ map (MonoidHom.fst G N) J ≤ H ∧ map (MonoidHom.snd G N) J ≤ K

theorem AddSubgroup.le_prod_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : J ≤ H.prod K ↔ map (AddMonoidHom.fst G N) J ≤ H ∧ map (AddMonoidHom.snd G N) J ≤ K

theorem Subgroup.prod_le_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} {J : Subgroup (G × N)} : H.prod K ≤ J ↔ map (MonoidHom.inl G N) H ≤ J ∧ map (MonoidHom.inr G N) K ≤ J

theorem AddSubgroup.prod_le_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : H.prod K ≤ J ↔ map (AddMonoidHom.inl G N) H ≤ J ∧ map (AddMonoidHom.inr G N) K ≤ J

@[simp]

theorem Subgroup.prod_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} {K : Subgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

@[simp]

theorem AddSubgroup.prod_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} : H.prod K = ⊥ ↔ H = ⊥ ∧ K = ⊥

theorem Subgroup.closure_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) : closure (s ×ˢ t) = (closure s).prod (closure t)

theorem AddSubgroup.closure_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {s : Set G} {t : Set N} (hs : 0 ∈ s) (ht : 0 ∈ t) : closure (s ×ˢ t) = (closure s).prod (closure t)

def Subgroup.prodEquiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) : ↥(H.prod K) ≃* ↥H × ↥K

Product of subgroups is isomorphic to their product as groups.

Equations

• H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_mul' := ⋯ }

def AddSubgroup.prodEquiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) : ↥(H.prod K) ≃+ ↥H × ↥K

Product of additive subgroups is isomorphic to their product as additive groups

Equations

• H.prodEquiv K = { toEquiv := Equiv.Set.prod ↑H ↑K, map_add' := ⋯ }

def Submonoid.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → MulOneClass (f i)] (I : Set η) (s : (i : η) → Submonoid (f i)) : Submonoid ((i : η) → f i)

A version of Set.pi for submonoids. Given an index set I and a family of submodules s : Π i, Submonoid f i, pi I s is the submonoid of dependent functions f : Π i, f i such that f i belongs to Pi I s whenever i ∈ I.

Equations

• Submonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, mul_mem' := ⋯, one_mem' := ⋯ }

def AddSubmonoid.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddZeroClass (f i)] (I : Set η) (s : (i : η) → AddSubmonoid (f i)) : AddSubmonoid ((i : η) → f i)

A version of Set.pi for AddSubmonoids. Given an index set I and a family of submodules s : Π i, AddSubmonoid f i, pi I s is the AddSubmonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations

• AddSubmonoid.pi I s = { carrier := I.pi fun (i : η) => (s i).carrier, add_mem' := ⋯, zero_mem' := ⋯ }

def Subgroup.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) : Subgroup ((i : η) → f i)

A version of Set.pi for subgroups. Given an index set I and a family of submodules s : Π i, Subgroup f i, pi I s is the subgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations

• Subgroup.pi I H = { toSubmonoid := Submonoid.pi I fun (i : η) => (H i).toSubmonoid, inv_mem' := ⋯ }

def AddSubgroup.pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) : AddSubgroup ((i : η) → f i)

A version of Set.pi for AddSubgroups. Given an index set I and a family of submodules s : Π i, AddSubgroup f i, pi I s is the AddSubgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations

• AddSubgroup.pi I H = { toAddSubmonoid := AddSubmonoid.pi I fun (i : η) => (H i).toAddSubmonoid, neg_mem' := ⋯ }

theorem Subgroup.coe_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) (H : (i : η) → Subgroup (f i)) : ↑(pi I H) = I.pi fun (i : η) => ↑(H i)

theorem AddSubgroup.coe_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) (H : (i : η) → AddSubgroup (f i)) : ↑(pi I H) = I.pi fun (i : η) => ↑(H i)

theorem Subgroup.mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)} {p : (i : η) → f i} : p ∈ pi I H ↔ ∀ i ∈ I, p i ∈ H i

theorem AddSubgroup.mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) {H : (i : η) → AddSubgroup (f i)} {p : (i : η) → f i} : p ∈ pi I H ↔ ∀ i ∈ I, p i ∈ H i

theorem Subgroup.pi_top {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (I : Set η) : (pi I fun (i : η) => ⊤) = ⊤

theorem AddSubgroup.pi_top {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (I : Set η) : (pi I fun (i : η) => ⊤) = ⊤

theorem Subgroup.pi_empty {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) : pi ∅ H = ⊤

theorem AddSubgroup.pi_empty {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) : pi ∅ H = ⊤

theorem Subgroup.pi_bot {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] : (pi Set.univ fun (i : η) => ⊥) = ⊥

theorem AddSubgroup.pi_bot {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] : (pi Set.univ fun (i : η) => ⊥) = ⊥

theorem Subgroup.le_pi_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] {I : Set η} {H : (i : η) → Subgroup (f i)} {J : Subgroup ((i : η) → f i)} : J ≤ pi I H ↔ ∀ i ∈ I, map (Pi.evalMonoidHom f i) J ≤ H i

theorem AddSubgroup.le_pi_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] {I : Set η} {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} : J ≤ pi I H ↔ ∀ i ∈ I, map (Pi.evalAddMonoidHom f i) J ≤ H i

@[simp]

theorem Subgroup.mulSingle_mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → Subgroup (f i)} (i : η) (x : f i) : Pi.mulSingle i x ∈ pi I H ↔ i ∈ I → x ∈ H i

@[simp]

theorem AddSubgroup.single_mem_pi {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] [DecidableEq η] {I : Set η} {H : (i : η) → AddSubgroup (f i)} (i : η) (x : f i) : Pi.single i x ∈ pi I H ↔ i ∈ I → x ∈ H i

theorem Subgroup.pi_eq_bot_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → Group (f i)] (H : (i : η) → Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

theorem AddSubgroup.pi_eq_bot_iff {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] (H : (i : η) → AddSubgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

class Subgroup.Characteristic {G : Type u_1} [Group G] (H : Subgroup G) : Prop

A subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

• fixed (ϕ : G ≃* G) : comap ϕ.toMonoidHom H = H

  H is fixed by all automorphisms

@[instance 100]

instance Subgroup.normal_of_characteristic {G : Type u_1} [Group G] (H : Subgroup G) [h : H.Characteristic] : H.Normal

class AddSubgroup.Characteristic {A : Type u_4} [AddGroup A] (H : AddSubgroup A) : Prop

An AddSubgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form Characteristic.iff...

• fixed (ϕ : A ≃+ A) : comap ϕ.toAddMonoidHom H = H

  H is fixed by all automorphisms

@[instance 100]

instance AddSubgroup.normal_of_characteristic {A : Type u_4} [AddGroup A] (H : AddSubgroup A) [h : H.Characteristic] : H.Normal

theorem Subgroup.characteristic_iff_comap_eq {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom H = H

theorem AddSubgroup.characteristic_iff_comap_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), comap ϕ.toAddMonoidHom H = H

theorem Subgroup.characteristic_iff_comap_le {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom H ≤ H

theorem AddSubgroup.characteristic_iff_comap_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), comap ϕ.toAddMonoidHom H ≤ H

theorem Subgroup.characteristic_iff_le_comap {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.toMonoidHom H

theorem AddSubgroup.characteristic_iff_le_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ comap ϕ.toAddMonoidHom H

theorem Subgroup.characteristic_iff_map_eq {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

theorem AddSubgroup.characteristic_iff_map_eq {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), map ϕ.toAddMonoidHom H = H

theorem Subgroup.characteristic_iff_map_le {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

theorem AddSubgroup.characteristic_iff_map_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), map ϕ.toAddMonoidHom H ≤ H

theorem Subgroup.characteristic_iff_le_map {G : Type u_1} [Group G] {H : Subgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

theorem AddSubgroup.characteristic_iff_le_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ map ϕ.toAddMonoidHom H

instance Subgroup.botCharacteristic {G : Type u_1} [Group G] : ⊥.Characteristic

instance AddSubgroup.botCharacteristic {G : Type u_1} [AddGroup G] : ⊥.Characteristic

instance Subgroup.topCharacteristic {G : Type u_1} [Group G] : ⊤.Characteristic

instance AddSubgroup.topCharacteristic {G : Type u_1} [AddGroup G] : ⊤.Characteristic

theorem Subgroup.normalizer_eq_top_iff {G : Type u_1} [Group G] {H : Subgroup G} : H.normalizer = ⊤ ↔ H.Normal

theorem AddSubgroup.normalizer_eq_top_iff {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.normalizer = ⊤ ↔ H.Normal

theorem Subgroup.normalizer_eq_top {G : Type u_1} [Group G] (H : Subgroup G) [h : H.Normal] : H.normalizer = ⊤

theorem AddSubgroup.normalizer_eq_top {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [h : H.Normal] : H.normalizer = ⊤

theorem Subgroup.le_normalizer_comap {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] (f : N →* G) : comap f H.normalizer ≤ (comap f H).normalizer

The preimage of the normalizer is contained in the normalizer of the preimage.

theorem AddSubgroup.le_normalizer_comap {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : N →+ G) : comap f H.normalizer ≤ (comap f H).normalizer

The preimage of the normalizer is contained in the normalizer of the preimage.

theorem Subgroup.le_normalizer_map {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] (f : G →* N) : map f H.normalizer ≤ (map f H).normalizer

The image of the normalizer is contained in the normalizer of the image.

theorem AddSubgroup.le_normalizer_map {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : G →+ N) : map f H.normalizer ≤ (map f H).normalizer

The image of the normalizer is contained in the normalizer of the image.

theorem Subgroup.comap_normalizer_eq_of_le_range {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] {f : N →* G} (h : H ≤ f.range) : comap f H.normalizer = (comap f H).normalizer

theorem AddSubgroup.comap_normalizer_eq_of_le_range {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] {f : N →+ G} (h : H ≤ f.range) : comap f H.normalizer = (comap f H).normalizer

theorem Subgroup.subgroupOf_normalizer_eq {G : Type u_1} [Group G] {H N : Subgroup G} (h : H ≤ N) : H.normalizer.subgroupOf N = (H.subgroupOf N).normalizer

theorem AddSubgroup.addSubgroupOf_normalizer_eq {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} (h : H ≤ N) : H.normalizer.addSubgroupOf N = (H.addSubgroupOf N).normalizer

theorem Subgroup.normal_subgroupOf_iff_le_normalizer {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : (H.subgroupOf K).Normal ↔ K ≤ H.normalizer

theorem AddSubgroup.normal_addSubgroupOf_iff_le_normalizer {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : (H.addSubgroupOf K).Normal ↔ K ≤ H.normalizer

theorem Subgroup.normal_subgroupOf_iff_le_normalizer_inf {G : Type u_1} [Group G] {H K : Subgroup G} : (H.subgroupOf K).Normal ↔ K ≤ (H ⊓ K).normalizer

theorem AddSubgroup.normal_addSubgroupOf_iff_le_normalizer_inf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : (H.addSubgroupOf K).Normal ↔ K ≤ (H ⊓ K).normalizer

@[instance 100]

instance Subgroup.normal_in_normalizer {G : Type u_1} [Group G] {H : Subgroup G} : (H.subgroupOf H.normalizer).Normal

@[instance 100]

instance AddSubgroup.normal_in_normalizer {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : (H.addSubgroupOf H.normalizer).Normal

theorem Subgroup.le_normalizer_of_normal_subgroupOf {G : Type u_1} [Group G] {H K : Subgroup G} [hK : (H.subgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer

theorem AddSubgroup.le_normalizer_of_normal_addSubgroupOf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [hK : (H.addSubgroupOf K).Normal] (HK : H ≤ K) : K ≤ H.normalizer

theorem Subgroup.subset_normalizer_of_normal {G : Type u_1} [Group G] {H : Subgroup G} {S : Set G} [hH : H.Normal] : S ⊆ ↑H.normalizer

theorem AddSubgroup.subset_normalizer_of_normal {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {S : Set G} [hH : H.Normal] : S ⊆ ↑H.normalizer

theorem Subgroup.le_normalizer_of_normal {G : Type u_1} [Group G] {H K : Subgroup G} [H.Normal] : K ≤ H.normalizer

theorem AddSubgroup.le_normalizer_of_normal {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} [H.Normal] : K ≤ H.normalizer

theorem Subgroup.inf_normalizer_le_normalizer_inf {G : Type u_1} [Group G] {H K : Subgroup G} : H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer

theorem AddSubgroup.inf_normalizer_le_normalizer_inf {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} : H.normalizer ⊓ K.normalizer ≤ (H ⊓ K).normalizer

def NormalizerCondition (G : Type u_1) [Group G] : Prop

Every proper subgroup H of G is a proper normal subgroup of the normalizer of H in G.

Equations

• NormalizerCondition G = ∀ H < ⊤, H < H.normalizer

theorem normalizerCondition_iff_only_full_group_self_normalizing {G : Type u_1} [Group G] : NormalizerCondition G ↔ ∀ (H : Subgroup G), H.normalizer = H → H = ⊤

Alternative phrasing of the normalizer condition: Only the full group is self-normalizing. This may be easier to work with, as it avoids inequalities and negations.

def Group.conjugatesOfSet {G : Type u_1} [Group G] (s : Set G) : Set G

Given a set s, conjugatesOfSet s is the set of all conjugates of the elements of s.

Equations

• Group.conjugatesOfSet s = ⋃ a ∈ s, conjugatesOf a

theorem Group.mem_conjugatesOfSet_iff {G : Type u_1} [Group G] {s : Set G} {x : G} : x ∈ conjugatesOfSet s ↔ ∃ a ∈ s, IsConj a x

theorem Group.subset_conjugatesOfSet {G : Type u_1} [Group G] {s : Set G} : s ⊆ conjugatesOfSet s

theorem Group.conjugatesOfSet_mono {G : Type u_1} [Group G] {s t : Set G} (h : s ⊆ t) : conjugatesOfSet s ⊆ conjugatesOfSet t

theorem Group.conjugates_subset_normal {G : Type u_1} [Group G] {N : Subgroup G} [tn : N.Normal] {a : G} (h : a ∈ N) : conjugatesOf a ⊆ ↑N

theorem Group.conjugatesOfSet_subset {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ ↑N) : conjugatesOfSet s ⊆ ↑N

theorem Group.conj_mem_conjugatesOfSet {G : Type u_1} [Group G] {s : Set G} {x c : G} : x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s

The set of conjugates of s is closed under conjugation.

def Subgroup.normalClosure {G : Type u_1} [Group G] (s : Set G) : Subgroup G

The normal closure of a set s is the subgroup closure of all the conjugates of elements of s. It is the smallest normal subgroup containing s.

Equations

• Subgroup.normalClosure s = Subgroup.closure (Group.conjugatesOfSet s)

theorem Subgroup.conjugatesOfSet_subset_normalClosure {G : Type u_1} [Group G] {s : Set G} : Group.conjugatesOfSet s ⊆ ↑(normalClosure s)

theorem Subgroup.subset_normalClosure {G : Type u_1} [Group G] {s : Set G} : s ⊆ ↑(normalClosure s)

theorem Subgroup.le_normalClosure {G : Type u_1} [Group G] {H : Subgroup G} : H ≤ normalClosure ↑H

instance Subgroup.normalClosure_normal {G : Type u_1} [Group G] {s : Set G} : (normalClosure s).Normal

The normal closure of s is a normal subgroup.

theorem Subgroup.normalClosure_le_normal {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] (h : s ⊆ ↑N) : normalClosure s ≤ N

The normal closure of s is the smallest normal subgroup containing s.

theorem Subgroup.normalClosure_subset_iff {G : Type u_1} [Group G] {s : Set G} {N : Subgroup G} [N.Normal] : s ⊆ ↑N ↔ normalClosure s ≤ N

theorem Subgroup.normalClosure_mono {G : Type u_1} [Group G] {s t : Set G} (h : s ⊆ t) : normalClosure s ≤ normalClosure t

theorem Subgroup.normalClosure_eq_iInf {G : Type u_1} [Group G] {s : Set G} : normalClosure s = ⨅ (N : Subgroup G), ⨅ (_ : N.Normal), ⨅ (_ : s ⊆ ↑N), N

@[simp]

theorem Subgroup.normalClosure_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : normalClosure ↑H = H

theorem Subgroup.normalClosure_idempotent {G : Type u_1} [Group G] {s : Set G} : normalClosure ↑(normalClosure s) = normalClosure s

theorem Subgroup.closure_le_normalClosure {G : Type u_1} [Group G] {s : Set G} : closure s ≤ normalClosure s

@[simp]

theorem Subgroup.normalClosure_closure_eq_normalClosure {G : Type u_1} [Group G] {s : Set G} : normalClosure ↑(closure s) = normalClosure s

def Subgroup.normalCore {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup G

The normal core of a subgroup H is the largest normal subgroup of G contained in H, as shown by Subgroup.normalCore_eq_iSup.

Equations

• H.normalCore = { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem Subgroup.normalCore_le {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore ≤ H

instance Subgroup.normalCore_normal {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore.Normal

theorem Subgroup.normal_le_normalCore {G : Type u_1} [Group G] {H N : Subgroup G} [hN : N.Normal] : N ≤ H.normalCore ↔ N ≤ H

theorem Subgroup.normalCore_mono {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : H.normalCore ≤ K.normalCore

theorem Subgroup.normalCore_eq_iSup {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore = ⨆ (N : Subgroup G), ⨆ (_ : N.Normal), ⨆ (_ : N ≤ H), N

@[simp]

theorem Subgroup.normalCore_eq_self {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : H.normalCore = H

theorem Subgroup.normalCore_idempotent {G : Type u_1} [Group G] (H : Subgroup G) : H.normalCore.normalCore = H.normalCore

theorem MonoidHom.prodMap_comap_prod {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') : Subgroup.comap (f.prodMap g) (S.prod S') = (Subgroup.comap f S).prod (Subgroup.comap g S')

theorem AddMonoidHom.prodMap_comap_prod {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N') : AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')

@[deprecated AddMonoidHom.prodMap_comap_prod (since := "2025-03-11")]

theorem AddMonoidHom.sumMap_comap_sum {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') (S : AddSubgroup N) (S' : AddSubgroup N') : AddSubgroup.comap (f.prodMap g) (S.prod S') = (AddSubgroup.comap f S).prod (AddSubgroup.comap g S')

Alias of AddMonoidHom.prodMap_comap_prod.

theorem MonoidHom.ker_prodMap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {G' : Type u_8} {N' : Type u_9} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') : (f.prodMap g).ker = f.ker.prod g.ker

theorem AddMonoidHom.ker_prodMap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') : (f.prodMap g).ker = f.ker.prod g.ker

@[deprecated AddMonoidHom.ker_prodMap (since := "2025-03-11")]

theorem AddMonoidHom.ker_sumMap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {G' : Type u_8} {N' : Type u_9} [AddGroup G'] [AddGroup N'] (f : G →+ N) (g : G' →+ N') : (f.prodMap g).ker = f.ker.prod g.ker

Alias of AddMonoidHom.ker_prodMap.

@[simp]

theorem MonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] : (fst G G').ker = ⊥.prod ⊤

@[simp]

theorem AddMonoidHom.ker_fst {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] : (fst G G').ker = ⊥.prod ⊤

@[simp]

theorem MonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] : (snd G G').ker = ⊤.prod ⊥

@[simp]

theorem AddMonoidHom.ker_snd {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] : (snd G G').ker = ⊤.prod ⊥

theorem Subgroup.Normal.map {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup G} (h : H.Normal) (f : G →* N) (hf : Function.Surjective ⇑f) : (Subgroup.map f H).Normal

theorem AddSubgroup.Normal.map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).Normal

theorem Subgroup.comap_normalizer_eq_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : N →* G} (hf : Function.Surjective ⇑f) : comap f H.normalizer = (comap f H).normalizer

The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

theorem AddSubgroup.comap_normalizer_eq_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : N →+ G} (hf : Function.Surjective ⇑f) : comap f H.normalizer = (comap f H).normalizer

The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

@[deprecated Subgroup.comap_normalizer_eq_of_le_range (since := "2025-03-13")]

theorem Subgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [Group G] {H : Subgroup G} {N : Type u_5} [Group N] {f : N →* G} (h : H ≤ f.range) : comap f H.normalizer = (comap f H).normalizer

Alias of Subgroup.comap_normalizer_eq_of_le_range.

@[deprecated AddSubgroup.comap_normalizer_eq_of_le_range (since := "2025-03-13")]

theorem AddSubgroup.comap_normalizer_eq_of_injective_of_le_range {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] {f : N →+ G} (h : H ≤ f.range) : comap f H.normalizer = (comap f H).normalizer

Alias of AddSubgroup.comap_normalizer_eq_of_le_range.

theorem Subgroup.map_equiv_normalizer_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G ≃* N) : map f.toMonoidHom H.normalizer = (map f.toMonoidHom H).normalizer

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

theorem AddSubgroup.map_equiv_normalizer_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G ≃+ N) : map f.toAddMonoidHom H.normalizer = (map f.toAddMonoidHom H).normalizer

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

theorem Subgroup.map_normalizer_eq_of_bijective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Bijective ⇑f) : map f H.normalizer = (map f H).normalizer

The image of the normalizer is equal to the normalizer of the image of a bijective function.

theorem AddSubgroup.map_normalizer_eq_of_bijective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Bijective ⇑f) : map f H.normalizer = (map f H).normalizer

The image of the normalizer is equal to the normalizer of the image of a bijective function.

def MonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) : G₂ →* G₃

Auxiliary definition used to define liftOfRightInverse

Equations

• f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_one' := ⋯, map_mul' := ⋯ }

def AddMonoidHom.liftOfRightInverseAux {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) : G₂ →+ G₃

Auxiliary definition used to define liftOfRightInverse

Equations

• f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun (b : G₂) => g (f_inv b), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

@[simp]

theorem AddMonoidHom.liftOfRightInverseAux_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (x : G₁) : (f.liftOfRightInverseAux f_inv hf g hg) (f x) = g x

def MonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)

liftOfRightInverse f hf g hg is the unique group homomorphism φ

• such that φ.comp f = g (MonoidHom.liftOfRightInverse_comp),
• where f : G₁ →+* G₂ has a RightInverse f_inv (hf),
• and g : G₂ →+* G₃ satisfies hg : f.ker ≤ g.ker.

See MonoidHom.eq_liftOfRightInverse for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

def AddMonoidHom.liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) : { g : G₁ →+ G₃ // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)

liftOfRightInverse f f_inv hf g hg is the unique additive group homomorphism φ

• such that φ.comp f = g (AddMonoidHom.liftOfRightInverse_comp),
• where f : G₁ →+ G₂ has a RightInverse f_inv (hf),
• and g : G₂ →+ G₃ satisfies hg : f.ker ≤ g.ker. See AddMonoidHom.eq_liftOfRightInverse for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev MonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (hf : Function.Surjective ⇑f) : { g : G₁ →* G₃ // f.ker ≤ g.ker } ≃ (G₂ →* G₃)

A non-computable version of MonoidHom.liftOfRightInverse for when no computable right inverse is available, that uses Function.surjInv.

Equations

• f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

@[reducible, inline]

noncomputable abbrev AddMonoidHom.liftOfSurjective {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f) : { g : G₁ →+ G₃ // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)

A non-computable version of AddMonoidHom.liftOfRightInverse for when no computable right inverse is available.

Equations

• f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯

@[simp]

theorem MonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

@[simp]

theorem AddMonoidHom.liftOfRightInverse_comp_apply {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) (x : G₁) : ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x

@[simp]

theorem MonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

@[simp]

theorem AddMonoidHom.liftOfRightInverse_comp {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g : G₁ →+ G₃ // f.ker ≤ g.ker }) : ((f.liftOfRightInverse f_inv hf) g).comp f = ↑g

theorem MonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [Group G₁] [Group G₂] [Group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem AddMonoidHom.eq_liftOfRightInverse {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [AddGroup G₁] [AddGroup G₂] [AddGroup G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) : h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

theorem Subgroup.Normal.comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (Subgroup.comap f H).Normal

theorem AddSubgroup.Normal.comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} (hH : H.Normal) (f : G →+ N) : (AddSubgroup.comap f H).Normal

@[instance 100]

instance Subgroup.normal_comap {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H : Subgroup N} [nH : H.Normal] (f : G →* N) : (comap f H).Normal

@[instance 100]

instance AddSubgroup.normal_comap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup N} [nH : H.Normal] (f : G →+ N) : (comap f H).Normal

theorem Subgroup.Normal.subgroupOf {G : Type u_1} [Group G] {H : Subgroup G} (hH : H.Normal) (K : Subgroup G) : (H.subgroupOf K).Normal

theorem AddSubgroup.Normal.addSubgroupOf {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (hH : H.Normal) (K : AddSubgroup G) : (H.addSubgroupOf K).Normal

@[instance 100]

instance Subgroup.normal_subgroupOf {G : Type u_1} [Group G] {H N : Subgroup G} [N.Normal] : (N.subgroupOf H).Normal

@[instance 100]

instance AddSubgroup.normal_addSubgroupOf {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} [N.Normal] : (N.addSubgroupOf H).Normal

theorem Subgroup.map_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set G) (f : G →* N) (hf : Function.Surjective ⇑f) : map f (normalClosure s) = normalClosure (⇑f '' s)

theorem Subgroup.comap_normalClosure {G : Type u_1} [Group G] {N : Type u_5} [Group N] (s : Set N) (f : G ≃* N) : normalClosure (⇑f ⁻¹' s) = comap (↑f) (normalClosure s)

theorem Subgroup.Normal.of_map_injective {G : Type u_6} {H : Type u_7} [Group G] [Group H] {φ : G →* H} (hφ : Function.Injective ⇑φ) {L : Subgroup G} (n : (Subgroup.map φ L).Normal) : L.Normal

theorem Subgroup.Normal.of_map_subtype {G : Type u_1} [Group G] {K : Subgroup G} {L : Subgroup ↥K} (n : (Subgroup.map K.subtype L).Normal) : L.Normal

theorem Subgroup.normal_subgroupOf_iff {G : Type u_1} [Group G] {H K : Subgroup G} (hHK : H ≤ K) : (H.subgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k * h * k⁻¹ ∈ H

theorem AddSubgroup.normal_addSubgroupOf_iff {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hHK : H ≤ K) : (H.addSubgroupOf K).Normal ↔ ∀ (h k : G), h ∈ H → k ∈ K → k + h + -k ∈ H

instance Subgroup.prod_subgroupOf_prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] {H₁ K₁ : Subgroup G} {H₂ K₂ : Subgroup N} [h₁ : (H₁.subgroupOf K₁).Normal] [h₂ : (H₂.subgroupOf K₂).Normal] : ((H₁.prod H₂).subgroupOf (K₁.prod K₂)).Normal

instance AddSubgroup.prod_addSubgroupOf_prod_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H₁ K₁ : AddSubgroup G} {H₂ K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal] : ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal

@[deprecated AddSubgroup.prod_addSubgroupOf_prod_normal (since := "2025-03-11")]

theorem AddSubgroup.sum_addSubgroupOf_sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H₁ K₁ : AddSubgroup G} {H₂ K₂ : AddSubgroup N} [h₁ : (H₁.addSubgroupOf K₁).Normal] [h₂ : (H₂.addSubgroupOf K₂).Normal] : ((H₁.prod H₂).addSubgroupOf (K₁.prod K₂)).Normal

Alias of AddSubgroup.prod_addSubgroupOf_prod_normal.

instance Subgroup.prod_normal {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (K : Subgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal

instance AddSubgroup.prod_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal

@[deprecated AddSubgroup.prod_normal (since := "2025-03-11")]

theorem AddSubgroup.sum_normal {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N) [hH : H.Normal] [hK : K.Normal] : (H.prod K).Normal

Alias of AddSubgroup.prod_normal.

theorem Subgroup.inf_subgroupOf_inf_normal_of_right {G : Type u_1} [Group G] (A B' B : Subgroup G) [hN : (B'.subgroupOf B).Normal] : ((A ⊓ B').subgroupOf (A ⊓ B)).Normal

theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_right {G : Type u_1} [AddGroup G] (A B' B : AddSubgroup G) [hN : (B'.addSubgroupOf B).Normal] : ((A ⊓ B').addSubgroupOf (A ⊓ B)).Normal

theorem Subgroup.inf_subgroupOf_inf_normal_of_left {G : Type u_1} [Group G] {A' A : Subgroup G} (B : Subgroup G) [hN : (A'.subgroupOf A).Normal] : ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal

theorem AddSubgroup.inf_addSubgroupOf_inf_normal_of_left {G : Type u_1} [AddGroup G] {A' A : AddSubgroup G} (B : AddSubgroup G) [hN : (A'.addSubgroupOf A).Normal] : ((A' ⊓ B).addSubgroupOf (A ⊓ B)).Normal

instance Subgroup.normal_inf_normal {G : Type u_1} [Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal

instance AddSubgroup.normal_inf_normal {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal

theorem Subgroup.normal_iInf_normal {G : Type u_1} [Group G] {ι : Type u_6} {a : ι → Subgroup G} (norm : ∀ (i : ι), (a i).Normal) : (iInf a).Normal

theorem AddSubgroup.normal_iInf_normal {G : Type u_1} [AddGroup G] {ι : Type u_6} {a : ι → AddSubgroup G} (norm : ∀ (i : ι), (a i).Normal) : (iInf a).Normal

theorem Subgroup.SubgroupNormal.mem_comm {G : Type u_1} [Group G] {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal] {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H

theorem AddSubgroup.SubgroupNormal.mem_comm {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (hK : H ≤ K) [hN : (H.addSubgroupOf K).Normal] {a b : G} (hb : b ∈ K) (h : a + b ∈ H) : b + a ∈ H

theorem Subgroup.commute_of_normal_of_disjoint {G : Type u_1} [Group G] (H₁ H₂ : Subgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : Commute x y

Elements of disjoint, normal subgroups commute.

theorem AddSubgroup.addCommute_of_normal_of_disjoint {G : Type u_1} [AddGroup G] (H₁ H₂ : AddSubgroup G) (hH₁ : H₁.Normal) (hH₂ : H₂.Normal) (hdis : Disjoint H₁ H₂) (x y : G) (hx : x ∈ H₁) (hy : y ∈ H₂) : AddCommute x y

Elements of disjoint, normal subgroups commute.

theorem Subgroup.normal_subgroupOf_of_le_normalizer {G : Type u_1} [Group G] {H N : Subgroup G} (hLE : H ≤ N.normalizer) : (N.subgroupOf H).Normal

theorem AddSubgroup.normal_addSubgroupOf_of_le_normalizer {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} (hLE : H ≤ N.normalizer) : (N.addSubgroupOf H).Normal

theorem Subgroup.normal_subgroupOf_sup_of_le_normalizer {G : Type u_1} [Group G] {H N : Subgroup G} (hLE : H ≤ N.normalizer) : (N.subgroupOf (H ⊔ N)).Normal

theorem AddSubgroup.normal_addSubgroupOf_sup_of_le_normalizer {G : Type u_1} [AddGroup G] {H N : AddSubgroup G} (hLE : H ≤ N.normalizer) : (N.addSubgroupOf (H ⊔ N)).Normal

theorem IsConj.normalClosure_eq_top_of {G : Type u_1} [Group G] {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg : g ∈ N} {hg' : g' ∈ N} (hc : IsConj g g') (ht : Subgroup.normalClosure {⟨g, hg⟩} = ⊤) : Subgroup.normalClosure {⟨g', hg'⟩} = ⊤

def ConjClasses.noncenter (G : Type u_6) [Monoid G] : Set (ConjClasses G)

The conjugacy classes that are not trivial.

Equations

• ConjClasses.noncenter G = {x : ConjClasses G | x.carrier.Nontrivial}

@[simp]

theorem ConjClasses.mem_noncenter {G : Type u_6} [Monoid G] (g : ConjClasses G) : g ∈ noncenter G ↔ g.carrier.Nontrivial

def AddSubgroup.inertia {M : Type u_6} [AddGroup M] (I : AddSubgroup M) (G : Type u_7) [Group G] [MulAction G M] : Subgroup G

Suppose G acts on M and I is a subgroup of M. The inertia subgroup of I is the subgroup of G whose action is trivial mod I.

Equations

• I.inertia G = { carrier := {σ : G | ∀ (x : M), σ • x - x ∈ I}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem AddSubgroup.mem_inertia {M : Type u_6} [AddGroup M] {I : AddSubgroup M} {G : Type u_7} [Group G] [MulAction G M] {σ : G} : σ ∈ I.inertia G ↔ ∀ (x : M), σ • x - x ∈ I