Theorems · Inductive type · category theory
CategoryTheory.Functor.Initial
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → PropA functor F : C ⥤ D is initial if for every d : D, the comma category of morphisms
F.obj c ⟶ d is connected.
- Defined in
- Mathlib.CategoryTheory.Limits.Final
- Cited by
- 84 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.Functorstatement · cited by 16,252
Cited by106
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.Initial.extendConestatement and proof · cited by 9
- CategoryTheory.Functor.Initial.isLimitWhiskerEquivstatement and proof · cited by 8
- CategoryTheory.Functor.initial_of_natIsostatement and proof · cited by 6
- CategoryTheory.Functor.initial_iff_of_isCofilteredstatement and proof · cited by 5
- CategoryTheory.Functor.initial_of_comp_full_faithfulstatement and proof · cited by 5
- CategoryTheory.Functor.Initial.conesEquivstatement and proof · cited by 4
- CategoryTheory.Functor.Initial.homToLiftstatement and proof · cited by 3
- CategoryTheory.Functor.Initial.liftstatement and proof · cited by 3
- CategoryTheory.Functor.Initial.limitConeOfCompstatement and proof · cited by 3
- CategoryTheory.Functor.initial_of_initial_compstatement and proof · cited by 3
- CategoryTheory.Limits.LimitPresentation.reindexstatement and proof · cited by 3
- CategoryTheory.Functor.initial_equivalence_compstatement and proof · cited by 3