instHasFiniteCoproductsOfHasExplicitFiniteCoproducts

English

The functor to TopCat preserves finite coproducts when explicit finite coproducts exist.

Русский

Функтор к TopCat сохраняет конечные копроизведения, если они существуют явно в P.

LaTeX

$$$\\text{PreservesFiniteCoproducts}(\\mathrm{compHausLikeToTop}\\ P)$$$

Lean4

instance [HasExplicitFiniteCoproducts.{w} P] : HasFiniteCoproducts (CompHausLike.{max u w} P) where
  out
    n := by
    let α := ULift.{w} (Fin n)
    let e : Discrete α ≌ Discrete (Fin n) := Discrete.equivalence Equiv.ulift
    exact hasColimitsOfShape_of_equivalence e

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