Theorems · Theorem · category theory
CategoryTheory.IsVanKampenColimit.isUniversal
∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F},
CategoryTheory.IsVanKampenColimit c → CategoryTheory.IsUniversalColimit c- Defined in
- Mathlib.CategoryTheory.Limits.VanKampen
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Functorstatement and proof · cited by 16,252
- CategoryTheory.Functor.mapproof · cited by 8,698
- CategoryTheory.Limits.Cocone.ptproof · cited by 1,354
- CategoryTheory.Functor.constproof · cited by 1,264
- CategoryTheory.Limits.Coconestatement and proof · cited by 746
- CategoryTheory.Limits.Cocone.ιproof · cited by 605
- CategoryTheory.NatTrans.Equifiberedproof · cited by 41
- CategoryTheory.IsVanKampenColimitstatement and proof · cited by 26
- CategoryTheory.IsUniversalColimitstatement · cited by 23
Cited by5
Results whose statement or proof uses this declaration.
- CategoryTheory.IsVanKampenColimit.map_reflectiveproof · cited by 2
- CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Finproof · cited by 1
- CategoryTheory.isVanKampenColimit_extendCofanproof · cited by 1
- AlgebraicGeometry.Scheme.Cover.isSheafFor_sigma_iffproof · cited by 1
- CategoryTheory.IsVanKampenColimit.isColimitproof · cited by 0