Basic

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

Statistics

Metric	Count
Definitions comap, fiber, presheafFiber, presheafFiberCompIso, presheafFiberDesc, presheafToSheafCompSheafFiber, sheafFiber, sheafFiberCompIso, toPresheafFiber, toPresheafFiberNatTrans	10
Theorems W_isInvertedBy_presheafFiber, comap_fiber, initiallySmall, instHasColimitsOfShapeOppositeElementsFiber, instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, instIsIsoMapFunctorOppositePresheafFiberToSheafify, instPreservesColimitsOfShapeOppositeElementsFiberForget, instPreservesColimitsOfSizeFunctorOppositePresheafFiber, instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall, instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, isCofiltered, jointly_surjective, presheafFiber_hom_ext, presheafFiber_hom_ext_iff, sheafFiberCompIso_hom_app, sheafFiberCompIso_inv_app, toPresheafFiberNatTrans_app, toPresheafFiber_eq_iff', toPresheafFiber_jointly_surjective, toPresheafFiber_jointly_surjective₂, toPresheafFiber_map_bijective, toPresheafFiber_map_injective, toPresheafFiber_map_surjective, toPresheafFiber_naturality, toPresheafFiber_naturality_apply, toPresheafFiber_naturality_assoc, toPresheafFiber_presheafFiberCompIso_hom_app, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, toPresheafFiber_presheafFiberDesc, toPresheafFiber_presheafFiberDesc_assoc, toPresheafFiber_w, toPresheafFiber_w_apply, toPresheafFiber_w_assoc	34
Total	44

CategoryTheory.GrothendieckTopology.Point

Definitions

Name	Category	Theorems
comap 📖	CompOp	1 math math: comap_fiber
fiber 📖	CompOp	15 math math: Hom.presheafFiber_app, toPresheafFiber_eq_iff', comap_fiber, id_hom, toPresheafFiber_w, toPresheafFiber_w_apply, jointly_surjective, comp_hom, instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits, instHasColimitsOfShapeOppositeElementsFiber, toPresheafFiber_w_assoc, comp_hom_assoc, instPreservesColimitsOfShapeOppositeElementsFiberForget, isCofiltered, initiallySmall
presheafFiber 📖	CompOp	28 math math: Hom.presheafFiber_app, toPresheafFiber_presheafFiberDesc, toPresheafFiber_eq_iff', Hom.presheafFiber_comp, toPresheafFiber_naturality_assoc, toPresheafFiber_jointly_surjective, instPreservesColimitsOfSizeFunctorOppositePresheafFiber, toPresheafFiber_naturality_apply, toPresheafFiber_w, Hom.presheafFiber_comp_assoc, W_isInvertedBy_presheafFiber, toPresheafFiber_map_bijective, toPresheafFiber_w_apply, instIsIsoMapFunctorOppositePresheafFiberToSheafify, Hom.presheafFiber_id, toPresheafFiber_w_assoc, instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, toPresheafFiber_presheafFiberDesc_assoc, toPresheafFiber_map_injective, toPresheafFiber_jointly_surjective₂, toPresheafFiber_map_surjective, toPresheafFiber_naturality, toPresheafFiberNatTrans_app, presheafFiber_hom_ext_iff, sheafFiberCompIso_hom_app, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, sheafFiberCompIso_inv_app, toPresheafFiber_presheafFiberCompIso_hom_app
presheafFiberCompIso 📖	CompOp	4 math math: sheafFiberCompIso_hom_app, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, sheafFiberCompIso_inv_app, toPresheafFiber_presheafFiberCompIso_hom_app
presheafFiberDesc 📖	CompOp	3 math math: Hom.presheafFiber_app, toPresheafFiber_presheafFiberDesc, toPresheafFiber_presheafFiberDesc_assoc
presheafToSheafCompSheafFiber 📖	CompOp	—
sheafFiber 📖	CompOp	7 math math: instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize, Hom.sheafFiber_comp_assoc, Hom.sheafFiber_comp, instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall, Hom.sheafFiber_id, sheafFiberCompIso_hom_app, sheafFiberCompIso_inv_app
sheafFiberCompIso 📖	CompOp	2 math math: sheafFiberCompIso_hom_app, sheafFiberCompIso_inv_app
toPresheafFiber 📖	CompOp	16 math math: Hom.presheafFiber_app, toPresheafFiber_presheafFiberDesc, toPresheafFiber_eq_iff', toPresheafFiber_naturality_assoc, toPresheafFiber_jointly_surjective, toPresheafFiber_naturality_apply, toPresheafFiber_w, toPresheafFiber_w_apply, toPresheafFiber_w_assoc, toPresheafFiber_presheafFiberDesc_assoc, toPresheafFiber_jointly_surjective₂, toPresheafFiber_naturality, toPresheafFiberNatTrans_app, presheafFiber_hom_ext_iff, toPresheafFiber_presheafFiberCompIso_hom_app_assoc, toPresheafFiber_presheafFiberCompIso_hom_app
toPresheafFiberNatTrans 📖	CompOp	1 math math: toPresheafFiberNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_isInvertedBy_presheafFiber 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W presheafFiber	—	CategoryTheory.GrothendieckTopology.W_iff_isLocallyBijective CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.isIso_iff_bijective toPresheafFiber_map_bijective
comap_fiber 📖	mathematical	CategoryTheory.CoverPreserving	fiber comap CategoryTheory.Functor.comp CategoryTheory.types	—	—
initiallySmall 📖	mathematical	—	CategoryTheory.InitiallySmall CategoryTheory.Functor.Elements fiber CategoryTheory.categoryOfElements	—	—
instHasColimitsOfShapeOppositeElementsFiber 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements	—	CategoryTheory.Limits.hasColimitsOfShape_of_finallySmall CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall
instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements instHasColimitsOfShapeOppositeElementsFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.hasExactColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel CategoryTheory.AB5OfSize.ofShape
instIsIsoMapFunctorOppositePresheafFiberToSheafify 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.sheafify CategoryTheory.Functor.map CategoryTheory.toSheafify	—	W_isInvertedBy_presheafFiber CategoryTheory.GrothendieckTopology.W_toSheafify
instPreservesColimitsOfShapeOppositeElementsFiberForget 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types Opposite CategoryTheory.Functor.Elements fiber CategoryTheory.Category.opposite CategoryTheory.categoryOfElements CategoryTheory.forget	—	CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel
instPreservesColimitsOfSizeFunctorOppositePresheafFiber 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber	—	instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.comp_preservesColimitsOfShape CategoryTheory.whiskeringLeft_preservesColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Limits.instIsLeftAdjointFunctorColim
instPreservesColimitsOfSizeSheafSheafFiberOfHasSheafifyOfWEqualsLocallyBijectiveOfReflectsIsomorphismsOfPreservesFilteredColimitsOfSizeForgetOfLocallySmall 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafFiber	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape instPreservesColimitsOfSizeFunctorOppositePresheafFiber W_isInvertedBy_presheafFiber CategoryTheory.GrothendieckTopology.W_toSheafify CategoryTheory.Functor.map_comp CategoryTheory.Sheaf.sheafifyCocone_ι_app_val
instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.Limits.comp_preservesFiniteLimits instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.instPreservesFiniteLimitsFunctorObjWhiskeringLeftOfHasFiniteLimits CategoryTheory.HasExactColimitsOfShape.preservesFiniteLimits instHasExactColimitsOfShapeOppositeElementsFiberOfLocallySmallOfAB5OfSizeOfHasFiniteLimits
instPreservesFiniteLimitsSheafSheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafFiber	—	CategoryTheory.Limits.hasFilteredColimitsOfSize_of_hasColimitsOfSize CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.Sheaf.instPreservesFiniteLimitsFunctorOppositeSheafToPresheafOfHasFiniteLimits instPreservesFiniteLimitsFunctorOppositePresheafFiberOfLocallySmallOfHasFiniteLimitsOfAB5OfSize
isCofiltered 📖	mathematical	—	CategoryTheory.IsCofiltered CategoryTheory.Functor.Elements fiber CategoryTheory.categoryOfElements	—	—
jointly_surjective 📖	mathematical	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve	CategoryTheory.Functor.map CategoryTheory.types fiber	—	—
presheafFiber_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber	—	—	CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
presheafFiber_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber	—	presheafFiber_hom_ext
sheafFiberCompIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.sheafCompose sheafFiber CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category sheafFiberCompIso Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight presheafFiber presheafFiberCompIso CategoryTheory.Sheaf.val	—	CategoryTheory.Category.comp_id
sheafFiberCompIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp sheafFiber CategoryTheory.sheafCompose CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category sheafFiberCompIso Opposite CategoryTheory.Category.opposite presheafFiber CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight presheafFiberCompIso CategoryTheory.Sheaf.val	—	CategoryTheory.Category.id_comp
toPresheafFiberNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op presheafFiber toPresheafFiberNatTrans toPresheafFiber	—	—
toPresheafFiber_eq_iff' 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber CategoryTheory.Functor.map CategoryTheory.types fiber Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty isCofiltered CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_jointly_surjective 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_jointly_surjective₂ 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber CategoryTheory.Limits.Types.FilteredColimit.jointly_surjective_of_isColimit₂ CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty isCofiltered CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeOppositeElementsFiberForget
toPresheafFiber_map_bijective 📖	mathematical	—	Function.Bijective CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	toPresheafFiber_map_injective toPresheafFiber_map_surjective
toPresheafFiber_map_injective 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	jointly_surjective CategoryTheory.Presheaf.equalizerSieve_mem toPresheafFiber_jointly_surjective₂ toPresheafFiber_naturality_apply toPresheafFiber_w_apply
toPresheafFiber_map_surjective 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber DFunLike.coe CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map	—	toPresheafFiber_jointly_surjective jointly_surjective CategoryTheory.Presheaf.imageSieve_mem toPresheafFiber_naturality_apply CategoryTheory.comp_apply
toPresheafFiber_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.NatTrans.naturality
toPresheafFiber_naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Opposite.op toPresheafFiber CategoryTheory.NatTrans.app	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toPresheafFiber_naturality
toPresheafFiber_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.Functor.map CategoryTheory.NatTrans.app	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_naturality
toPresheafFiber_presheafFiberCompIso_hom_app 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom presheafFiberCompIso CategoryTheory.Functor.map	—	CategoryTheory.ι_preservesColimitIso_inv CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final CategoryTheory.isFiltered_op_of_isCofiltered isCofiltered CategoryTheory.instLocallySmallOpposite CategoryTheory.CategoryOfElements.instLocallySmallElements CategoryTheory.instFinallySmallOppositeOfInitiallySmall initiallySmall CategoryTheory.FinallySmall.instFinalFilteredFinalModelFromFilteredFinalModel CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.FinallySmall.instIsFilteredFilteredFinalModel CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
toPresheafFiber_presheafFiberCompIso_hom_app_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Functor.comp toPresheafFiber CategoryTheory.NatTrans.app CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom presheafFiberCompIso CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_presheafFiberCompIso_hom_app
toPresheafFiber_presheafFiberDesc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber presheafFiberDesc	—	CategoryTheory.Limits.colimit.ι_desc
toPresheafFiber_presheafFiberDesc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber presheafFiberDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_presheafFiberDesc
toPresheafFiber_w 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toPresheafFiber CategoryTheory.types fiber	—	CategoryTheory.Limits.colimit.w CategoryTheory.Limits.hasColimitOfHasColimitsOfShape instHasColimitsOfShapeOppositeElementsFiber
toPresheafFiber_w_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor CategoryTheory.Functor.category presheafFiber CategoryTheory.ConcreteCategory.hom toPresheafFiber CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.types fiber	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toPresheafFiber_w
toPresheafFiber_w_assoc 📖	mathematical	—	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.Functor CategoryTheory.Functor.category presheafFiber toPresheafFiber CategoryTheory.types fiber	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPresheafFiber_w

---

← Back to Index