SheafHom

📁 Source: Mathlib/CategoryTheory/Sites/SheafHom.lean

Statistics

Metric	Count
Definitions app, presheafHom, presheafHomSectionsEquiv, sheafHom, sheafHom', sheafHom'Iso, sheafHomSectionsEquiv	7
Theorems hom, app_cond, exists_app, isAmalgamation_iff, presheafHom_isSheafFor, presheafHom_map_app, presheafHom_map_app_op_mk_id, presheafHom_obj, sheafHomSectionsEquiv_symm_apply_coe_apply	9
Total	16

CategoryTheory

Definitions

Name	Category	Theorems
presheafHom 📖	CompOp	6 math math: presheafHom_obj, Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality, presheafHom_map_app, Presheaf.IsSheaf.hom, presheafHom_isSheafFor, presheafHom_map_app_op_mk_id
presheafHomSectionsEquiv 📖	CompOp	—
sheafHom 📖	CompOp	1 math math: sheafHomSectionsEquiv_symm_apply_coe_apply
sheafHom' 📖	CompOp	—
sheafHom'Iso 📖	CompOp	—
sheafHomSectionsEquiv 📖	CompOp	1 math math: sheafHomSectionsEquiv_symm_apply_coe_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presheafHom_isSheafFor 📖	mathematical	—	Presieve.IsSheafFor presheafHom Sieve.arrows	—	existsUnique_of_exists_of_unique Limits.IsLimit.hom_ext Category.assoc PresheafHom.IsSheafFor.app_cond Functor.map_comp op_comp Over.w Functor.map_comp_assoc PresheafHom.isAmalgamation_iff Category.id_comp Functor.map_id Category.comp_id op_id NatTrans.ext NatTrans.naturality
presheafHom_map_app 📖	mathematical	CategoryStruct.comp Category.toCategoryStruct	NatTrans.app Opposite Over Opposite.unop Opposite.op Category.opposite instCategoryOver Functor.comp Functor.op Over.forget Functor.map types presheafHom Quiver.Hom.op CategoryStruct.toQuiver	—	—
presheafHom_map_app_op_mk_id 📖	mathematical	—	NatTrans.app Opposite Over Opposite.unop Opposite.op Category.opposite instCategoryOver Functor.comp Functor.op Over.forget Functor.map types presheafHom Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct CategoryStruct.id	—	presheafHom_map_app Category.id_comp
presheafHom_obj 📖	mathematical	—	Functor.obj Opposite Category.opposite types presheafHom Quiver.Hom Functor Over Opposite.unop instCategoryOver CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.comp Functor.op Over.forget	—	—
sheafHomSectionsEquiv_symm_apply_coe_apply 📖	mathematical	—	Set Set.instMembership Functor.sections Opposite Category.opposite Sheaf.val types sheafHom DFunLike.coe Equiv Quiver.Hom Sheaf CategoryStruct.toQuiver Category.toCategoryStruct Sheaf.instCategorySheaf Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sheafHomSectionsEquiv Functor.map Over Opposite.unop instCategoryOver GrothendieckTopology.over GrothendieckTopology.overPullback	—	—

CategoryTheory.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom 📖	mathematical	CategoryTheory.Presheaf.IsSheaf	CategoryTheory.types CategoryTheory.presheafHom	—	CategoryTheory.isSheaf_iff_isSheaf_of_type CategoryTheory.presheafHom_isSheafFor CategoryTheory.Presheaf.isSheaf_iff_isLimit CategoryTheory.GrothendieckTopology.pullback_stable

CategoryTheory.PresheafHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAmalgamation_iff 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.presheafHom CategoryTheory.Sieve.arrows	CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation CategoryTheory.NatTrans.app Opposite CategoryTheory.Over Opposite.unop Opposite.op CategoryTheory.Category.opposite CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.forget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.presheafHom_map_app_op_mk_id CategoryTheory.NatTrans.ext' CategoryTheory.Sieve.downward_closed CategoryTheory.Category.id_comp CategoryTheory.FunctorToTypes.map_id_apply

CategoryTheory.PresheafHom.IsSheafFor

Definitions

Name	Category	Theorems
app 📖	CompOp	1 math math: app_cond

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_cond 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.presheafHom CategoryTheory.Sieve.arrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op app CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Over Opposite.unop CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.forget CategoryTheory.CategoryStruct.id CategoryTheory.NatTrans.app	—	exists_app
exists_app 📖	mathematical	CategoryTheory.Presieve.FamilyOfElements.Compatible CategoryTheory.presheafHom CategoryTheory.Sieve.arrows	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Over Opposite.unop CategoryTheory.instCategoryOver CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Over.forget CategoryTheory.CategoryStruct.id CategoryTheory.NatTrans.app	—	CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Over.w_assoc CategoryTheory.Category.comp_id CategoryTheory.NatTrans.naturality CategoryTheory.FunctorToTypes.map_id_apply CategoryTheory.presheafHom_map_app_op_mk_id CategoryTheory.Functor.map_comp_assoc CategoryTheory.op_comp CategoryTheory.Over.w CategoryTheory.Limits.IsLimit.fac

---

← Back to Index