preserves_fin_of_preserves_binary_and_initial

English

If F preserves the initial object and binary coproducts, then it preserves coproducts indexed by Fin n for any n.

Русский

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

LaTeX

$$$\forall n,\forall f:\mathrm{Fin}(n)\to C,\ PreservesColimit(\mathrm{Discrete.functor}(f),F)$$$

Lean4

/-- If `F` preserves the initial object and binary coproducts, then it preserves products indexed by
`Fin n` for any `n`.
-/
theorem preserves_fin_of_preserves_binary_and_initial :
    ∀ (n : ℕ) (f : Fin n → C), PreservesColimit (Discrete.functor f) F
  | 0 => fun f =>
    by
    letI : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
      preservesColimitsOfShape_of_equiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
    infer_instance
  | n + 1 => by
    haveI := preserves_fin_of_preserves_binary_and_initial n
    intro f
    apply
      preservesColimit_of_preserves_colimit_cocone (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _))
        _
    apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
    let this :=
      extendCofanIsColimit (fun i => F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F _)
        (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)
    refine IsColimit.ofIsoColimit this ?_
    apply Cocones.ext _ _
    · apply Iso.refl _
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply Category.comp_id
    · rintro i _
      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
      rw [comp_id, ← F.map_comp]

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