instPreservesLimitWalkingCospanCospanToCompHausLike

English

The limit preservation holds when transporting along toCompHausLike h.

Русский

Сохранение пределов сохраняется при переходе к CompHausLike через h.

LaTeX

$$$\\text{PreservesLimit}(\\mathrm{cospan}\\ f\\ g)\\ (\\mathrm{toCompHausLike}\\ h)$$$

Lean4

/-- The functor to another `CompHausLike` preserves pullbacks. -/
noncomputable instance {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop) :
    PreservesLimit (cospan f g) (toCompHausLike h) :=
  by
  have : PreservesLimit (cospan f g) (toCompHausLike h ⋙ compHausLikeToTop P') :=
    inferInstanceAs (PreservesLimit _ (compHausLikeToTop _))
  exact preservesLimit_of_reflects_of_preserves (toCompHausLike h) (compHausLikeToTop P')

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