quotientKerEquivOfSurjective — Mathlib

English

If f is surjective, the quotient by ker f bijects with β. If a right inverse is known, the isomorphism is definitional.

Русский

Если f сюръективна, то фактор-множество по ker f субъективно биективно к β. При наличии правой инверсии каноническое изоморфство задаётся явно.

LaTeX

$$$$ Quotient(\\ker f) \\simeq β. $$$$

Lean4

/-- The quotient of α by the kernel of a surjective function f bijects with f's codomain.

If a specific right-inverse of `f` is known, `Setoid.quotientKerEquivOfRightInverse` can be
definitionally more useful. -/
noncomputable def quotientKerEquivOfSurjective (hf : Surjective f) : Quotient (ker f) ≃ β :=
  quotientKerEquivOfRightInverse _ (Function.surjInv hf) (rightInverse_surjInv hf)

Похожие утверждения