Structures · Category theory
CategoryTheory.MorphismProperty.HasOfPostcompProperty
A class of morphisms W has the of-postcomp property w.r.t. W' if whenever
g is in W' and f ≫ g is in W, also f is in W.
- Shape
- 2 explicit arguments · adds of_postcomp
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 by50
- CategoryTheory.MorphismProperty.of_postcomp
- AlgebraicGeometry.Scheme.smallPretopology
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj
- CategoryTheory.MorphismProperty.postcomp_iff
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp
- CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_postcomp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'
- AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology
- AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected
- AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.MorphismProperty.instHasOfPrecompPropertyUnopOfHasOfPostcompPropertyOpposite
- CategoryTheory.MorphismProperty.CostructuredArrow.instPreservesLimitsOfShapeTopOverWalkingCospanToOver
- CategoryTheory.MorphismProperty.CostructuredArrow.createsLimitsOfShape_walkingCospan
- AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp'
- CategoryTheory.MorphismProperty.instHasOfPrecompPropertyOppositeOpOfHasOfPostcompProperty
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_I₀
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp
- CategoryTheory.Over.closedUnderLimitsOfShape_pullback
- CategoryTheory.MorphismProperty.CostructuredArrow.hasPullbacks
- AlgebraicGeometry.Scheme.instOverPullbackCoverOverProp
- CategoryTheory.MorphismProperty.Over.createsLimitsOfShape_walkingCospan
- CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le
- AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app
- CategoryTheory.CostructuredArrow.closedUnderLimitsOfShape_walkingCospan
- CategoryTheory.MorphismProperty.Over.instHasFiniteLimitsTopOfHasFiniteWidePullbacks
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_f
- AlgebraicGeometry.Scheme.smallPretopology.congr_simp
- CategoryTheory.MorphismProperty.Over.hasFiniteLimits
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj_counit_app
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_X
- AlgebraicGeometry.Scheme.isCoverDense_toOver_Spec
- CategoryTheory.MorphismProperty.Over.hasPullbacks
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_X
- CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopPullback
- CategoryTheory.MorphismProperty.Over.instPreservesFiniteLimitsTopOverForget
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_f
- AlgebraicGeometry.Scheme.isOneHypercoverDense_toOver_Spec
- CategoryTheory.MorphismProperty.instCodescendsAlongOfIsStableUnderCobaseChangeOfHasOfPostcompPropertyOfRespectsLeft
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj.congr_simp
- AlgebraicGeometry.Scheme.instOverXPullbackCoverOverProp'
- CategoryTheory.MorphismProperty.Over.instCreatesFiniteLimitsTopOverForget
- CategoryTheory.MorphismProperty.instHasOfPostcompPropertyMin
- AlgebraicGeometry.Scheme.Cover.intersectionOfLocallyDirected_f
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀
- AlgebraicGeometry.Scheme.smallGrothendieckTopologyOfLE_eq_toGrothendieck_smallPretopology
- AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology
Ancestors0
No ancestors.