Structures · Category theory
CategoryTheory.IsSplitMono
IsSplitMono f is the assertion that f admits a retraction
- Defined in
- Mathlib.CategoryTheory.EpiMono
- Shape
- One type argument · adds exists_splitMono
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- SimplexCategoryGenRel
- ChainComplex
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- CategoryTheory.retraction
- CategoryTheory.IsSplitMono.id
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel
- CategoryTheory.IsSplitMono.exists_splitMono
- CategoryTheory.Limits.coneOfIsSplitMono
- CategoryTheory.isIso_of_epi_of_isSplitMono
- CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero
- CategoryTheory.retraction.congr_simp
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr
- CategoryTheory.RegularMono.ofIsSplitMono
- CategoryTheory.mem_essImage_of_unit_isSplitMono
- CategoryTheory.Limits.coneOfIsSplitMono_ι
- CategoryTheory.instIsRegularMonoOfIsSplitMono
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst
- CategoryTheory.instIsSplitMonoMap
- HomologicalComplex.Hom.instIsSplitMonoF
- CategoryTheory.IsIso.of_mono_retraction
- CategoryTheory.retraction_isSplitEpi
- CategoryTheory.IsSplitMono.mono
- CategoryTheory.IsSplitMono.id_assoc
- CategoryTheory.Functor.instIsSplitMonoApp
- CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app
- CategoryTheory.Limits.coneOfIsSplitMono_π_app
- CategoryTheory.Limits.coneOfIsSplitMono_pt
- CategoryTheory.instIsSplitEpiOppositeOpOfIsSplitMono
- CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitMonoOfCokernel
- CategoryTheory.Limits.isSplitMonoEqualizes
- CategoryTheory.instIsSplitMonoComp
- CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt
Ancestors0
No ancestors.