Structures · Category theory
CategoryTheory.Mono
A morphism f is a monomorphism if it can be cancelled when postcomposed:
g ≫ f = h ≫ f implies g = h.
[Stacks Tag 003B](https://stacks.math.columbia.edu/tag/003B)
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Shape
- One type argument · adds right_cancellation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by4
Forgetful instances
Every CategoryTheory.Mono is also a
Provided automatically by
Concrete types that are instances25
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- HomologicalComplex
- Action
- AlgebraicGeometry.Scheme
- AddCommGrpCat
- TopCat
- AlgebraicGeometry.SheafedSpace
- AlgebraicGeometry.LocallyRingedSpace
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- AlgebraicGeometry.PresheafedSpace
- TopCat.Presheaf
- TopModuleCat
- SSet
- CochainComplex
- CochainComplex.Plus
- SimplexCategory
- SemiSimplexCategory
- ChainComplex
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by639
- CategoryTheory.cancel_mono
- CategoryTheory.Subobject.underlyingIso
- CategoryTheory.isIso_of_mono_of_epi
- CategoryTheory.Subobject.underlyingIso_arrow
- AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono
- CategoryTheory.Subobject.map
- CategoryTheory.Subobject.ofMkLEMk
- CategoryTheory.Subobject.Classifier.χ
- CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk
- SSet.relativeCellComplexOfMono
- CategoryTheory.injective_of_mono
- CategoryTheory.Subobject.ofLEMk
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData
- CategoryTheory.ShortComplex.Exact.fIsKernel
- CategoryTheory.MonoOver.map
- CategoryTheory.Subobject.ofMkLE
- CategoryTheory.Injective.factorThru
- CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'
- CategoryTheory.SubobjectRepresentableBy.χ
- AlgebraicTopology.DoldKan.Isδ₀
- CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
- CategoryTheory.Subobject.mk_eq_mk_of_comm
- CategoryTheory.Injective.comp_factorThru
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono
- CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono
- CategoryTheory.mono_of_mono_fac
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology
- CategoryTheory.ShortComplex.Exact.lift_f
- CategoryTheory.mono_of_mono
- SimplexCategory.len_le_of_mono
- CategoryTheory.HasSubobjectClassifier.χ
- CategoryTheory.ShortComplex.Exact.lift
- CategoryTheory.Injective.factors
- CategoryTheory.SubobjectRepresentableBy.iso
- CategoryTheory.IsKernelPair.id_of_mono
- CategoryTheory.Subobject.isoOfMkEqMk
- CategoryTheory.Balanced.isIso_of_mono_of_epi
- CategoryTheory.Subobject.mk_le_mk_of_comm
- CategoryTheory.Subobject.ofMkLEMk_comp
- CategoryTheory.Limits.pullbackFstFstIso
- SimplexCategory.eq_id_of_mono
- SSet.nonDegenerate_iff_of_mono
- CategoryTheory.Subobject.isIso_iff_mk_eq_top
- CategoryTheory.MorphismProperty.monomorphisms.infer_property
- CategoryTheory.Adhesive.van_kampen
- CategoryTheory.Subobject.Classifier.uniq
- CategoryTheory.NatTrans.mono_of_mono_app
- CategoryTheory.SubobjectRepresentableBy.π
- CategoryTheory.Simple.mono_isIso_iff_nonzero