English
Let c be a congruence on a monoid M and f a monoid homomorphism M →* P constant on c-equivalence classes; then the image of the induced lift c.lift f is the same as the image of f.
Русский
Пусть c — конгруэнтность на моноиде M, а f: M →* P — гомоморфизм, константный на классах эквивалентности c; тогда образ индуцированного лейфта c.lift f совпадает с образом f.
LaTeX
$$$\operatorname{mrange}(c.lift f H) = \operatorname{mrange}(f)$, где $H: c \leq \ker f$.$$
Lean4
/-- Given a congruence relation `c` on a monoid and a homomorphism `f` constant on `c`'s
equivalence classes, `f` has the same image as the homomorphism that `f` induces on the
quotient. -/
@[to_additive /-- Given an additive congruence relation `c` on an `AddMonoid` and a homomorphism `f`
constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces
on the quotient. -/
]
theorem lift_range (H : c ≤ ker f) : MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f :=
Submonoid.ext fun x => ⟨by rintro ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, fun ⟨y, hy⟩ => ⟨↑y, hy⟩⟩
