preservesFiniteBiproductsOfAdditive

English

If F is additive, then it preserves finite biproducts.

Русский

Если F аддитивен, то он сохраняет конечные биобразования (би-произведения).

LaTeX

$$$[\text{Additive } F] \Rightarrow \operatorname{PreservesFiniteBiproducts}(F)$$$

Lean4

instance (priority := 100) preservesFiniteBiproductsOfAdditive [Additive F] : PreservesFiniteBiproducts F where
  preserves := fun {J} _ =>
    let ⟨_⟩ := nonempty_fintype J
    {
      preserves :=
        {
          preserves := fun hb =>
            ⟨isBilimitOfTotal _
                (by
                  simp_rw [F.mapBicone_π, F.mapBicone_ι, ← F.map_comp]
                  erw [← F.map_sum, ← F.map_id, IsBilimit.total hb])⟩ } }

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