Structures · Category theory
CategoryTheory.EffectiveEpi
A morphism f : Y ⟶ X is an effective epimorphism provided that f exhibits X as a colimit
of the diagram of all "relations" R ⇉ Y.
If f has a kernel pair, then this is equivalent to showing that the corresponding cofork is
a colimit.
- Shape
- One type argument · adds effectiveEpi
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- AlgebraicGeometry.Scheme
- TopCat
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- CategoryTheory.Functor.regularEpiOfPreserves
- CategoryTheory.EffectiveEpi.desc
- CategoryTheory.isColimitCoforkOfEffectiveEpi
- CategoryTheory.EffectiveEpi.getStruct
- CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc
- CategoryTheory.Preregular.exists_fac
- CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback
- CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback'
- CategoryTheory.EffectiveEpi.fac
- CategoryTheory.EffectiveEpi.effectiveEpi
- CategoryTheory.Functor.regularEpiOfPreserves_left
- CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi
- CategoryTheory.instEffectiveEpiFamily
- CategoryTheory.Functor.map_effectiveEpi
- CategoryTheory.Functor.regularEpiOfPreserves_isColimit
- CategoryTheory.isRegularEpi_of_EffectiveEpi
- CategoryTheory.Functor.PreservesEffectiveEpis.preserves
- CategoryTheory.regularTopology.instEffectiveEpiComp
- CategoryTheory.Functor.regularEpiOfPreserves_right
- CategoryTheory.effectiveEpiFamilyStructSingletonOfEffectiveEpi
- CategoryTheory.strongEpi_of_effectiveEpi
- CategoryTheory.epi_of_effectiveEpi
- CategoryTheory.effectiveEpi_of_effectiveEpi_epi_comp
- CategoryTheory.precoherentEffectiveEpiFamilyCompEffectiveEpis
- CategoryTheory.Functor.regularEpiOfPreserves_W
- CategoryTheory.regularEpiOfEffectiveEpi
- CategoryTheory.EffectiveEpi.fac_assoc
- CategoryTheory.EffectiveEpi.uniq
- CategoryTheory.EffectiveEpi.desc.congr_simp
Ancestors0
No ancestors.