Structures · Category theory
CategoryTheory.MorphismProperty.IsStableUnderComposition
A morphism property satisfies IsStableUnderComposition if the composition of
two such morphisms still falls in the class.
- Shape
- One type argument · adds comp_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances2
- AlgebraicGeometry.Scheme
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by141
- CategoryTheory.MorphismProperty.comp_mem
- CategoryTheory.MorphismProperty.Over.map
- CategoryTheory.MorphismProperty.Under.map
- AlgebraicGeometry.Scheme.smallPretopology
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj
- AlgebraicGeometry.Scheme.Cover.pushforwardIso
- CategoryTheory.Span.comp
- CategoryTheory.MorphismProperty.Over.mapId
- CategoryTheory.MorphismProperty.Over.mapComp
- CategoryTheory.MorphismProperty.Comma.Hom.comp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp
- CategoryTheory.MorphismProperty.Under.mapPushoutAdj
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'
- HomotopicalAlgebra.isCofibrant_of_cofibration
- CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback
- CategoryTheory.MorphismProperty.Over.mapCongr
- CategoryTheory.Localization.Construction.morphismProperty_eq_top
- CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology
- CategoryTheory.MorphismProperty.Under.mapId
- AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
- CategoryTheory.MorphismProperty.exists_map_eq_of_presieve
- CategoryTheory.MorphismProperty.Under.mapCongr
- CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem
- AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology
- CategoryTheory.MorphismProperty.Under.mapComp
- CategoryTheory.MorphismProperty.composePath_mem_of_id_mem
- AlgebraicGeometry.Scheme.locallyCoverDense_of_le
- CategoryTheory.MorphismProperty.pullbackMap
- CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition
- CategoryTheory.MorphismProperty.coverPreserving_comap_forget
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- AlgebraicGeometry.HasRingHomProperty.descendsAlong
- HomotopicalAlgebra.isFibrant_of_fibration
- CategoryTheory.MorphismProperty.IsStableUnderComposition.ind_of_preIndSpreads
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.MorphismProperty.pullback_map
- CategoryTheory.MorphismProperty.CostructuredArrow.instPreservesLimitsOfShapeTopOverWalkingCospanToOver
- AlgebraicGeometry.Scheme.Cover.pushforwardIso_f
- HomotopicalAlgebra.PathObject.instFibrationP₁
- CategoryTheory.Under.closedUnderColimitsOfShape_pushout
- CategoryTheory.MorphismProperty.IsStableUnderComposition.inf
- CategoryTheory.MorphismProperty.CostructuredArrow.createsLimitsOfShape_walkingCospan
- CategoryTheory.MorphismProperty.isRightAdjoint_pullback
- CategoryTheory.MorphismProperty.Under.map_map_right
- AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp'
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀
- CategoryTheory.MorphismProperty.Over.map_obj_left
- HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp
Ancestors0
No ancestors.