RegularTopology

📁 Source: Mathlib/CategoryTheory/Sites/Coherent/RegularTopology.lean

Statistics

Metric	Count
Definitions	0
Theorems instEffectiveEpiComp, mem_sieves_iff_hasEffectiveEpi, mem_sieves_of_hasEffectiveEpi	3
Total	3

CategoryTheory.regularTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEffectiveEpiComp 📖	mathematical	—	CategoryTheory.EffectiveEpi CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.effectiveEpi_iff_effectiveEpiFamily CategoryTheory.Sieve.effectiveEpimorphic_family CategoryTheory.Sieve.pullback_comp CategoryTheory.GrothendieckTopology.pullback_stable' mem_sieves_of_hasEffectiveEpi CategoryTheory.Category.id_comp CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit isSheaf_yoneda_obj
mem_sieves_iff_hasEffectiveEpi 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.regularTopology CategoryTheory.EffectiveEpi CategoryTheory.Sieve.arrows	—	CategoryTheory.Category.id_comp CategoryTheory.IsSplitEpi.EffectiveEpi CategoryTheory.IsSplitEpi.of_iso CategoryTheory.IsIso.id instEffectiveEpiComp mem_sieves_of_hasEffectiveEpi
mem_sieves_of_hasEffectiveEpi 📖	mathematical	CategoryTheory.EffectiveEpi CategoryTheory.Sieve.arrows	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.regularTopology	—	CategoryTheory.Sieve.generate_le_iff CategoryTheory.Presieve.le_of_factorsThru_sieve CategoryTheory.Category.id_comp CategoryTheory.Coverage.saturate_of_superset

---

← Back to Index