LeftExact

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

Statistics

Metric	Count
Definitions coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation, liftToDiagramLimitObj, liftToDiagramLimitObjAux, liftToPlusObjLimitObj, plusPlusFunctorIsoSheafification, plusPlusIsoSheafify, plusPlusSheafIsoPresheafToSheaf	7
Theorems coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app, liftToDiagramLimitObjAux_fac, liftToDiagramLimitObjAux_fac_assoc, liftToPlusObjLimitObj_fac, preserveFiniteLimits_plusFunctor, preservesFiniteLimits_sheafification, preservesLimit_diagramFunctor, preservesLimitsOfShape_diagramFunctor, preservesLimitsOfShape_plusFunctor, preservesLimitsOfShape_sheafification, preservesLimits_diagramFunctor, adhesive, balanced, finitary_extensive, instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify, instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify, instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover, instHasSheafifyType, preservesFiniteLimits_presheafToSheaf, preservesLimitsOfShape_presheafToSheaf, toSheafify_plusPlusIsoSheafify_hom, toSheafify_plusPlusIsoSheafify_hom_assoc	23
Total	30

CategoryTheory

Definitions

Name	Category	Theorems
plusPlusFunctorIsoSheafification 📖	CompOp	—
plusPlusIsoSheafify 📖	CompOp	2 math math: toSheafify_plusPlusIsoSheafify_hom, toSheafify_plusPlusIsoSheafify_hom_assoc
plusPlusSheafIsoPresheafToSheaf 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify 📖	mathematical	—	Adhesive Sheaf Sheaf.instCategorySheaf	—	adhesive_of_reflective Sheaf.instHasLimitsOfShape adhesive_functor Limits.functorCategoryHasLimitsOfShape Limits.functorCategoryHasColimitsOfShape Limits.hasColimitOfHasColimitsOfShape Sheaf.instHasColimitsOfShape instHasWeakSheafifyOfHasSheafify instFullSheafFunctorOppositeSheafToPresheaf instFaithfulSheafFunctorOppositeSheafToPresheaf Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify 📖	mathematical	—	FinitaryExtensive Sheaf Sheaf.instCategorySheaf	—	finitaryExtensive_of_reflective Sheaf.instHasFiniteCoproducts instHasWeakSheafifyOfHasSheafify FinitaryExtensive.hasFiniteCoproducts HasPullbacksOfInclusions.instOfHasPullbacks Limits.hasColimitsOfShape_discrete Finite.of_fintype Sheaf.instHasLimitsOfShape finitaryExtensive_functor instFullSheafFunctorOppositeSheafToPresheaf instFaithfulSheafFunctorOppositeSheafToPresheaf Limits.functorCategoryHasLimit Limits.hasLimitOfHasLimitsOfShape Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan
instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover 📖	mathematical	Limits.HasMultiequalizer GrothendieckTopology.Cover.shape GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape types forget Limits.PreservesLimitsOfShape Limits.WalkingMulticospan Limits.WalkingMulticospan.instSmallCategory Small	HasSheafify	—	HasSheafify.mk' preservesFiniteLimits_presheafToSheaf
instHasSheafifyType 📖	mathematical	—	HasSheafify types	—	instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover Limits.Types.hasLimit UnivLE.small UnivLE.self Limits.Types.hasColimitsOfShape Opposite.small Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Types.instIsEquivalenceForgetTypeHom reflectsIsomorphisms_of_full_and_faithful Types.instFullForgetTypeHom instFaithfulForget Functor.corepresentable_preservesLimitsOfShape Types.instIsCorepresentableForgetTypeHom Types.instPreservesLimitsOfSizeForgetTypeHom Limits.hasFiniteLimits_of_hasLimits Limits.Types.hasLimitsOfSize
preservesFiniteLimits_presheafToSheaf 📖	mathematical	Limits.HasMultiequalizer GrothendieckTopology.Cover.shape GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape types forget Limits.PreservesLimitsOfShape Limits.WalkingMulticospan Limits.WalkingMulticospan.instSmallCategory Small	Limits.PreservesFiniteLimits Functor Functor.category Sheaf Sheaf.instCategorySheaf plusPlusSheaf	—	Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize preservesLimitsOfShape_presheafToSheaf Limits.hasLimitsOfShape_of_hasFiniteLimits
preservesLimitsOfShape_presheafToSheaf 📖	mathematical	Limits.HasMultiequalizer GrothendieckTopology.Cover.shape GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape types forget Limits.PreservesLimitsOfShape Limits.WalkingMulticospan Limits.WalkingMulticospan.instSmallCategory Small	Functor Functor.category Sheaf Sheaf.instCategorySheaf plusPlusSheaf	—	Limits.preservesLimitsOfShape_of_equiv Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms Limits.hasLimitsOfShape_of_equivalence Limits.preservesLimitsOfShapeOfPreservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits Limits.PreservesLimitsOfShape.preservesLimit GrothendieckTopology.preservesLimitsOfShape_sheafification CreatesLimit.toReflectsLimit
toSheafify_plusPlusIsoSheafify_hom 📖	mathematical	Limits.HasMultiequalizer GrothendieckTopology.Cover.shape GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape types forget Limits.PreservesLimitsOfShape Limits.WalkingMulticospan Limits.WalkingMulticospan.instSmallCategory	CategoryStruct.comp Functor Category.toCategoryStruct Functor.category GrothendieckTopology.sheafify sheafify sheafToPresheaf_isRightAdjoint GrothendieckTopology.toSheafify Iso.hom plusPlusIsoSheafify toSheafify	—	sheafToPresheaf_isRightAdjoint Category.comp_id Adjunction.unit_leftAdjointUniq_hom_app
toSheafify_plusPlusIsoSheafify_hom_assoc 📖	mathematical	Limits.HasMultiequalizer GrothendieckTopology.Cover.shape GrothendieckTopology.Cover.index Limits.HasColimitsOfShape Opposite GrothendieckTopology.Cover Category.opposite Preorder.smallCategory GrothendieckTopology.instPreorderCover Limits.PreservesColimitsOfShape types forget Limits.PreservesLimitsOfShape Limits.WalkingMulticospan Limits.WalkingMulticospan.instSmallCategory	CategoryStruct.comp Functor Category.toCategoryStruct Functor.category GrothendieckTopology.sheafify GrothendieckTopology.toSheafify sheafify sheafToPresheaf_isRightAdjoint Iso.hom plusPlusIsoSheafify toSheafify	—	sheafToPresheaf_isRightAdjoint Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_plusPlusIsoSheafify_hom

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation 📖	CompOp	2 math math: coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app
liftToDiagramLimitObj 📖	CompOp	—
liftToDiagramLimitObjAux 📖	CompOp	2 math math: liftToDiagramLimitObjAux_fac, liftToDiagramLimitObjAux_fac_assoc
liftToPlusObjLimitObj 📖	CompOp	1 math math: liftToPlusObjLimitObj_fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op Cover.Arrow.Y coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation Cover Preorder.smallCategory instPreorderCover diagramFunctor	—	—
coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite Cover Preorder.smallCategory instPreorderCover diagramFunctor CategoryTheory.evaluation Opposite.op Cover.Arrow.Y CategoryTheory.Limits.Cone.π coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Multiequalizer.ι	—	—
liftToDiagramLimitObjAux_fac 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.Limits.limit CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.flip Opposite.op Cover.Arrow.Y Opposite.unop liftToDiagramLimitObjAux CategoryTheory.NatTrans.app CategoryTheory.Limits.limit.π CategoryTheory.Functor.const CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Multiequalizer.ι	—	CategoryTheory.Limits.IsLimit.fac
liftToDiagramLimitObjAux_fac_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor CategoryTheory.Functor.obj CategoryTheory.evaluation CategoryTheory.Limits.limit CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.flip Opposite.op Cover.Arrow.Y Opposite.unop liftToDiagramLimitObjAux CategoryTheory.NatTrans.app CategoryTheory.Limits.limit.π CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π CategoryTheory.Limits.Multiequalizer.ι	—	CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftToDiagramLimitObjAux_fac
liftToPlusObjLimitObj_fac 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget Small	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.Functor.category plusFunctor CategoryTheory.Functor.obj CategoryTheory.evaluation Opposite.op plusObj CategoryTheory.Limits.limit CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.flip liftToPlusObjLimitObj CategoryTheory.NatTrans.app plusMap CategoryTheory.Limits.limit.π CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π	—	CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape preservesLimit_diagramFunctor CategoryTheory.Limits.IsLimit.fac CategoryTheory.Category.assoc CategoryTheory.Iso.eq_inv_comp CategoryTheory.Iso.inv_comp_eq CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom_assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc CategoryTheory.Iso.comp_inv_eq CategoryTheory.Limits.colimit.ι_desc
preserveFiniteLimits_plusFunctor 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget Small	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor CategoryTheory.Functor.category plusFunctor	—	CategoryTheory.Limits.preservesFiniteLimits_of_preservesFiniteLimitsOfSize CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits preservesLimitsOfShape_plusFunctor
preservesFiniteLimits_sheafification 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget Small	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor CategoryTheory.Functor.category sheafification	—	CategoryTheory.Limits.comp_preservesFiniteLimits preserveFiniteLimits_plusFunctor
preservesLimit_diagramFunctor 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Limits.PreservesLimit CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor	—	CategoryTheory.Limits.preservesLimit_of_evaluation CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Limits.Multiequalizer.lift_ι_assoc liftToDiagramLimitObjAux_fac CategoryTheory.Limits.limit_obj_ext CategoryTheory.Limits.limit.lift_π
preservesLimitsOfShape_diagramFunctor 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor	—	preservesLimit_diagramFunctor
preservesLimitsOfShape_plusFunctor 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget Small	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Functor CategoryTheory.Functor.category plusFunctor	—	CategoryTheory.Limits.preservesLimit_of_evaluation CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone CategoryTheory.Limits.functorCategoryHasLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape liftToPlusObjLimitObj_fac preservesLimit_diagramFunctor CategoryTheory.Limits.limit.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.colimit.ι_map CategoryTheory.Limits.colimit.ι_desc_assoc CategoryTheory.Limits.functorCategoryHasColimit CategoryTheory.Limits.ι_colimitLimitIso_limit_π_assoc CategoryTheory.Limits.hasColimitCompEvaluation CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom CategoryTheory.NatTrans.comp_app
preservesLimitsOfShape_sheafification 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget Small	CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Functor CategoryTheory.Functor.category sheafification	—	CategoryTheory.Limits.comp_preservesLimitsOfShape preservesLimitsOfShape_plusFunctor
preservesLimits_diagramFunctor 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Limits.PreservesLimits CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor	—	preservesLimitsOfShape_diagramFunctor CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits

CategoryTheory.SheafOfTypes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adhesive 📖	mathematical	—	CategoryTheory.Adhesive CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify CategoryTheory.Type.adhesive CategoryTheory.Limits.Types.instHasPullbacksType CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Limits.hasFiniteColimits_of_hasColimits CategoryTheory.Limits.Types.hasColimitsOfSize UnivLE.self
balanced 📖	mathematical	—	CategoryTheory.Balanced CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.Adhesive.toRegularMonoCategory adhesive
finitary_extensive 📖	mathematical	—	CategoryTheory.FinitaryExtensive CategoryTheory.Sheaf CategoryTheory.types CategoryTheory.Sheaf.instCategorySheaf	—	CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify CategoryTheory.types.finitaryExtensive CategoryTheory.Limits.Types.instHasPullbacksType

---

← Back to Index