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.

Equations

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

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

@[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_isCommutative {G : Type u_7} [CommGroup G] {N : Type u_8} [Group N] (f : G →* N) : f.range.IsCommutative

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• f.rangeRestrict = f.codRestrict f.range ⋯

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 ⋯

@[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_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

@[deprecated MonoidHom.range_eq_top]

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

Alias of MonoidHom.range_eq_top.

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

@[deprecated MonoidHom.range_eq_top_of_surjective]

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

Alias of MonoidHom.range_eq_top_of_surjective.

---

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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) : (Subgroup.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) : (AddSubgroup.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.

Equations

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

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' := ⋯ }

@[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) : ↑((MonoidHom.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) : ↑((AddMonoidHom.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) : (MonoidHom.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) : (AddMonoidHom.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.

Equations

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

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

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} : ↑((MonoidHom.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} : ↑((AddMonoidHom.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 ((MonoidHom.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 ((AddMonoidHom.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') : (MonoidHom.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

Equations

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

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' := ⋯ }

@[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] {N : Type u_5} [Group N] (f : G →* N) {x y : G} : x / y ∈ f.ker ↔ f x = f y

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

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

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

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

theorem MonoidHom.comap_ker {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.comap f g.ker = (g.comp f).ker

theorem AddMonoidHom.comap_ker {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.comap f g.ker = (g.comp 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] {N : Type u_5} [Group N] (K : Subgroup G) (f : G →* N) : (f.restrict K).ker = f.ker.subgroupOf K

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

@[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] : MonoidHom.ker 1 = ⊤

@[simp]

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

@[simp]

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

@[simp]

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

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) : (Subgroup.inclusion h).ker = ⊥

@[simp]

theorem AddSubgroup.ker_inclusion {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : (AddSubgroup.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_sum {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} {G'' : Type u_3} [Group G] [Group G'] [Group G''] (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

theorem MonoidHom.coe_toMultiplicative_ker {A : Type u_8} {A' : Type u_9} [AddGroup A] [AddGroup 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

Equations

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

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' := ⋯ }

@[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} : Subgroup.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} : AddSubgroup.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) : Subgroup.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) : AddSubgroup.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) : Subgroup.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) : AddSubgroup.map f H ≤ f.range

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

theorem AddSubgroup.map_subtype_le {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : AddSubgroup.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 ≤ Subgroup.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 ≤ AddSubgroup.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) : Subgroup.map f (Subgroup.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) : AddSubgroup.map f (AddSubgroup.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) : Subgroup.comap f (Subgroup.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) : AddSubgroup.comap f (AddSubgroup.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) : Subgroup.map f (Subgroup.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) : AddSubgroup.map f (AddSubgroup.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) : Subgroup.map f (Subgroup.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) : AddSubgroup.map f (AddSubgroup.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) : Subgroup.comap f K ≤ Subgroup.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) : AddSubgroup.comap f K ≤ AddSubgroup.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) : Subgroup.comap f K ≤ Subgroup.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) : AddSubgroup.comap f K ≤ AddSubgroup.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) : Subgroup.comap f K < Subgroup.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) : AddSubgroup.comap f K < AddSubgroup.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 (Subgroup.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 (AddSubgroup.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) : Subgroup.comap f (Subgroup.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) : AddSubgroup.comap f (AddSubgroup.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) : Subgroup.comap f (Subgroup.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) : AddSubgroup.comap f (AddSubgroup.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} : Subgroup.map f H ≤ Subgroup.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} : AddSubgroup.map f H ≤ AddSubgroup.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} : Subgroup.map f H ≤ Subgroup.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} : AddSubgroup.map f H ≤ AddSubgroup.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} : Subgroup.map f H = Subgroup.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} : AddSubgroup.map f H = AddSubgroup.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} : Subgroup.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} : AddSubgroup.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} : Subgroup.map f H ≤ Subgroup.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} : AddSubgroup.map f H ≤ AddSubgroup.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'} : Subgroup.map G'.subtype H ≤ Subgroup.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'} : AddSubgroup.map G'.subtype H ≤ AddSubgroup.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 (Subgroup.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 (AddSubgroup.map f)

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 : Subgroup.map f H = Subgroup.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 : AddSubgroup.map f H = AddSubgroup.map f K) : H = K

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

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

theorem AddSubgroup.closure_preimage_eq_top {G : Type u_1} [AddGroup G] (s : Set G) : AddSubgroup.closure (⇑(AddSubgroup.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) : Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.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) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.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) : Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.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) : AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)

theorem Subgroup.sup_subgroupOf_eq {G : Type u_1} [Group G] {H K L : Subgroup G} (hH : H ≤ L) (hK : K ≤ L) : H.subgroupOf L ⊔ K.subgroupOf L = (H ⊔ K).subgroupOf L

theorem AddSubgroup.sup_addSubgroupOf_eq {G : Type u_1} [AddGroup G] {H K L : AddSubgroup G} (hH : H ≤ L) (hK : K ≤ L) : H.addSubgroupOf L ⊔ K.addSubgroupOf L = (H ⊔ K).addSubgroupOf L

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