EffectiveEpimorphic

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

Statistics

Metric	Count
Definitions EffectiveEpimorphic, EffectiveEpimorphic, generateFamily, generateSingleton, effectiveEpiFamilyStructOfIsColimit, effectiveEpiStructOfIsColimit, isColimitOfEffectiveEpiFamilyStruct, isColimitOfEffectiveEpiStruct	8
Theorems iff_forall_isSheafFor_yoneda, isSheafFor_of_isRepresentable, singleton_of_isRepresentable_of_effectiveEpi, iff_forall_isSheafFor_yoneda, effectiveEpimorphic_family, effectiveEpimorphic_singleton, generateFamily_eq, generateSingleton_eq	8
Total	16

CategoryTheory

Definitions

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

CategoryTheory.Presieve

Definitions

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

CategoryTheory.Presieve.EffectiveEpimorphic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_forall_isSheafFor_yoneda 📖	mathematical	—	CategoryTheory.Presieve.EffectiveEpimorphic CategoryTheory.Presieve.IsSheafFor CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	CategoryTheory.Presieve.isSheafFor_iff_generate
isSheafFor_of_isRepresentable 📖	mathematical	—	CategoryTheory.Presieve.IsSheafFor	—	CategoryTheory.Presieve.isSheafFor_comp_uliftFunctor_iff CategoryTheory.Presieve.isSheafFor_iso CategoryTheory.Functor.instIsRepresentableCompOppositeUliftFunctor iff_forall_isSheafFor_yoneda

CategoryTheory.Presieve.IsSheafFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singleton_of_isRepresentable_of_effectiveEpi 📖	mathematical	—	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Presieve.singleton	—	CategoryTheory.Presieve.EffectiveEpimorphic.isSheafFor_of_isRepresentable CategoryTheory.Sieve.effectiveEpimorphic_singleton

CategoryTheory.Sieve

Definitions

Name	Category	Theorems
EffectiveEpimorphic 📖	MathDef	1 math math: EffectiveEpimorphic.iff_forall_isSheafFor_yoneda
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

CategoryTheory.Sieve.EffectiveEpimorphic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_forall_isSheafFor_yoneda 📖	mathematical	—	CategoryTheory.Sieve.EffectiveEpimorphic CategoryTheory.Presieve.IsSheafFor CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Sieve.arrows	—	CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit

---

← Back to Index