Sieves

📁 Source: Mathlib/CategoryTheory/Subfunctor/Sieves.lean

Statistics

Metric	Count
Definitions familyOfElementsOfSection, sieveOfSection, familyOfElementsOfSection, sieveOfSection	4
Theorems family_of_elements_compatible, family_of_elements_compatible, sieveOfSection_apply	3
Total	7

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
familyOfElementsOfSection 📖	CompOp	2 math math: Subpresheaf.family_of_elements_compatible, family_of_elements_compatible
sieveOfSection 📖	CompOp	4 math math: CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection, Subpresheaf.family_of_elements_compatible, family_of_elements_compatible, sieveOfSection_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
family_of_elements_compatible 📖	mathematical	—	CategoryTheory.Presieve.FamilyOfElements.Compatible toFunctor Opposite CategoryTheory.Category.opposite Opposite.unop CategoryTheory.Sieve.arrows sieveOfSection familyOfElementsOfSection	—	CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.op_comp
sieveOfSection_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows Opposite.unop sieveOfSection CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types Opposite.op Set Set.instMembership obj CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
familyOfElementsOfSection 📖	CompOp	—
sieveOfSection 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
family_of_elements_compatible 📖	mathematical	—	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.Subfunctor.toFunctor Opposite CategoryTheory.Category.opposite Opposite.unop CategoryTheory.Sieve.arrows CategoryTheory.Subfunctor.sieveOfSection CategoryTheory.Subfunctor.familyOfElementsOfSection	—	CategoryTheory.Subfunctor.family_of_elements_compatible

---

← Back to Index