English
For a quotient map f, there is a canonical homeomorphism between the quotient by ker f and the codomain Y, given hf.
Русский
Для отображения-функции f существует канонический гомеоморфизм между частными эквивалентностями и целевым пространством Y, задаваемый hf.
LaTeX
$$$\\text{homeomorph}(hf) : Quotient(\\ker f) \\simeq_t Y$$$
Lean4
/-- The homeomorphism from the quotient of a quotient map to its codomain. This is
`Setoid.quotientKerEquivOfSurjective` as a homeomorphism.
-/
@[simps!]
noncomputable def homeomorph (hf : IsQuotientMap f) : Quotient (Setoid.ker f) ≃ₜ Y
where
toEquiv := Setoid.quotientKerEquivOfSurjective _ hf.surjective
continuous_toFun := isQuotientMap_quot_mk.continuous_iff.mpr hf.continuous
continuous_invFun := by
rw [hf.continuous_iff]
convert continuous_quotient_mk'
ext
simp only [Equiv.invFun_as_coe, Function.comp_apply,
(Setoid.quotientKerEquivOfSurjective f hf.surjective).symm_apply_eq]
rfl
