# 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 `Group`s

- `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

source
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.

Equations

- f.range = (Subgroup.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source
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`.

Equations

- f.range = (AddSubgroup.map f ⊤).copy (Set.range ⇑f) ⋯

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
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 ⊤
source
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 ⊤
source
instance MonoidHom.range_isMulCommutative {G : Type u_7} [CommGroup G] {N : Type u_8} [Group N] (f : G →* N) :
IsMulCommutative ↥f.range
source
instance AddMonoidHom.range_isAddCommutative {G : Type u_7} [AddCommGroup G] {N : Type u_8} [AddGroup N] (f : G →+ N) :
IsAddCommutative ↥f.range
source
@[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
source
@[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
source
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`.

Equations

- f.rangeRestrict = f.codRestrict f.range ⋯

Instances For

source
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`.

Equations

- f.rangeRestrict = f.codRestrict f.range ⋯

Instances For

source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
theorem MonoidHom.rangeRestrict_surjective {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
Function.Surjective ⇑f.rangeRestrict
source
theorem AddMonoidHom.rangeRestrict_surjective {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
Function.Surjective ⇑f.rangeRestrict
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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.

source
@[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.

source
@[simp]
theorem MonoidHom.range_one {G : Type u_1} [Group G] {N : Type u_5} [Group N] :
range 1 = ⊥
source
@[simp]
theorem AddMonoidHom.range_zero {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] :
range 0 = ⊥
source
@[simp]
theorem Subgroup.range_subtype {G : Type u_1} [Group G] (H : Subgroup G) :
H.subtype.range = H
source
@[simp]
theorem AddSubgroup.range_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
H.subtype.range = H
source
theorem Subgroup.subtype_range {G : Type u_1} [Group G] (H : Subgroup G) :
H.subtype.range = H

Alias of `Subgroup.range_subtype`.

source
theorem AddSubgroup.subtype_range {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
H.subtype.range = H
source
@[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
source
@[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
source
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
source
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
source
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`.

Equations

- MonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
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`.

Equations

- AddMonoidHom.ofLeftInverse h = { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
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.

Equations

- MonoidHom.ofInjective hf = MulEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯

Instances For

source
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.

Equations

- AddMonoidHom.ofInjective hf = AddEquiv.ofBijective (f.codRestrict f.range ⋯) ⋯

Instances For

source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
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`

Equations

- f.ker = { toSubmonoid := MonoidHom.mker f, inv_mem' := ⋯ }

Instances For

source
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`

Equations

- f.ker = { toAddSubmonoid := AddMonoidHom.mker f, neg_mem' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
@[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
source
theorem MonoidHom.div_mem_ker_iff {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) {x y : G} :
x / y ∈ f.ker ↔ f x = f y
source
theorem AddMonoidHom.sub_mem_ker_iff {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {x y : G} :
x - y ∈ f.ker ↔ f x = f y
source
theorem MonoidHom.coe_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :
↑f.ker = ⇑f ⁻¹' {1}
source
theorem AddMonoidHom.coe_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :
↑f.ker = ⇑f ⁻¹' {0}
source
@[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
source
@[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
source
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
source
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
source
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
Equations

- f.decidableMemKer x = decidable_of_iff (f x = 1) ⋯

source
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
Equations

- f.decidableMemKer x = decidable_of_iff (f x = 0) ⋯

source
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
source
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
source
@[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
source
@[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
source
@[simp]
theorem MonoidHom.ker_restrict {G : Type u_1} [Group G] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) :
(f.restrict K).ker = f.ker.subgroupOf K
source
@[simp]
theorem AddMonoidHom.ker_restrict {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) :
(f.restrict K).ker = f.ker.addSubgroupOf K
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem MonoidHom.ker_one {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] :
ker 1 = ⊤
source
@[simp]
theorem AddMonoidHom.ker_zero {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] :
ker 0 = ⊤
source
@[simp]
theorem MonoidHom.ker_id {G : Type u_1} [Group G] :
(id G).ker = ⊥
source
@[simp]
theorem AddMonoidHom.ker_id {G : Type u_1} [AddGroup G] :
(id G).ker = ⊥
source
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
source
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
source
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
source
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
source
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
source
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
source
@[simp]
theorem Subgroup.ker_subtype {G : Type u_1} [Group G] (H : Subgroup G) :
H.subtype.ker = ⊥
source
@[simp]
theorem AddSubgroup.ker_subtype {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
H.subtype.ker = ⊥
source
@[simp]
theorem Subgroup.ker_inclusion {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) :
(inclusion h).ker = ⊥
source
@[simp]
theorem AddSubgroup.ker_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) :
(inclusion h).ker = ⊥
source
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
source
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
source
theorem MonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [Group G] [Group G'] [Group G''] (f : G →* G') (g : G' →* G'') :
f.range ≤ g.ker ↔ g.comp f = 1
source
theorem AddMonoidHom.range_le_ker_iff {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [AddGroup G] [AddGroup G'] [AddGroup G''] (f : G →+ G') (g : G' →+ G'') :
f.range ≤ g.ker ↔ g.comp f = 0
source
@[instance 100]
instance MonoidHom.normal_ker {G : Type u_1} [Group G] {M : Type u_7} [MulOneClass M] (f : G →* M) :
f.ker.Normal
source
@[instance 100]
instance AddMonoidHom.normal_ker {G : Type u_1} [AddGroup G] {M : Type u_7} [AddZeroClass M] (f : G →+ M) :
f.ker.Normal
source
@[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
source
@[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
source
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`

Equations

- f.eqLocus g = { toSubmonoid := f.eqLocusM g, inv_mem' := ⋯ }

Instances For

source
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`

Equations

- f.eqLocus g = { toAddSubmonoid := f.eqLocusM g, neg_mem' := ⋯ }

Instances For

source
@[simp]
theorem MonoidHom.eqLocus_same {G : Type u_1} [Group G] {N : Type u_5} [Group N] (f : G →* N) :
f.eqLocus f = ⊤
source
@[simp]
theorem AddMonoidHom.eqLocus_same {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) :
f.eqLocus f = ⊤
source
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.

source
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.

source
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
source
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
source
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
source
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
source
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
source
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
source
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 = ⊥
source
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 = ⊥
source
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
source
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
source
theorem Subgroup.map_subtype_le {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) :
map H.subtype K ≤ H
source
theorem AddSubgroup.map_subtype_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) :
map H.subtype K ≤ H
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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)
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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`.

Equations

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

Instances For

source
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`.

Equations

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

Instances For

source
@[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'
source
@[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'
source
@[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
source
@[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
source
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)
source
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)
source
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
source
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
source
@[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
source
@[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
source
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)
source
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)
source
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`.

source
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`.

source
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
source
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
source
theorem Subgroup.closure_preimage_eq_top {G : Type u_1} [Group G] (s : Set G) :
closure (⇑(closure s).subtype ⁻¹' s) = ⊤
source
theorem AddSubgroup.closure_preimage_eq_top {G : Type u_1} [AddGroup G] (s : Set G) :
closure (⇑(closure s).subtype ⁻¹' s) = ⊤
source
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)
source
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)
source
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)
source
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)
source
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
source
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
source
@[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`.

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