Theorems · Theorem · category theory

CategoryTheory.finitaryExtensive_iff_of_isTerminal

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.HasPullbacksOfInclusions C] (T : C) (HT : CategoryTheory.Limits.IsTerminal T)
  (c₀ : CategoryTheory.Limits.BinaryCofan T T) (hc₀ : CategoryTheory.Limits.IsColimit c₀),
  CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀

Defined in

Mathlib.CategoryTheory.Extensive

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasFiniteCoproductsCategoryTheory.HasPullbacksOfInclusions