Ranges and equality loci of group homomorphisms

This file supplies the characteristic membership equation for the subgroup equality locus and the invariance of the range of a group homomorphism under precomposition with a surjection.

Main results

• MonoidHom.mem_eqLocus: membership in the equality locus is pointwise equality.
• MonoidHom.range_comp_of_surjective: precomposition with a surjection preserves the range.

@[simp]

theorem MonoidHom.mem_eqLocus {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] {f g : G →* M} {x : G} : x ∈ f.eqLocus g ↔ f x = g x

Membership in the equality locus of two group homomorphisms is pointwise equality.

@[simp]

theorem AddMonoidHom.mem_eqLocus {G : Type u_1} {M : Type u_2} [AddGroup G] [AddMonoid M] {f g : G →+ M} {x : G} : x ∈ f.eqLocus g ↔ f x = g x

theorem MonoidHom.range_comp_of_surjective {G : Type u_1} [Group G] {N : Type u_3} {P : Type u_4} [Group N] [Group P] (g : N →* P) (f : G →* N) (hf : Function.Surjective ⇑f) : (g.comp f).range = g.range

Precomposition with a surjective group homomorphism does not change the range.

theorem AddMonoidHom.range_comp_of_surjective {G : Type u_1} [AddGroup G] {N : Type u_3} {P : Type u_4} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) (hf : Function.Surjective ⇑f) : (g.comp f).range = g.range

Precomposition with a surjective additive group homomorphism does not change the range.