English
The lift construction IsQuotientMap.liftEquiv provides an equivalence between the quotient of all g through f and C(Y,Z).
Русский
Конструкция подъёма IsQuotientMap.liftEquiv устанавливает эквиваленцию между множествами гомоморфизмов и C(Y,Z).
LaTeX
$$$\\text{liftEquiv} : \\{ g:\\, C(X,Z) \\// \\text{FactorsThrough } g\\ f \\} \\simeq C(Y,Z)$$$
Lean4
/-- Descend a continuous map, which is constant on the fibres, along a quotient map. -/
@[simps]
noncomputable def lift : C(Y, Z)
where
toFun :=
((fun i ↦ Quotient.liftOn' i g (fun _ _ (hab : f _ = f _) ↦ h hab)) : Quotient (Setoid.ker f) → Z) ∘
hf.homeomorph.symm
continuous_toFun := Continuous.comp (continuous_quot_lift _ g.2) (Homeomorph.continuous _)
