isUniversal_finiteCoproducts — Mathlib

English

The van Kampen property holds for finite coproduct diagrams, implying that certain pushout-related colimits reflect isomorphisms.

Русский

Свойство ван Кампена выполняется для диаграмм конечного копроизведения, что значит, что определённые колимитные связки в отношении пушпута отражают изоморфизмы.

LaTeX

$$$IsVanKampenColimit\; c$ for finite coproducts$$

Lean4

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

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