Extensive

📁 Source: Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean

Statistics

Metric	Count
Definitions	0
Theorems effectiveEpi_desc_iff_effectiveEpiFamily, instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis, instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis	3
Total	3

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpi_desc_iff_effectiveEpiFamily 📖	mathematical	—	EffectiveEpi Limits.sigmaObj Limits.hasColimitOfHasColimitsOfShape Discrete discreteCategory Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Discrete.functor Limits.Sigma.desc EffectiveEpiFamily	—	Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts FinitaryPreExtensive.hasPullbacks_of_inclusions Limits.instIsIsoDescι IsIso.epi_of_iso FinitaryPreExtensive.isIso_sigmaDesc_fst instEffectiveEpiDescOfEffectiveEpiFamily
instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis 📖	mathematical	—	Functor.PreservesFiniteEffectiveEpiFamilies	—	Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Limits.sigmaComparison_map_desc instEffectiveEpiOfEffectiveEpiFamily instEffectiveEpiFamilyCompOfIsSplitEpi IsSplitEpi.of_iso Limits.instIsIsoSigmaComparison Limits.PreservesColimitsOfShape.preservesColimit Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts instEffectiveEpiFamily Functor.map_effectiveEpi instEffectiveEpiDescOfEffectiveEpiFamily
instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis 📖	mathematical	—	Functor.ReflectsFiniteEffectiveEpiFamilies	—	Limits.hasColimitOfHasColimitsOfShape Limits.hasColimitsOfShape_discrete FinitaryPreExtensive.hasFiniteCoproducts Functor.effectiveEpi_of_map Limits.instIsIsoSigmaComparison Limits.PreservesColimitsOfShape.preservesColimit Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Limits.sigmaComparison_map_desc instEffectiveEpiOfEffectiveEpiFamily instEffectiveEpiFamilyCompOfIsSplitEpi IsSplitEpi.of_iso IsIso.inv_isIso instEffectiveEpiFamily instEffectiveEpiDescOfEffectiveEpiFamily

---

← Back to Index