Kernel and range of group homomorphisms

We define and prove results about the kernel and range of group homomorphisms.

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

Main definitions

Notation used here:

• G N are Groups

• x is an element of type G

• f g : N →* G are group homomorphisms

Definitions in the file:

• MonoidHom.range f : the range of the group homomorphism f is a subgroup

• MonoidHom.ker f : the kernel of a group homomorphism f is the subgroup of elements x : G such that f x = 1

• MonoidHom.eqLocus f g : given group homomorphisms f, g, the elements of G such that f x = g x form a subgroup of G

Implementation notes

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

Tags

subgroup, subgroups

def MonoidHom.range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup N

The range of a monoid homomorphism from a group is a subgroup.

def AddMonoidHom.range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup N

The range of an AddMonoidHom from an AddGroup is an AddSubgroup.

@[simp]

theorem MonoidHom.coe_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : ↑f.range = Set.range ⇑f

@[simp]

theorem AddMonoidHom.coe_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : ↑f.range = Set.range ⇑f

@[simp]

theorem MonoidHom.mem_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ (x : G), f x = y

@[simp]

theorem AddMonoidHom.mem_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {y : N} : y ∈ f.range ↔ ∃ (x : G), f x = y

theorem MonoidHom.range_eq_map {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range = Subgroup.map f ⊤

theorem AddMonoidHom.range_eq_map {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = AddSubgroup.map f ⊤

instance MonoidHom.range_isMulCommutative {G : Type u_7} [CommGroup G] {N : Type u_8} [Group N] (f : G →* N) : IsMulCommutative ↥f.range

instance AddMonoidHom.range_isAddCommutative {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) : IsAddCommutative ↥f.range

@[simp]

theorem MonoidHom.restrict_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) : (f.restrict K).range = Subgroup.map f K

@[simp]

theorem AddMonoidHom.restrict_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) : (f.restrict K).range = AddSubgroup.map f K

def MonoidHom.rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : G →* ↥f.range

The canonical surjective group homomorphism G →* f(G) induced by a group homomorphism G →* N.

def AddMonoidHom.rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : G →+ ↥f.range

The canonical surjective AddGroup homomorphism G →+ f(G) induced by a group homomorphism G →+ N.

@[simp]

theorem MonoidHom.coe_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (g : G) : ↑(f.rangeRestrict g) = f g

@[simp]

theorem AddMonoidHom.coe_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (g : G) : ↑(f.rangeRestrict g) = f g

theorem MonoidHom.coe_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subtype.val ∘ ⇑f.rangeRestrict = ⇑f

theorem AddMonoidHom.coe_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Subtype.val ∘ ⇑f.rangeRestrict = ⇑f

theorem MonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f

theorem AddMonoidHom.subtype_comp_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range.subtype.comp f.rangeRestrict = f

theorem MonoidHom.rangeRestrict_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Function.Surjective ⇑f.rangeRestrict

theorem AddMonoidHom.rangeRestrict_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : Function.Surjective ⇑f.rangeRestrict

@[simp]

theorem MonoidHom.rangeRestrict_injective_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f

@[simp]

theorem AddMonoidHom.rangeRestrict_injective_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} : Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f

theorem MonoidHom.map_range {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : Subgroup.map g f.range = (g.comp f).range

theorem AddMonoidHom.map_range {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g f.range = (g.comp f).range

theorem MonoidHom.range_comp {G : Type u_1} [Group G] {N : Type u_5} {P : Type u_6} [Group N] [Group P] (g : N →* P) (f : G →* N) : (g.comp f).range = Subgroup.map g f.range

theorem AddMonoidHom.range_comp {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : (g.comp f).range = AddSubgroup.map g f.range

theorem MonoidHom.range_eq_top {G : Type u_1} [Group G] {N : Type u_7} [Group N] {f : G →* N} : f.range = ⊤ ↔ Function.Surjective ⇑f

theorem AddMonoidHom.range_eq_top {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] {f : G →+ N} : f.range = ⊤ ↔ Function.Surjective ⇑f

@[simp]

theorem MonoidHom.range_eq_top_of_surjective {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (hf : Function.Surjective ⇑f) : f.range = ⊤

The range of a surjective monoid homomorphism is the whole of the codomain.

@[simp]

theorem AddMonoidHom.range_eq_top_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (hf : Function.Surjective ⇑f) : f.range = ⊤

The range of a surjective AddMonoid homomorphism is the whole of the codomain.

@[simp]

theorem MonoidHom.range_one {G : Type u_1} [Group G] {N : Type u_5} [Group N] : range 1 = ⊥

@[simp]

theorem AddMonoidHom.range_zero {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] : range 0 = ⊥

@[simp]

theorem Subgroup.range_subtype {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.range = H

@[simp]

theorem AddSubgroup.range_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype.range = H

theorem Subgroup.subtype_range {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.range = H

Alias of Subgroup.range_subtype.

theorem AddSubgroup.subtype_range {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype.range = H

@[simp]

theorem Subgroup.inclusion_range {G : Type u_1} [Group G] {H K : Subgroup G} (h_le : H ≤ K) : (inclusion h_le).range = H.subgroupOf K

@[simp]

theorem AddSubgroup.inclusion_range {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h_le : H ≤ K) : (inclusion h_le).range = H.addSubgroupOf K

theorem MonoidHom.subgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [Group G₁] [Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂) (h : f.range ≤ K) : f.range.subgroupOf K = (f.codRestrict K ⋯).range

theorem AddMonoidHom.addSubgroupOf_range_eq_of_le {G₁ : Type u_7} {G₂ : Type u_8} [AddGroup G₁] [AddGroup G₂] {K : AddSubgroup G₂} (f : G₁ →+ G₂) (h : f.range ≤ K) : f.range.addSubgroupOf K = (f.codRestrict K ⋯).range

def MonoidHom.ofLeftInverse {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) : G ≃* ↥f.range

Computable alternative to MonoidHom.ofInjective.

def AddMonoidHom.ofLeftInverse {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) : G ≃+ ↥f.range

Computable alternative to AddMonoidHom.ofInjective.

@[simp]

theorem MonoidHom.ofLeftInverse_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) (x : G) : ↑((ofLeftInverse h) x) = f x

@[simp]

theorem AddMonoidHom.ofLeftInverse_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : G) : ↑((ofLeftInverse h) x) = f x

@[simp]

theorem MonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {g : N →* G} (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range) : (ofLeftInverse h).symm x = g ↑x

@[simp]

theorem AddMonoidHom.ofLeftInverse_symm_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range) : (ofLeftInverse h).symm x = g ↑x

noncomputable def MonoidHom.ofInjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) : G ≃* ↥f.range

The range of an injective group homomorphism is isomorphic to its domain.

noncomputable def AddMonoidHom.ofInjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) : G ≃+ ↥f.range

The range of an injective additive group homomorphism is isomorphic to its domain.

theorem MonoidHom.ofInjective_apply {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {x : G} : ↑((ofInjective hf) x) = f x

theorem AddMonoidHom.ofInjective_apply {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {x : G} : ↑((ofInjective hf) x) = f x

@[simp]

theorem MonoidHom.apply_ofInjective_symm {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) (x : ↥f.range) : f ((ofInjective hf).symm x) = ↑x

@[simp]

theorem AddMonoidHom.apply_ofInjective_symm {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) (x : ↥f.range) : f ((ofInjective hf).symm x) = ↑x

@[simp]

theorem MonoidHom.coe_toAdditive_range {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (toAdditive f).range = Subgroup.toAddSubgroup f.range

@[simp]

theorem MonoidHom.coe_toMultiplicative_range {A : Type u_7} {A' : Type u_8} [AddGroup A] [AddGroup A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).range = AddSubgroup.toSubgroup f.range

def MonoidHom.ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : Subgroup G

The multiplicative kernel of a monoid homomorphism is the subgroup of elements x : G such that f x = 1

def AddMonoidHom.ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : AddSubgroup G

The additive kernel of an AddMonoid homomorphism is the AddSubgroup of elements such that f x = 0

@[simp]

theorem MonoidHom.ker_toSubmonoid {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : f.ker.toSubmonoid = mker f

@[simp]

theorem AddMonoidHom.ker_toAddSubmonoid {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker.toAddSubmonoid = mker f

@[simp]

theorem MonoidHom.mem_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1

@[simp]

theorem AddMonoidHom.mem_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] {f : G →+ M} {x : G} : x ∈ f.ker ↔ f x = 0

theorem MonoidHom.div_mem_ker_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) {x y : G} : x / y ∈ f.ker ↔ f x = f y

theorem AddMonoidHom.sub_mem_ker_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x y : G} : x - y ∈ f.ker ↔ f x = f y

theorem MonoidHom.coe_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : ↑f.ker = ⇑f ⁻¹' {1}

theorem AddMonoidHom.coe_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : ↑f.ker = ⇑f ⁻¹' {0}

@[simp]

theorem MonoidHom.ker_toHomUnits {G : Type u_1} [Group G] {M : Type u_8} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker

@[simp]

theorem AddMonoidHom.ker_toHomAddUnits {G : Type u_1} [AddGroup G] {M : Type u_8} [AddMonoid M] (f : G →+ M) : f.toHomAddUnits.ker = f.ker

theorem MonoidHom.eq_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) {x y : G} : f x = f y ↔ y⁻¹ * x ∈ f.ker

theorem AddMonoidHom.eq_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) {x y : G} : f x = f y ↔ -y + x ∈ f.ker

@[implicit_reducible]

instance MonoidHom.decidableMemKer {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] [DecidableEq M] (f : G →* M) : DecidablePred fun (x : G) => x ∈ f.ker

@[implicit_reducible]

instance AddMonoidHom.decidableMemKer {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] [DecidableEq M] (f : G →+ M) : DecidablePred fun (x : G) => x ∈ f.ker

theorem MonoidHom.comap_ker {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_8} [MulOneClass P] (g : N →* P) (f : G →* N) : Subgroup.comap f g.ker = (g.comp f).ker

theorem AddMonoidHom.comap_ker {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_8} [AddZeroClass P] (g : N →+ P) (f : G →+ N) : AddSubgroup.comap f g.ker = (g.comp f).ker

@[simp]

theorem MonoidHom.ker_comp_mulEquiv {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_8} [MulOneClass P] (g : N →* P) (iso : G ≃* N) : (g.comp ↑iso).ker = Subgroup.map (↑iso.symm) g.ker

The kernel of a homomorphism composed with an isomorphism is equal to the kernel of the homomorphism mapped by the inverse isomorphism.

@[simp]

theorem AddMonoidHom.ker_comp_addEquiv {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_8} [AddZeroClass P] (g : N →+ P) (iso : G ≃+ N) : (g.comp ↑iso).ker = AddSubgroup.map (↑iso.symm) g.ker

@[simp]

theorem MonoidHom.ker_mulEquiv_comp {G : Type u_1} [Group G] {N : Type u_5} [Group N] {P : Type u_8} [MulOneClass P] (f : G →* N) (iso : N ≃* P) : ((↑iso).comp f).ker = f.ker

Composing with an isomorphism on the codomain does not change the kernel.

@[simp]

theorem AddMonoidHom.ker_addEquiv_comp {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {P : Type u_8} [AddZeroClass P] (f : G →+ N) (iso : N ≃+ P) : ((↑iso).comp f).ker = f.ker

@[simp]

theorem MonoidHom.comap_bot {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : Subgroup.comap f ⊥ = f.ker

@[simp]

theorem AddMonoidHom.comap_bot {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.comap f ⊥ = f.ker

@[simp]

theorem MonoidHom.ker_restrict {G : Type u_1} [Group G] (K : Subgroup G) {M : Type u_7} [MulOneClass M] (f : G →* M) : (f.restrict K).ker = f.ker.subgroupOf K

@[simp]

theorem AddMonoidHom.ker_restrict {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {M : Type u_7} [AddZeroClass M] (f : G →+ M) : (f.restrict K).ker = f.ker.addSubgroupOf K

@[simp]

theorem MonoidHom.ker_codRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] {S : Type u_8} [SetLike S N] [SubmonoidClass S N] (f : G →* N) (s : S) (h : ∀ (x : G), f x ∈ s) : (f.codRestrict s h).ker = f.ker

@[simp]

theorem AddMonoidHom.ker_codRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {S : Type u_8} [SetLike S N] [AddSubmonoidClass S N] (f : G →+ N) (s : S) (h : ∀ (x : G), f x ∈ s) : (f.codRestrict s h).ker = f.ker

@[simp]

theorem MonoidHom.ker_rangeRestrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.rangeRestrict.ker = f.ker

@[simp]

theorem AddMonoidHom.ker_rangeRestrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.rangeRestrict.ker = f.ker

@[simp]

theorem MonoidHom.ker_one {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] : ker 1 = ⊤

@[simp]

theorem AddMonoidHom.ker_zero {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] : ker 0 = ⊤

@[simp]

theorem MonoidHom.ker_id {G : Type u_1} [Group G] : (id G).ker = ⊥

@[simp]

theorem AddMonoidHom.ker_id {G : Type u_1} [AddGroup G] : (id G).ker = ⊥

theorem MonoidHom.ker_eq_top_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] {f : G →* M} : f.ker = ⊤ ↔ f = 1

theorem AddMonoidHom.ker_eq_top_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] {f : G →+ M} : f.ker = ⊤ ↔ f = 0

theorem MonoidHom.range_eq_bot_iff {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {f : G →* G'} : f.range = ⊥ ↔ f = 1

theorem AddMonoidHom.range_eq_bot_iff {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} : f.range = ⊥ ↔ f = 0

theorem MonoidHom.ker_eq_bot_iff {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : f.ker = ⊥ ↔ Function.Injective ⇑f

theorem AddMonoidHom.ker_eq_bot_iff {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker = ⊥ ↔ Function.Injective ⇑f

@[simp]

theorem Subgroup.ker_subtype {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.ker = ⊥

@[simp]

theorem AddSubgroup.ker_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.subtype.ker = ⊥

@[simp]

theorem Subgroup.ker_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥

@[simp]

theorem AddSubgroup.ker_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : (inclusion h).ker = ⊥

theorem MonoidHom.ker_prod {G : Type u_1} [Group G] {M : Type u_8} {N : Type u_9} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) : (f.prod g).ker = f.ker ⊓ g.ker

theorem AddMonoidHom.ker_prod {G : Type u_1} [AddGroup G] {M : Type u_8} {N : Type u_9} [AddZeroClass M] [AddZeroClass N] (f : G →+ M) (g : G →+ N) : (f.prod g).ker = f.ker ⊓ g.ker

theorem MonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {M : Type u_7} [MulOneClass M] (f : G →* G') (g : G' →* M) : f.range ≤ g.ker ↔ g.comp f = 1

theorem AddMonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {M : Type u_7} [AddZeroClass M] (f : G →+ G') (g : G' →+ M) : f.range ≤ g.ker ↔ g.comp f = 0

@[instance 100]

instance MonoidHom.normal_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) : f.ker.Normal

@[instance 100]

instance AddMonoidHom.normal_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) : f.ker.Normal

@[simp]

theorem MonoidHom.coe_toAdditive_ker {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') : (toAdditive f).ker = Subgroup.toAddSubgroup f.ker

@[simp]

theorem MonoidHom.coe_toMultiplicative_ker {A : Type u_8} {A' : Type u_9} [AddGroup A] [AddZeroClass A'] (f : A →+ A') : (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker

def MonoidHom.eqLocus {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] (f g : G →* M) : Subgroup G

The subgroup of elements x : G such that f x = g x

def AddMonoidHom.eqLocus {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] (f g : G →+ M) : AddSubgroup G

The additive subgroup of elements x : G such that f x = g x

@[simp]

theorem MonoidHom.eqLocus_same {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) : f.eqLocus f = ⊤

@[simp]

theorem AddMonoidHom.eqLocus_same {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.eqLocus f = ⊤

theorem MonoidHom.eqOn_closure {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f g : G →* M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem AddMonoidHom.eqOn_closure {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f g : G →+ M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(AddSubgroup.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem MonoidHom.eq_of_eqOn_top {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {f g : G →* M} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

theorem AddMonoidHom.eq_of_eqOn_top {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {f g : G →+ M} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

theorem MonoidHom.eq_of_eqOn_dense {G : Type u_1} [Group G] {M : Type u_7} [Monoid M] {s : Set G} (hs : Subgroup.closure s = ⊤) {f g : G →* M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

theorem AddMonoidHom.eq_of_eqOn_dense {G : Type u_1} [AddGroup G] {M : Type u_7} [AddMonoid M] {s : Set G} (hs : AddSubgroup.closure s = ⊤) {f g : G →+ M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g

theorem Subgroup.map_eq_bot_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} : map f H = ⊥ ↔ H ≤ f.ker

theorem AddSubgroup.map_eq_bot_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} : map f H = ⊥ ↔ H ≤ f.ker

theorem Subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) {f : G →* N} (hf : Function.Injective ⇑f) : map f H = ⊥ ↔ H = ⊥

theorem AddSubgroup.map_eq_bot_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Injective ⇑f) : map f H = ⊥ ↔ H = ⊥

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

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

theorem Subgroup.map_subtype_le {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : map H.subtype K ≤ H

theorem AddSubgroup.map_subtype_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : map H.subtype K ≤ H

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

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

theorem Subgroup.map_comap_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup N) : map f (comap f H) = f.range ⊓ H

theorem AddSubgroup.map_comap_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : map f (comap f H) = f.range ⊓ H

theorem Subgroup.comap_map_eq {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) (H : Subgroup G) : comap f (map f H) = H ⊔ f.ker

theorem AddSubgroup.comap_map_eq {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : comap f (map f H) = H ⊔ f.ker

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

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

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

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

theorem Subgroup.comap_le_comap_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K L : Subgroup N} (hf : K ≤ f.range) : comap f K ≤ comap f L ↔ K ≤ L

theorem AddSubgroup.comap_le_comap_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : K ≤ f.range) : comap f K ≤ comap f L ↔ K ≤ L

theorem Subgroup.comap_le_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective ⇑f) : comap f K ≤ comap f L ↔ K ≤ L

theorem AddSubgroup.comap_le_comap_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : Function.Surjective ⇑f) : comap f K ≤ comap f L ↔ K ≤ L

theorem Subgroup.comap_lt_comap_of_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {K L : Subgroup N} (hf : Function.Surjective ⇑f) : comap f K < comap f L ↔ K < L

theorem AddSubgroup.comap_lt_comap_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K L : AddSubgroup N} (hf : Function.Surjective ⇑f) : comap f K < comap f L ↔ K < L

theorem Subgroup.comap_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Surjective ⇑f) : Function.Injective (comap f)

theorem AddSubgroup.comap_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) : Function.Injective (comap f)

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

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

theorem Subgroup.comap_map_eq_self_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) (H : Subgroup G) : comap f (map f H) = H

theorem AddSubgroup.comap_map_eq_self_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) (H : AddSubgroup G) : comap f (map f H) = H

theorem Subgroup.map_le_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

theorem AddSubgroup.map_le_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

theorem Subgroup.map_le_map_iff' {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

theorem AddSubgroup.map_le_map_iff' {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

theorem Subgroup.map_eq_map_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H K : Subgroup G} : map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker

theorem AddSubgroup.map_eq_map_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker

theorem Subgroup.map_eq_range_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} {H : Subgroup G} : map f H = f.range ↔ Codisjoint H f.ker

theorem AddSubgroup.map_eq_range_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} : map f H = f.range ↔ Codisjoint H f.ker

theorem Subgroup.map_le_map_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {H K : Subgroup G} : map f H ≤ map f K ↔ H ≤ K

theorem AddSubgroup.map_le_map_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : map f H ≤ map f K ↔ H ≤ K

@[simp]

theorem Subgroup.map_subtype_le_map_subtype {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : map G'.subtype H ≤ map G'.subtype K ↔ H ≤ K

@[simp]

theorem AddSubgroup.map_subtype_le_map_subtype {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'} : map G'.subtype H ≤ map G'.subtype K ↔ H ≤ K

def Subgroup.MapSubtype.orderIso {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup ↥H ≃o { H' : Subgroup G // H' ≤ H }

Subgroups of the subgroup H are considered as subgroups that are less than or equal to H.

def AddSubgroup.MapSubtype.orderIso {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : AddSubgroup ↥H ≃o { H' : AddSubgroup G // H' ≤ H }

Additive subgroups of the subgroup H are considered as additive subgroups that are less than or equal to H.

@[simp]

theorem AddSubgroup.MapSubtype.orderIso_apply_coe {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (H' : AddSubgroup ↥H) : ↑((orderIso H) H') = map H.subtype H'

@[simp]

theorem Subgroup.MapSubtype.orderIso_apply_coe {G : Type u_1} [Group G] (H : Subgroup G) (H' : Subgroup ↥H) : ↑((orderIso H) H') = map H.subtype H'

@[simp]

theorem Subgroup.MapSubtype.orderIso_symm_apply {G : Type u_1} [Group G] (H : Subgroup G) (sH' : { H' : Subgroup G // H' ≤ H }) : (orderIso H).symm sH' = (↑sH').subgroupOf H

@[simp]

theorem AddSubgroup.MapSubtype.orderIso_symm_apply {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (sH' : { H' : AddSubgroup G // H' ≤ H }) : (orderIso H).symm sH' = (↑sH').addSubgroupOf H

theorem Subgroup.forall {G : Type u_1} [Group G] {H : Subgroup G} {P : Subgroup ↥H → Prop} : (∀ (H' : Subgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.subgroupOf H)

theorem AddSubgroup.forall {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {P : AddSubgroup ↥H → Prop} : (∀ (H' : AddSubgroup ↥H), P H') ↔ ∀ H' ≤ H, P (H'.addSubgroupOf H)

theorem Subgroup.map_lt_map_iff_of_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (hf : Function.Injective ⇑f) {H K : Subgroup G} : map f H < map f K ↔ H < K

theorem AddSubgroup.map_lt_map_iff_of_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : map f H < map f K ↔ H < K

@[simp]

theorem Subgroup.map_subtype_lt_map_subtype {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : map G'.subtype H < map G'.subtype K ↔ H < K

@[simp]

theorem AddSubgroup.map_subtype_lt_map_subtype {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'} : map G'.subtype H < map G'.subtype K ↔ H < K

theorem Subgroup.map_injective {G : Type u_1} [Group G] {N : Type u_5} [Group N] {f : G →* N} (h : Function.Injective ⇑f) : Function.Injective (map f)

theorem AddSubgroup.map_injective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) : Function.Injective (map f)

theorem Subgroup.map_subtype_inj {G : Type u_1} [Group G] {H : Subgroup G} {K L : Subgroup ↥H} : map H.subtype K = map H.subtype L ↔ K = L

theorem AddSubgroup.map_subtype_inj {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {K L : AddSubgroup ↥H} : map H.subtype K = map H.subtype L ↔ K = L

theorem Subgroup.map_injective_of_ker_le {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H K : Subgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) : H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem AddSubgroup.map_injective_of_ker_le {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H K : AddSubgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : map f H = map f K) : H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem Subgroup.ker_subgroupMap {G : Type u_1} [Group G] {N : Type u_5} [Group N] (H : Subgroup G) (f : G →* N) : (f.subgroupMap H).ker = f.ker.subgroupOf H

theorem AddSubgroup.ker_addSubgroupMap {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) : (f.addSubgroupMap H).ker = f.ker.addSubgroupOf H

theorem Subgroup.closure_preimage_eq_top {G : Type u_1} [Group G] (s : Set G) : closure (⇑(closure s).subtype ⁻¹' s) = ⊤

theorem AddSubgroup.closure_preimage_eq_top {G : Type u_1} [AddGroup G] (s : Set G) : closure (⇑(closure s).subtype ⁻¹' s) = ⊤

theorem Subgroup.comap_sup_eq_of_le_range {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {H K : Subgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) : comap f H ⊔ comap f K = comap f (H ⊔ K)

theorem AddSubgroup.comap_sup_eq_of_le_range {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H K : AddSubgroup N} (hH : H ≤ f.range) (hK : K ≤ f.range) : comap f H ⊔ comap f K = comap f (H ⊔ K)

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

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

theorem Subgroup.subgroupOf_sup {G : Type u_1} [Group G] {A A' B : Subgroup G} (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

theorem AddSubgroup.addSubgroupOf_sup {G : Type u_1} [AddGroup G] {A A' B : AddSubgroup G} (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').addSubgroupOf B = A.addSubgroupOf B ⊔ A'.addSubgroupOf B

@[deprecated Subgroup.subgroupOf_sup "Use in reverse direction." (since := "2025-11-03")]

theorem Subgroup.sup_subgroupOf_eq {G : Type u_1} [Group G] {A A' B : Subgroup G} (hA : A ≤ B) (hA' : A' ≤ B) : (A ⊔ A').subgroupOf B = A.subgroupOf B ⊔ A'.subgroupOf B

Alias of Subgroup.subgroupOf_sup.

theorem Subgroup.codisjoint_subgroupOf_sup {G : Type u_1} [Group G] (H K : Subgroup G) : Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

theorem AddSubgroup.codisjoint_addSubgroupOf_sup {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : Codisjoint (H.addSubgroupOf (H ⊔ K)) (K.addSubgroupOf (H ⊔ K))

theorem Subgroup.subgroupOf_map_powMonoidHom_eq_range {M : Type u_6} [CommGroup M] (S : Subgroup M) (n : ℕ) : (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range

theorem AddSubgroup.addSubgroupOf_map_nsmulAddMonoidHom_eq_range {M : Type u_6} [AddCommGroup M] (S : AddSubgroup M) (n : ℕ) : (map (nsmulAddMonoidHom n) S).addSubgroupOf S = (nsmulAddMonoidHom n).range

@[simp]

theorem MulEquiv.range_eq_top {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (e : G ≃* G') : (↑e).range = ⊤

@[simp]

theorem AddEquiv.range_eq_top {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') : (↑e).range = ⊤

theorem MulEquiv.map_range_powMonoidHom {M : Type u_5} {N : Type u_6} [CommGroup M] [CommGroup N] (e : M ≃* N) (n : ℕ) : Subgroup.map (↑e) (powMonoidHom n).range = (powMonoidHom n).range

theorem AddEquiv.map_range_nsmulAddMonoidHom {M : Type u_5} {N : Type u_6} [AddCommGroup M] [AddCommGroup N] (e : M ≃+ N) (n : ℕ) : AddSubgroup.map (↑e) (nsmulAddMonoidHom n).range = (nsmulAddMonoidHom n).range