Over

📁 Source: Mathlib/CategoryTheory/Sites/Point/Over.lean

Statistics

Metric	Count
Definitions over	1
Theorems over_fiber, instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveHomOfHasSheafifyType, over	3
Total	4

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasEnoughPointsOverOverOfWEqualsLocallyBijectiveHomOfHasSheafifyType 📖	mathematical	—	HasEnoughPoints CategoryTheory.Over CategoryTheory.instCategoryOver over	—	HasEnoughPoints.exists_objectProperty CategoryTheory.ObjectProperty.instSmallOfObjOfSmall small_sigma CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall UnivLE.small UnivLE.self CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
over 📖	CompOp	2 math math: CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, over_fiber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
over_fiber 📖	mathematical	—	fiber CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.GrothendieckTopology.over over CategoryTheory.FunctorToTypes.fromOverFunctor	—	—

CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
over 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.GrothendieckTopology.over CategoryTheory.ObjectProperty.ofObj CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.obj CategoryTheory.types CategoryTheory.GrothendieckTopology.Point.fiber CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.GrothendieckTopology.Point.over	—	mk' CategoryTheory.Over.locallySmall CategoryTheory.Over.mk_surjective Equiv.surjective CategoryTheory.GrothendieckTopology.mem_over_iff Equiv.apply_symm_apply CategoryTheory.Sieve.exists_eq_ofArrows jointly_reflect_ofArrows_mem_of_small CategoryTheory.FunctorToTypes.mem_fromOverSubfunctor_iff CategoryTheory.Functor.map_comp

---

← Back to Index