preservesFiniteProducts_unop — Mathlib

English

If F preserves finite coproducts, then F.unop preserves finite products.

Русский

Если F сохраняет конечные копродукты, то F.unop сохраняет конечные произведения.

LaTeX

$$$\operatorname{PreservesFiniteCoproducts}(F) \Rightarrow \operatorname{PreservesFiniteProducts}(F^{unop})$$$

Lean4

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite coproducts, then `F.unop : C ⥤ D` preserves finite
products. -/
theorem preservesFiniteProducts_unop (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesFiniteCoproducts F] : PreservesFiniteProducts F.unop
    where
  preserves
    _ := by
    apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_unop
    exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

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