Structures · Category theory
CategoryTheory.MorphismProperty.HasOfPrecompProperty
A class of morphisms W has the of-precomp property w.r.t. W' if whenever
f is in W' and f ≫ g is in W, also g is in W.
- Shape
- 2 explicit arguments · adds of_precomp
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- AlgebraicGeometry.Scheme
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by17
- CategoryTheory.MorphismProperty.precomp_iff
- CategoryTheory.MorphismProperty.of_precomp
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj
- CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_precomp
- CategoryTheory.Under.closedUnderColimitsOfShape_pushout
- CategoryTheory.MorphismProperty.HasOfPrecompProperty.of_le
- CategoryTheory.MorphismProperty.Under.instCreatesFiniteColimitsTopUnderForget
- CategoryTheory.MorphismProperty.Under.instHasPushoutsTopOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty
- CategoryTheory.MorphismProperty.instHasOfPrecompPropertyMin
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj_unit_app
- CategoryTheory.MorphismProperty.Under.instPreservesFiniteColimitsTopUnderForget
- CategoryTheory.MorphismProperty.Under.instHasFiniteColimitsTopOfHasFiniteWidePushouts
- CategoryTheory.MorphismProperty.Under.instCreatesColimitsOfShapeTopUnderWalkingSpanForgetOfHasPushoutsOfIsStableUnderCompositionOfIsStableUnderCobaseChangeOfHasOfPrecompProperty
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj_counit_app
- CategoryTheory.MorphismProperty.instDescendsAlongOfIsStableUnderBaseChangeOfHasOfPrecompPropertyOfRespectsRight
- CategoryTheory.MorphismProperty.instHasOfPostcompPropertyUnopOfHasOfPrecompPropertyOpposite
- CategoryTheory.MorphismProperty.instHasOfPostcompPropertyOppositeOpOfHasOfPrecompProperty
Ancestors0
No ancestors.