English
If a function f has a kernel relation H contained in r and the quotient lift is injective, then ker f = r.
Русский
Если для функции f ядро hk удовлетворяет hk ≤ r и образующий тождественный отображатель фактор-множества является инъективным, то ker f = r.
LaTeX
$$$$ ker f = r. $$$$
Lean4
/-- Equivalence between functions `α → β` such that `r x y → f x = f y` and functions
`quotient r → β`. -/
def liftEquiv (r : Setoid α) : { f : α → β // r ≤ ker f } ≃ (Quotient r → β)
where
toFun f := Quotient.lift (f : α → β) f.2
invFun f := ⟨f ∘ Quotient.mk'', fun x y h => by simp [ker_def, Quotient.sound' h]⟩
right_inv _ := funext fun x => Quotient.inductionOn' x fun _ => rfl
