Theorems · Definition · category theory
CategoryTheory.PreZeroHypercover.HasPullbacks
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreZeroHypercover S → PropThe assumption that the pullback of X i₁ and X i₂ over S exists
for any i₁ and i₂.
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- CategoryTheory.PreZeroHypercover.I₀proof · cited by 763
- CategoryTheory.PreZeroHypercover.fproof · cited by 542
- CategoryTheory.Limits.HasPullbackproof · cited by 434
- CategoryTheory.PreZeroHypercoverstatement and proof · cited by 256
Cited by45
Results whose statement or proof uses this declaration.
- CategoryTheory.PreZeroHypercover.toPreOneHypercoverstatement and proof · cited by 23
- CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacksstatement and proof · cited by 7
- CategoryTheory.PreZeroHypercover.refineOneHypercoverstatement and proof · cited by 6
- CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacksstatement and proof · cited by 5
- CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacksstatement and proof · cited by 3
- CategoryTheory.Precoverage.ZeroHypercover.glueMorphismsstatement and proof · cited by 3
- CategoryTheory.Precoverage.ZeroHypercover.toOneHypercoverstatement and proof · cited by 2
- CategoryTheory.GrothendieckTopology.OneHypercover.mk'statement and proof · cited by 1
- CategoryTheory.PreZeroHypercover.isLimitSigmaOfIsColimitEquivstatement and proof · cited by 1
- CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iffstatement and proof · cited by 1
- CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphismsstatement and proof · cited by 1
- CategoryTheory.Presieve.isSheafFor_sigmaDesc_iffproof · cited by 1