EffectiveEpimorphic

📁 Source: Mathlib/CategoryTheory/Sites/EffectiveEpimorphic.lean

Statistics

Metric	Count
Definitions EffectiveEpimorphic, EffectiveEpimorphic, generateFamily, generateSingleton, effectiveEpiFamilyStructOfIsColimit, effectiveEpiStructOfIsColimit, isColimitOfEffectiveEpiFamilyStruct, isColimitOfEffectiveEpiStruct	8
Theorems effectiveEpimorphic_family, effectiveEpimorphic_singleton, generateFamily_eq, generateSingleton_eq	4
Total	12

CategoryTheory

Definitions

Name	Category	Theorems
effectiveEpiFamilyStructOfIsColimit 📖	CompOp	—
effectiveEpiStructOfIsColimit 📖	CompOp	—
isColimitOfEffectiveEpiFamilyStruct 📖	CompOp	—
isColimitOfEffectiveEpiStruct 📖	CompOp	—

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
EffectiveEpimorphic 📖	MathDef	2 math math: CategoryTheory.Sieve.effectiveEpimorphic_singleton, CategoryTheory.Sieve.effectiveEpimorphic_family

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
EffectiveEpimorphic 📖	MathDef	—
generateFamily 📖	CompOp	1 math math: generateFamily_eq
generateSingleton 📖	CompOp	1 math math: generateSingleton_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpimorphic_family 📖	mathematical	—	CategoryTheory.Presieve.EffectiveEpimorphic CategoryTheory.Presieve.ofArrows CategoryTheory.EffectiveEpiFamily	—	Nonempty.map generateFamily_eq
effectiveEpimorphic_singleton 📖	mathematical	—	CategoryTheory.Presieve.EffectiveEpimorphic CategoryTheory.Presieve.singleton CategoryTheory.EffectiveEpi	—	Nonempty.map generateSingleton_eq
generateFamily_eq 📖	mathematical	—	generate CategoryTheory.Presieve.ofArrows generateFamily	—	ext
generateSingleton_eq 📖	mathematical	—	generate CategoryTheory.Presieve.singleton generateSingleton	—	ext

---

← Back to Index