Structures · Category theory
CategoryTheory.Epi
A morphism f is an epimorphism if it can be cancelled when precomposed:
f ≫ g = f ≫ h implies g = h.
[Stacks Tag 003B](https://stacks.math.columbia.edu/tag/003B)
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Shape
- One type argument · adds left_cancellation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances25
- CategoryTheory.Functor
- CategoryTheory.Over
- ModuleCat
- HomologicalComplex
- TopCat
- SheafOfModules
- CommRingCat
- PresheafOfModules
- CategoryTheory.Under
- CategoryTheory.Sheaf
- CategoryTheory.CostructuredArrow
- CategoryTheory.StructuredArrow
- TopCat.Presheaf
- CompHausLike
- TopModuleCat
- CategoryTheory.Idempotents.Karoubi
- SSet
- CategoryTheory.Preadditive.RightFreyd
- LightProfinite
- Profinite
- LightCondMod
- SimplexCategory
- SemiNormedGrp
- CompHaus
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by389
- CategoryTheory.cancel_epi
- CategoryTheory.isIso_of_mono_of_epi
- CategoryTheory.epi_of_epi_fac
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData
- CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'
- CategoryTheory.ShortComplex.Exact.gIsCokernel
- CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
- CategoryTheory.epi_of_epi
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono
- CategoryTheory.surjective_up_to_refinements_of_epi
- CategoryTheory.isSplitEpi_of_epi
- CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono
- CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology
- SimplexCategory.len_le_of_epi
- CategoryTheory.Projective.factorThru
- CategoryTheory.Projective.factorThru_comp
- SheafOfModules.GeneratingSections.ofEpi
- CategoryTheory.Balanced.isIso_of_mono_of_epi
- CategoryTheory.Limits.zero_of_epi_comp
- CategoryTheory.ShortComplex.Exact.desc
- CategoryTheory.Epi.left_cancellation
- CategoryTheory.Limits.eq_of_epi_equalizer
- CategoryTheory.Projective.factors
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData
- CategoryTheory.ShortComplex.Exact.g_desc
- CategoryTheory.ShortComplex.ShortExact.map
- CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'
- CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono
- CategoryTheory.SimplicialObject.Splitting.IndexSet.epiComp
- CategoryTheory.Abelian.epiDesc
- CategoryTheory.ObjectProperty.epiModSerre_of_epi
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage
- CategoryTheory.surjective_of_epi
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand
- CompHaus.lift
- CategoryTheory.IsIso.of_epi_section'
- CategoryTheory.Limits.isCokernelEpiComp
- CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi
- CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono
- CategoryTheory.Limits.PushoutCocone.inl_eq_inr_of_epi_eq
- CategoryTheory.Abelian.comp_epiDesc
- Profinite.lift
- AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀
- HomologicalComplex.epi_homologyMap_of_epi_of_not_rel
- CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi
- CategoryTheory.normalEpiOfEpi
- SSet.unique_nonDegenerate_map
- CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono
- CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation
Ancestors0
No ancestors.