CoherentSheaves

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

Statistics

Metric	Count
Definitions	0
Theorems isSheaf_yoneda_obj, subcanonical, isSheaf_coherent	3
Total	3

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_coherent 📖	mathematical	—	Presieve.IsSheaf coherentTopology Presieve.IsSheafFor Presieve.ofArrows	—	—

CategoryTheory.coherentTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_yoneda_obj 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	CategoryTheory.isSheaf_coherent CategoryTheory.EffectiveEpiFamily.effectiveEpiFamily CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit CategoryTheory.Sieve.generateFamily_eq CategoryTheory.Sieve.le_generate CategoryTheory.Presieve.restrict_extend CategoryTheory.Presieve.isAmalgamation_restrict CategoryTheory.Presieve.isAmalgamation_sieveExtend
subcanonical 📖	mathematical	—	CategoryTheory.GrothendieckTopology.Subcanonical CategoryTheory.coherentTopology	—	CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj isSheaf_yoneda_obj

---

← Back to Index