Pullback

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

Statistics

Metric	Count
Definitions sheafAdjunctionContinuous, sheafPullback, sheafAdjunctionContinuous, sheafPullback, sheafPullbackIso	5
Theorems instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat, instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify, instPreservesFiniteLimitsSheafSheafPullback, preservesFiniteLimits	4
Total	9

CategoryTheory.Functor

Definitions

Name	Category	Theorems
sheafAdjunctionContinuous 📖	CompOp	—
sheafPullback 📖	CompOp	2 math math: sheafPullbackConstruction.preservesFiniteLimits, SmallCategories.instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat

CategoryTheory.Functor.SmallCategories

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPreservesFiniteLimitsSheafSheafPullbackOfRepresentablyFlat 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPullback CategoryTheory.Functor.sheafPullbackConstruction.instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify CategoryTheory.Functor.instHasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Functor.comp CategoryTheory.CostructuredArrow.proj CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.types CategoryTheory.forget CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.GrothendieckTopology.Cover Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited	—	CategoryTheory.Functor.sheafPullbackConstruction.preservesFiniteLimits CategoryTheory.Functor.instHasLeftKanExtension CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self CategoryTheory.lan_preservesFiniteLimits_of_flat CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms

CategoryTheory.Functor.sheafPullbackConstruction

Definitions

Name	Category	Theorems
sheafAdjunctionContinuous 📖	CompOp	—
sheafPullback 📖	CompOp	1 math math: instPreservesFiniteLimitsSheafSheafPullback
sheafPullbackIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesFiniteLimitsSheafSheafPullback 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafPullback CategoryTheory.instHasWeakSheafifyOfHasSheafify	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.Limits.comp_preservesFiniteLimits CategoryTheory.instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint
preservesFiniteLimits 📖	mathematical	CategoryTheory.Functor.HasLeftKanExtension Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPullback instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify CategoryTheory.instHasWeakSheafifyOfHasSheafify	—	CategoryTheory.Limits.preservesFiniteLimits_of_natIso CategoryTheory.instHasWeakSheafifyOfHasSheafify instIsRightAdjointSheafSheafPushforwardContinuousOfHasWeakSheafify instPreservesFiniteLimitsSheafSheafPullback

---

← Back to Index