Theorems · Definition · category theory
CategoryTheory.Presieve.ofArrows.casesOn
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
{motive : ⦃Y_1 : C⦄ → (a : Y_1 ⟶ X) → CategoryTheory.Presieve.ofArrows Y f a → Prop} ⦃Y_1 : C⦄ {a : Y_1 ⟶ X}
(t : CategoryTheory.Presieve.ofArrows Y f a), (∀ (i : ι), motive (f i) ⋯) → motive a t- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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 and proof · cited by 32,603
- CategoryTheory.Presieve.ofArrowsstatement and proof · cited by 150
Cited by64
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Cover.exists_eqproof · cited by 12
- CategoryTheory.Sieve.ofArrows_category'proof · cited by 6
- TopCat.Presheaf.IsSheaf.section_extproof · cited by 5
- CategoryTheory.Presieve.ofArrows_surjproof · cited by 4
- CategoryTheory.Presieve.ofArrows_pullbackproof · cited by 3
- CategoryTheory.Presieve.presieve₀_preZeroHypercoverproof · cited by 2
- CategoryTheory.Presieve.pushforward_ofArrowsproof · cited by 2
- CategoryTheory.Pseudofunctor.DescentData.exists_equivalence_of_sieve_eqproof · cited by 2
- CategoryTheory.Presieve.uncurry_ofArrowsproof · cited by 2