English
Let f: α → β and an equivalence relation r on β. The pullback of r along f, denoted comap f r, is the equivalence on α given by x ∼ y iff f(x) ∼_r f(y). This pullback coincides with the kernel of the composed map α → β → Quotient(β) given by x ↦ ⟦f(x)⟧. In particular, comap f r = ker( Quotient.mk'' ∘ f ).
Русский
Пусть f: α → β и r — эквивалентность на β. Обратная прообразация r по f, обозначаемая comap f r, есть эквивалентность на α: x ∼ y тогда и только тогда, когда f(x) ∼_r f(y). Эта связь совпадает с керном композиции: ker(Quotient.mk'' ∘ f). В частности, comap f r = ker(Quotient.mk'' ∘ f).
LaTeX
$$$\\operatorname{comap}_f(r) = \\ker\\bigl( \\operatorname{Quotient.mk}'' \\circ f \\bigr).$$$
Lean4
/-- Given a map `f : N → M` and an equivalence relation `r` on `β`, the equivalence relation
induced on `α` by `f` equals the kernel of `r`'s quotient map composed with `f`. -/
theorem comap_eq {f : α → β} {r : Setoid β} : comap f r = ker (@Quotient.mk'' _ r ∘ f) :=
ext fun x y => show _ ↔ ⟦_⟧ = ⟦_⟧ by rw [Quotient.eq]; rfl
