preservesProduct_of_preservesBiproduct

English

If the biproduct comparison is mono, then F preserves the biproduct of f.

Русский

Если сравнение биопродукта моно, то F сохраняет биопродукт f.

LaTeX

$$$\mathrm{Mono}(\mathrm{biproductComparison}\ F\ f) \Rightarrow \mathrm{PreservesBiproduct}\ f\ F$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products. -/
theorem preservesProduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesLimit (Discrete.functor f) F where
  preserves
    hc :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨IsLimit.ofIsoLimit
          ((IsLimit.postcomposeInvEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
            (isBilimitOfPreserves F (biconeIsBilimitOfLimitConeOfIsLimit hc)).isLimit) <|
        Cones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

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