Structures · Category theory
CategoryTheory.IsSplitEpi
IsSplitEpi f is the assertion that f admits a section
- Defined in
- Mathlib.CategoryTheory.EpiMono
- Shape
- One type argument · adds exists_splitEpi
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 by37
- CategoryTheory.section_
- CategoryTheory.IsSplitEpi.id
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel
- CategoryTheory.isIso_of_mono_of_isSplitEpi
- CategoryTheory.IsSplitEpi.exists_splitEpi
- CategoryTheory.Limits.coconeOfIsSplitEpi
- CategoryTheory.Sieve.generate_of_contains_isSplitEpi
- CategoryTheory.Sieve.generate_of_singleton_isSplitEpi
- CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero
- CategoryTheory.section_.congr_simp
- CategoryTheory.Limits.coconeOfIsSplitEpi_π
- CategoryTheory.IsSplitEpi.EffectiveEpi
- CategoryTheory.IsSplitEpi.epi
- CategoryTheory.IsSplitEpi.id_assoc
- CategoryTheory.instIsRegularEpiOfIsSplitEpi
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt
- CategoryTheory.instIsSplitMonoOppositeOpOfIsSplitMono
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl
- HomologicalComplex.Hom.instIsSplitEpiF
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst
- CategoryTheory.Limits.coconeOfIsSplitEpi_ι_app
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd
- CategoryTheory.IsIso.of_epi_section
- CategoryTheory.Limits.isSplitEpiCoequalizes
- CategoryTheory.instIsSplitEpiMap
- CategoryTheory.Sieve.galoisInsertionOfIsSplitEpi
- CategoryTheory.RegularEpi.ofSplitEpi
- CategoryTheory.Limits.coconeOfIsSplitEpi_pt
- CategoryTheory.section_isSplitMono
- CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr
- CategoryTheory.Limits.isBilimitBinaryBiconeOfIsSplitEpiOfKernel
- CategoryTheory.Adjunction.full_L_of_isSplitEpi_unit_app
- CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi
- CategoryTheory.mem_essImage_of_counit_isSplitEpi
- CategoryTheory.instIsSplitEpiComp
- CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi
- CategoryTheory.Functor.instIsSplitEpiApp
Ancestors0
No ancestors.