Theorems · Definition · category theory
CategoryTheory.Sieve.uliftFunctorInclusion
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
{X : C} → (S : CategoryTheory.Sieve X) → S.uliftFunctor ⟶ CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj XA variant of Sieve.functorInclusion with universe lifting.
- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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.Homstatement · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.Functorstatement · cited by 16,252
- Oppositestatement · cited by 8,081
- CategoryTheory.Sievestatement and proof · cited by 552
- CategoryTheory.Functor.whiskerRightproof · cited by 467
- CategoryTheory.uliftYonedastatement · cited by 84
- CategoryTheory.uliftFunctorproof · cited by 58
- CategoryTheory.Sieve.functorInclusionproof · cited by 8
- CategoryTheory.Sieve.uliftFunctorstatement · cited by 5
Cited by3
Results whose statement or proof uses this declaration.
- CategoryTheory.Sieve.sieveOfUliftSubfunctor_uliftFunctorInclusionstatement · cited by 0
- CategoryTheory.Sieve.uliftFunctorInclusion_appstatement and proof · cited by 0
- CategoryTheory.Sieve.uliftNatTransOfLe_commstatement · cited by 0