Category

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

Statistics

Metric	Count
Definitions hom, presheafFiber, sheafFiber, instCategory	4
Theorems ext, ext_iff, presheafFiber_app, presheafFiber_comp, presheafFiber_comp_assoc, presheafFiber_id, sheafFiber_comp, sheafFiber_comp_assoc, sheafFiber_id, comp_hom, comp_hom_assoc, hom_ext, hom_ext_iff, id_hom	14
Total	18

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
instCategory 📖	CompOp	23 math math: id_hom, Hom.presheafFiber_comp, CategoryTheory.GrothendieckTopology.HasEnoughPoints.exists_objectProperty, Hom.sheafFiber_comp_assoc, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectMonomorphisms, Hom.presheafFiber_comp_assoc, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.over, CategoryTheory.GrothendieckTopology.pointBotFunctor_map_hom, CategoryTheory.GrothendieckTopology.pointBotFunctor_obj, Hom.sheafFiber_comp, Opens.instIsThinPointOpensGrothendieckTopology, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type, Hom.presheafFiber_id, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyFaithful, comp_hom, Hom.sheafFiber_id, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.W_iff, comp_hom_assoc, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem, CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectEpimorphisms, CategoryTheory.GrothendieckTopology.instSmallPointBotPointsBotOfSmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category fiber	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category fiber Hom.hom CategoryTheory.GrothendieckTopology.Point instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Functor CategoryTheory.types CategoryTheory.Functor.category fiber	—	—

CategoryTheory.GrothendieckTopology.Point.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	7 math math: presheafFiber_app, CategoryTheory.GrothendieckTopology.Point.id_hom, ext_iff, CategoryTheory.GrothendieckTopology.pointBotFunctor_map_hom, CategoryTheory.GrothendieckTopology.Point.hom_ext_iff, CategoryTheory.GrothendieckTopology.Point.comp_hom, CategoryTheory.GrothendieckTopology.Point.comp_hom_assoc
presheafFiber 📖	CompOp	4 math math: presheafFiber_app, presheafFiber_comp, presheafFiber_comp_assoc, presheafFiber_id
sheafFiber 📖	CompOp	3 math math: sheafFiber_comp_assoc, sheafFiber_comp, sheafFiber_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
presheafFiber_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.Point.presheafFiber presheafFiber CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc CategoryTheory.Functor.obj CategoryTheory.GrothendieckTopology.Point.toPresheafFiber CategoryTheory.types CategoryTheory.GrothendieckTopology.Point.fiber hom	—	—
presheafFiber_comp 📖	mathematical	—	presheafFiber CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.Point.presheafFiber	—	CategoryTheory.NatTrans.ext' CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc_assoc
presheafFiber_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.presheafFiber presheafFiber CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' presheafFiber_comp
presheafFiber_id 📖	mathematical	—	presheafFiber CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.Point.presheafFiber	—	CategoryTheory.NatTrans.ext' CategoryTheory.GrothendieckTopology.Point.presheafFiber_hom_ext CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc CategoryTheory.Category.comp_id
sheafFiber_comp 📖	mathematical	—	sheafFiber CategoryTheory.CategoryStruct.comp CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.Point.sheafFiber	—	CategoryTheory.NatTrans.ext' presheafFiber_comp
sheafFiber_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.sheafFiber sheafFiber CategoryTheory.GrothendieckTopology.Point CategoryTheory.GrothendieckTopology.Point.instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafFiber_comp
sheafFiber_id 📖	mathematical	—	sheafFiber CategoryTheory.CategoryStruct.id CategoryTheory.GrothendieckTopology.Point CategoryTheory.Category.toCategoryStruct CategoryTheory.GrothendieckTopology.Point.instCategory CategoryTheory.Functor CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.GrothendieckTopology.Point.sheafFiber	—	CategoryTheory.NatTrans.ext' presheafFiber_id

---

← Back to Index