English
For a monoid hom f and a congruence c on M, the comap of f along f.map_mul c equals ker (c.mk'.comp f).
Русский
Для моноидного гомоморфизма f и конгруэнции c на M, комап along f.map_mul c равен ker (c.mk'.comp f).
LaTeX
$$$\operatorname{comap} f\ f.mapMul\ c = \ker (c.mk'.comp f)$$$
Lean4
/-- Given a monoid homomorphism `f : N → M` and a congruence relation `c` on `M`, the congruence
relation induced on `N` by `f` equals the kernel of `c`'s quotient homomorphism composed with
`f`. -/
@[to_additive /-- Given an `AddMonoid` homomorphism `f : N → M` and an additive congruence relation
`c` on `M`, the additive congruence relation induced on `N` by `f` equals the kernel of `c`'s
quotient homomorphism composed with `f`. -/
]
theorem comap_eq {f : N →* M} : comap f f.map_mul c = ker (c.mk'.comp f) :=
ext fun x y => show c _ _ ↔ c.mk' _ = c.mk' _ by rw [← c.eq]; rfl
