liftEquiv — Mathlib

English

IsQuotientMap.liftEquiv establishes an equivalence between the space of compatible families 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

/-- `IsQuotientMap.lift` as an equivalence. -/
@[simps]
noncomputable def liftEquiv : { g : C(X, Z) // Function.FactorsThrough g f } ≃ C(Y, Z)
    where
  toFun g := hf.lift g g.prop
  invFun g := ⟨g.comp f, fun _ _ h ↦ by simp only [ContinuousMap.comp_apply]; rw [h]⟩
  left_inv := by intro; simp
  right_inv := by
    intro g
    ext a
    simpa using congrArg g (Function.rightInverse_surjInv hf.surjective a)

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