Structures · Category theory
CategoryTheory.Limits.HasStrongEpiMonoFactorisations
A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.
- Shape
- One type argument · adds has_fac
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- CategoryTheory.Functor
- SimplexCategory
- NonemptyFinLinOrd
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- CategoryTheory.Limits.image.isoStrongEpiMono
- CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι
- CategoryTheory.Limits.HasStrongEpiMonoFactorisations.has_fac
- CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc
- CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation
- CategoryTheory.MonoOver.liftStructOfHasStrongEpiMonoFactorisation
- CategoryTheory.Subobject.hasColimitsOfSize
- CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization
- CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData
- CategoryTheory.MonoOver.isColimitCoconeOfHasStrongEpiMonoFactorisation
- CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation.congr_simp
- CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono
- CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations
- CategoryTheory.Limits.hasStrongEpiImages_of_hasStrongEpiMonoFactorisations
- CategoryTheory.MonoOver.hasColimitsOfSize_of_hasStrongEpiMonoFactorisations
- CategoryTheory.Limits.functorialEpiMonoFactorizationData
- CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence
- CategoryTheory.MonoOver.commSqOfHasStrongEpiMonoFactorisation
Ancestors0
No ancestors.