CoherentTopology

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

Statistics

Metric	Count
Definitions	0
Theorems transitive_of_finite, mem_sieves_iff_hasEffectiveEpiFamily, mem_sieves_of_hasEffectiveEpiFamily, precoherentEffectiveEpiFamilyCompEffectiveEpis	4
Total	4

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
precoherentEffectiveEpiFamilyCompEffectiveEpis 📖	mathematical	EffectiveEpi	EffectiveEpiFamily CategoryStruct.comp Category.toCategoryStruct	—	EffectiveEpiFamily.reindex EffectiveEpiFamily.transitive_of_finite Finite.of_fintype

CategoryTheory.EffectiveEpiFamily

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
transitive_of_finite 📖	mathematical	Finite CategoryTheory.EffectiveEpiFamily	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Sieve.effectiveEpimorphic_family CategoryTheory.Sieve.pullback_comp CategoryTheory.GrothendieckTopology.pullback_stable' CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily CategoryTheory.Category.id_comp CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit CategoryTheory.coherentTopology.isSheaf_yoneda_obj

CategoryTheory.coherentTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_sieves_iff_hasEffectiveEpiFamily 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.coherentTopology CategoryTheory.EffectiveEpiFamily CategoryTheory.Sieve.arrows	—	CategoryTheory.Category.id_comp Finite.of_fintype CategoryTheory.instEffectiveEpiFamily CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.IsIso.id Finite.instSigma CategoryTheory.EffectiveEpiFamily.transitive_of_finite mem_sieves_of_hasEffectiveEpiFamily
mem_sieves_of_hasEffectiveEpiFamily 📖	mathematical	CategoryTheory.EffectiveEpiFamily CategoryTheory.Sieve.arrows	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.coherentTopology	—	CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_superset

---

← Back to Index