EffectiveEpi

📁 Source: Mathlib/Topology/Category/TopCat/EffectiveEpi.lean

Statistics

Metric	Count
Definitions EffectiveEpi, effectiveEpiStructOfQuotientMap	2
Theorems EffectiveEpi, effectiveEpi_iff_isQuotientMap	2
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
EffectiveEpi 📖	CompData	34 math math: AlgebraicGeometry.Scheme.instEffectiveEpiOfLocallyOfFinitePresentationOfSurjectiveOfFlat, effectiveEpi_of_kernelPair, Preregular.exists_fac, Profinite.effectiveEpi_tfae, AlgebraicGeometry.effectiveEpi_base_of_flat, Functor.ReflectsEffectiveEpis.reflects, Functor.EffectivePresentation.effectiveEpi, Functor.map_effectiveEpi, LightProfinite.effectiveEpi_iff_surjective, regularTopology.mem_sieves_iff_hasEffectiveEpi, Functor.effectiveEpi_of_map, Presieve.regular.single_epi, Sieve.effectiveEpimorphic_singleton, instEffectiveEpiOfEffectiveEpiFamily, Functor.PreservesEffectiveEpis.preserves, regularTopology.isLocallySurjective_iff, AlgebraicGeometry.Scheme.instEffectiveEpiOfQuasiCompactOfSurjectiveOfFlat, Functor.instEffectiveEpiEffectiveEpiOver, effectiveEpiOfKernelPair, IsSplitEpi.EffectiveEpi, isRegularEpi_iff_effectiveEpi, instEffectiveEpiOfIsRegularEpi, CompHaus.effectiveEpi_tfae, effectiveEpi_desc_iff_effectiveEpiFamily, instEffectiveEpiDescOfEffectiveEpiFamily, RegularEpi.effectiveEpi, effectiveEpi_of_effectiveEpi_epi_comp, regularTopology.exists_effectiveEpi_iff_mem_induced, instEffectiveEpiOfIsIso, TopCat.effectiveEpi_iff_isQuotientMap, effectiveEpi_iff_effectiveEpiFamily, CommRingCat.Opposite.effectiveEpi_of_faithfullyFlat, Stonean.effectiveEpi_tfae, regularTopology.instEffectiveEpiComp

CategoryTheory.IsSplitEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
EffectiveEpi 📖	mathematical	—	CategoryTheory.EffectiveEpi	—	CategoryTheory.Category.comp_id CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi CategoryTheory.instEffectiveEpiFamily CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.id

TopCat

Definitions

Name	Category	Theorems
effectiveEpiStructOfQuotientMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpi_iff_isQuotientMap 📖	mathematical	—	CategoryTheory.EffectiveEpi TopCat instCategory Topology.IsQuotientMap carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	—	isQuotientMap_of_isColimit_cofork CategoryTheory.isRegularEpi_of_EffectiveEpi CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.IsRegularEpi.w

---

← Back to Index