Monomorphisms

📁 Source: Mathlib/AlgebraicTopology/SimplicialSet/Monomorphisms.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsStableUnderCobaseChangeMonomorphisms, instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType, instIsStableUnderFilteredColimitsMonomorphisms	3
Total	3

SSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsStableUnderCobaseChangeMonomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderCobaseChange SSet largeCategory CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.functorCategory_monomorphisms CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeFunctorFunctorCategoryOfHasPushouts CategoryTheory.Types.instIsStableUnderCobaseChangeMonomorphismsType CategoryTheory.Limits.Types.instHasPushoutsType
instIsStableUnderCoproductsMonomorphismsOfHasCoproductsType 📖	mathematical	CategoryTheory.Limits.HasCoproducts CategoryTheory.types	CategoryTheory.MorphismProperty.IsStableUnderCoproducts SSet largeCategory CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.instIsStableUnderCoproductsFunctorMonomorphismsOfHasCoproductsOfHasPullbacks CategoryTheory.Types.instIsStableUnderCoproductsMonomorphismsType CategoryTheory.Limits.Types.instHasPullbacksType
instIsStableUnderFilteredColimitsMonomorphisms 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits SSet largeCategory CategoryTheory.MorphismProperty.monomorphisms	—	CategoryTheory.MorphismProperty.functorCategory_monomorphisms CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.MorphismProperty.IsStableUnderColimitsOfShape.functorCategory CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.isStableUnderColimitsOfShape CategoryTheory.Types.instIsStableUnderFilteredColimitsMonomorphismsType CategoryTheory.Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self

---

← Back to Index