preservesBinaryProducts_of_preservesTerminal_and_pullbacks

English

A functor that preserves terminal objects and pullbacks preserves binary products.

Русский

Функтор, сохраняющий терминальные объекты и pullbacks, сохраняет бинарные произведения.

LaTeX

$$$\\forall X,Y:\\ C,\\ F(X\\times Y) \\cong F(X) \\times F(Y)\\quad(\\text{canonical isomorphism})$$$

Lean4

/-- A functor that preserves terminal objects and pullbacks preserves binary products. -/
theorem preservesBinaryProducts_of_preservesTerminal_and_pullbacks [HasTerminal C] [HasPullbacks C]
    [PreservesLimitsOfShape (Discrete.{0} PEmpty) F] [PreservesLimitsOfShape WalkingCospan F] :
    PreservesLimitsOfShape (Discrete WalkingPair) F :=
  ⟨fun {K} =>
    preservesLimit_of_preserves_limit_cone (limitConeOfTerminalAndPullbacks K).2
      (by
        apply isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)
        apply isLimitOfHasPullbackOfPreservesLimit)⟩

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