Theorems · Theorem · category theory
CategoryTheory.Coverage.eq_top_pullback
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {S T : CategoryTheory.Sieve X},
S ≤ T → ∀ (f : Y ⟶ X), S.arrows f → CategoryTheory.Sieve.pullback f T = ⊤- Defined in
- Mathlib.CategoryTheory.Sites.Coverage
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 29 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.
Cites10
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.CategoryStruct.compproof · cited by 17,999
- Top.topstatement · cited by 9,680
- CategoryTheory.Sievestatement and proof · cited by 552
- CategoryTheory.Sieve.arrowsstatement and proof · cited by 446
- CategoryTheory.Sieve.pullbackstatement · cited by 126
- CategoryTheory.Sieve.extproof · cited by 43
- CategoryTheory.Sieve.downward_closedproof · cited by 39
- CategoryTheory.Sieve.pullback_applyproof · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- CategoryTheory.Coverage.saturate_of_supersetproof · cited by 5