Structures · Category theory
CategoryTheory.Presieve.HasPairwisePullbacks
Given a presieve R on X, the predicate R.HasPairwisePullbacks means that for all arrows
f and g in R, the pullback of f and g exists.
- Defined in
- Mathlib.CategoryTheory.Sites.Sieves
- Shape
- One type argument · adds has_pullbacks
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- CategoryTheory.Equalizer.Presieve.Arrows.SecondObj
- CategoryTheory.Equalizer.Presieve.Arrows.secondMap
- CategoryTheory.Equalizer.Presieve.Arrows.firstMap
- CategoryTheory.Presieve.Arrows.PullbackCompatible
- CategoryTheory.Presieve.HasPairwisePullbacks.has_pullbacks
- CategoryTheory.Equalizer.Presieve.firstMap
- CategoryTheory.Equalizer.Presieve.secondMap
- CategoryTheory.Equalizer.Presieve.SecondObj
- CategoryTheory.Presieve.Arrows.pullbackCompatible_iff
- CategoryTheory.Equalizer.Presieve.w
- CategoryTheory.Presieve.isSheafFor_of_preservesProduct
- CategoryTheory.Presieve.preservesProduct_of_isSheafFor
- CategoryTheory.Equalizer.Presieve.Arrows.w
- CategoryTheory.Presieve.FamilyOfElements.PullbackCompatible
- CategoryTheory.Presieve.HasPairwisePullbacks.map_of_preservesPairwisePullbacks
- CategoryTheory.Presieve.pullbackCompatible_iff
- CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition
- CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff
- CategoryTheory.Equalizer.Presieve.sheaf_condition
- CategoryTheory.Presieve.IsSheafFor.comp_iff_of_preservesPairwisePullbacks
- CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows
- CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff
- CategoryTheory.Presieve.isSheafFor_iff_preservesProduct
- CategoryTheory.Presieve.firstMap_eq_secondMap
- CategoryTheory.Equalizer.Presieve.compatible_iff
- CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks
- CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff_of_small
- CategoryTheory.Presieve.Arrows.PullbackCompatible.congr_simp
Ancestors0
No ancestors.