preservesShape_fin_of_preserves_binary_and_initial

English

If F preserves the initial object and binary coproducts, then it preserves colimits of shape Discrete Fin n for any n.

Русский

Если F сохраняет начальный объект и бинарные копроизведения, то он сохраняет колимиты формой Discrete Fin n для любого n.

LaTeX

$$$\forall n,\ PreservesColimitsOfShape(Discrete(\mathrm{Fin}(n))) F$$$

Lean4

/-- If `F` preserves the initial object and binary coproducts, then it preserves colimits of shape
`Discrete (Fin n)`.
-/
theorem preservesShape_fin_of_preserves_binary_and_initial (n : ℕ) : PreservesColimitsOfShape (Discrete (Fin n)) F where
  preservesColimit
    {K} := by
    let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _
    haveI := preserves_fin_of_preserves_binary_and_initial F n fun n => K.obj ⟨n⟩
    apply preservesColimit_of_iso_diagram F that

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