isVanKampen_finiteCoproducts — Mathlib

English

If a functor preserves and reflects certain colimits, the target category is finitary extensive whenever the source is.

Русский

Если функтор сохраняет и отражает определённые колимиты, то целевая категория конечна расширяемая тогда, когда исходная.

LaTeX

$$$FinitaryExtensive\; C$ given preservation/reflection conditions$$

Lean4

theorem isVanKampen_finiteCoproducts [FinitaryExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F}
    (hc : IsColimit c) : IsVanKampenColimit c :=
  by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι
  apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp
  apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin
  exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc

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