Structures · Category theory
CategoryTheory.MorphismProperty.IsMultiplicative
A morphism property is multiplicative if it contains identities and is stable by composition.
- Shape
- One type argument
Extends2
Extended by3
Concrete types that are instances11
- CategoryTheory.Functor
- HomologicalComplex
- AlgebraicGeometry.Scheme
- CategoryTheory.ObjectProperty.FullSubcategory
- TopCat
- CategoryTheory.Paths
- HomotopyCategory
- SSet
- CochainComplex
- HomotopyCategory.Plus
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by420
- CategoryTheory.MorphismProperty.Over.pullback
- CategoryTheory.MorphismProperty.Comma.forget
- CategoryTheory.MorphismProperty.Comma.mapLeft
- CategoryTheory.MorphismProperty.Comma.mapRight
- CategoryTheory.MorphismProperty.Over.map
- CategoryTheory.WideSubcategory.obj
- CategoryTheory.InducedWideCategory.Hom.hom
- HomotopicalAlgebra.ReedyStructure.deg
- CategoryTheory.MorphismProperty.Comma.mapLeftIso
- CategoryTheory.MorphismProperty.Comma.mapRightIso
- CategoryTheory.MorphismProperty.Under.pushout
- CategoryTheory.MorphismProperty.Over.forget
- HomotopicalAlgebra.ReedyStructure.degHom
- CategoryTheory.InducedWideCategory
- CategoryTheory.MorphismProperty.Under.map
- CategoryTheory.MorphismProperty.Over.homMk
- CategoryTheory.MorphismProperty.Under.forget
- CategoryTheory.MorphismProperty.pretopology
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued
- CategoryTheory.WideSubcategory.isoMk
- AlgebraicGeometry.Scheme.pretopology
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData
- CategoryTheory.MorphismProperty.Comma.mapLeftComp
- CategoryTheory.MorphismProperty.Comma.mapRightEq
- CategoryTheory.MorphismProperty.Comma.mapLeftEq
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans
- CategoryTheory.MorphismProperty.Comma.isoMk
- CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso
- HomotopicalAlgebra.ReedyStructure.exists_fac
- HomotopicalAlgebra.ReedyStructure.degHom_le
- CategoryTheory.MorphismProperty.Comma.mapRightId
- CategoryTheory.MorphismProperty.Comma.mapLeftId
- CategoryTheory.MorphismProperty.Over.pullbackComp
- AlgebraicGeometry.Scheme.smallPretopology
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj
- CategoryTheory.MorphismProperty.Comma.Hom.ext'
- CategoryTheory.MorphismProperty.Comma.mapRightComp
- CategoryTheory.MorphismProperty.overEquivOfIsInitial
- CategoryTheory.MorphismProperty.Under.isoMk
- CategoryTheory.MorphismProperty.Over.mapId
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso
- CategoryTheory.MorphismProperty.Arrow.forget
- CategoryTheory.MorphismProperty.Over.isoMk
- CategoryTheory.MorphismProperty.Over.mapComp
- CategoryTheory.MorphismProperty.Under.pushoutCompForgetIso
- CategoryTheory.MorphismProperty.multiplicativeClosure_le_iff
- CategoryTheory.MorphismProperty.Under.homMk