PreservesSheafification

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

Statistics

Metric	Count
Definitions composeAndSheafify, instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify, presheafToSheafCompComposeAndSheafifyIso, sheafComposeNatIso, sheafComposeNatTrans, sheafifyComposeIso, toPresheafToSheafCompComposeAndSheafify	7
Theorems le, W_isInvertedBy_whiskeringRight_presheafToSheaf, W_of_preservesSheafification, instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, instPreservesSheafification, instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms, preservesSheafification_iff_of_adjunctions, preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, instIsIsoFunctorOppositeSheafSheafComposeNatTrans, instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, presheafToSheafCompComposeAndSheafifyIso_inv_app, sheafComposeIso_hom_fac, sheafComposeIso_hom_fac_assoc, sheafComposeIso_inv_fac, sheafComposeIso_inv_fac_assoc, sheafComposeNatTrans_app_uniq, sheafComposeNatTrans_fac, toPresheafToSheafCompComposeAndSheafify_app	20
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify 📖	CompOp	—
presheafToSheafCompComposeAndSheafifyIso 📖	CompOp	1 math math: presheafToSheafCompComposeAndSheafifyIso_inv_app
sheafComposeNatIso 📖	CompOp	—
sheafComposeNatTrans 📖	CompOp	7 math math: instIsIsoFunctorOppositeSheafSheafComposeNatTrans, GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction, GrothendieckTopology.sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, sheafComposeNatTrans_app_uniq, GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose, GrothendieckTopology.instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction, sheafComposeNatTrans_fac
sheafifyComposeIso 📖	CompOp	5 math math: constantCommuteCompose_hom_app_val, sheafComposeIso_hom_fac, sheafComposeIso_inv_fac_assoc, sheafComposeIso_hom_fac_assoc, sheafComposeIso_inv_fac
toPresheafToSheafCompComposeAndSheafify 📖	CompOp	2 math math: toPresheafToSheafCompComposeAndSheafify_app, instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoFunctorOppositeSheafSheafComposeNatTrans 📖	mathematical	—	IsIso Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Functor.comp Functor.obj Functor.whiskeringRight sheafCompose sheafComposeNatTrans	—	GrothendieckTopology.preservesSheafification_iff_of_adjunctions_of_hasSheafCompose
instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify 📖	mathematical	—	IsIso Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Functor.comp Functor.obj Functor.whiskeringRight presheafToSheaf Sheaf.composeAndSheafify toPresheafToSheafCompComposeAndSheafify	—	NatTrans.isIso_iff_isIso_app GrothendieckTopology.W_iff GrothendieckTopology.W_of_preservesSheafification GrothendieckTopology.W_toSheafify
presheafToSheafCompComposeAndSheafifyIso_inv_app 📖	mathematical	—	NatTrans.app Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Functor.comp Functor.obj Functor.whiskeringRight presheafToSheaf Sheaf.composeAndSheafify Iso.inv presheafToSheafCompComposeAndSheafifyIso Functor.map Sheaf.val Functor.whiskerRight toSheafify	—	—
sheafComposeIso_hom_fac 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.comp sheafify toSheafify Iso.hom sheafifyComposeIso Functor.whiskerRight	—	sheafComposeNatTrans_fac
sheafComposeIso_hom_fac_assoc 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.comp sheafify toSheafify Iso.hom sheafifyComposeIso Functor.whiskerRight	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafComposeIso_hom_fac
sheafComposeIso_inv_fac 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.comp sheafify Functor.whiskerRight toSheafify Iso.inv sheafifyComposeIso	—	sheafComposeIso_hom_fac Category.assoc Iso.hom_inv_id Category.comp_id
sheafComposeIso_inv_fac_assoc 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.comp sheafify Functor.whiskerRight toSheafify Iso.inv sheafifyComposeIso	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafComposeIso_inv_fac
sheafComposeNatTrans_app_uniq 📖	mathematical	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.obj Functor.id Functor.comp Sheaf Sheaf.instCategorySheaf sheafToPresheaf sheafCompose NatTrans.app Adjunction.unit Functor.map Functor.whiskerRight	Functor.whiskeringRight sheafComposeNatTrans	—	Equiv.injective Equiv.apply_symm_apply Adjunction.homEquiv_unit
sheafComposeNatTrans_fac 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category Functor.obj Functor.id Functor.comp Sheaf Sheaf.instCategorySheaf sheafToPresheaf sheafCompose NatTrans.app Adjunction.unit Functor.map Functor.whiskeringRight sheafComposeNatTrans Functor.whiskerRight	—	Adjunction.homEquiv_counit Functor.map_comp Adjunction.unit_naturality_assoc Adjunction.right_triangle_components Category.comp_id
toPresheafToSheafCompComposeAndSheafify_app 📖	mathematical	—	NatTrans.app Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Functor.comp Functor.obj Functor.whiskeringRight presheafToSheaf Sheaf.composeAndSheafify toPresheafToSheafCompComposeAndSheafify Functor.map Sheaf.val Functor.whiskerRight toSheafify	—	—

CategoryTheory.GrothendieckTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
W_isInvertedBy_whiskeringRight_presheafToSheaf 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf W CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.presheafToSheaf	—	W_iff W_of_preservesSheafification
W_of_preservesSheafification 📖	mathematical	W	CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.whiskerRight	—	PreservesSheafification.le
instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.types CategoryTheory.forget	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.plusPlusSheaf CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.sheafCompose CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.sheafComposeNatTrans CategoryTheory.plusPlusAdjunction	—	CategoryTheory.NatIso.isIso_of_isIso_app CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.hasSheafCompose_of_preservesMulticospan instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction
instIsIsoSheafAppFunctorOppositeSheafComposeNatTransPlusPlusAdjunction 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.types CategoryTheory.forget	CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.plusPlusSheaf CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.sheafCompose CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.NatTrans.app CategoryTheory.sheafComposeNatTrans CategoryTheory.plusPlusAdjunction	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.isIso_iff_of_reflects_iso CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv CategoryTheory.Iso.isIso_inv
instPreservesSheafification 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.types CategoryTheory.forget	PreservesSheafification	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.hasSheafCompose_of_preservesMulticospan preservesSheafification_iff_of_adjunctions_of_hasSheafCompose instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction
instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms 📖	mathematical	CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.types CategoryTheory.forget CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory	PreservesSheafification	—	instPreservesSheafification CategoryTheory.Limits.Types.hasLimitsOfShape UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget
preservesSheafification_iff_of_adjunctions 📖	mathematical	—	PreservesSheafification CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.id CategoryTheory.sheafToPresheaf CategoryTheory.Functor.map CategoryTheory.Functor.whiskerRight CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit	—	W_iff_isIso_map_of_adjunction W_of_preservesSheafification CategoryTheory.Adjunction.instIsIsoMapAppUnitOfFaithfulOfFull CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.MorphismProperty.postcomp_iff CategoryTheory.MorphismProperty.Respects.toRespectsRight CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPostcompProperty CategoryTheory.Functor.whiskerRight_comp CategoryTheory.NatTrans.naturality CategoryTheory.MorphismProperty.precomp_iff CategoryTheory.MorphismProperty.Respects.toRespectsLeft CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty CategoryTheory.ObjectProperty.isLocal_of_isIso CategoryTheory.Functor.isIso_whiskerRight CategoryTheory.Functor.map_isIso
preservesSheafification_iff_of_adjunctions_of_hasSheafCompose 📖	mathematical	—	PreservesSheafification CategoryTheory.IsIso CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.sheafCompose CategoryTheory.sheafComposeNatTrans	—	preservesSheafification_iff_of_adjunctions CategoryTheory.NatTrans.isIso_iff_isIso_app W_iff_isIso_map_of_adjunction W_sheafToPresheaf_map_iff_isIso CategoryTheory.sheafComposeNatTrans_fac CategoryTheory.MorphismProperty.precomp_iff CategoryTheory.MorphismProperty.Respects.toRespectsLeft CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsLocal CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toHasOfPrecompProperty W_adj_unit_app
sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.types CategoryTheory.forget	CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.sheafToPresheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.plusPlusSheaf CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.sheafCompose CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.NatTrans.app CategoryTheory.sheafComposeNatTrans CategoryTheory.plusPlusAdjunction CategoryTheory.Iso.inv sheafify sheafifyCompIso	—	CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.hasSheafCompose_of_preservesMulticospan Equiv.injective CategoryTheory.Sheaf.cond HasSheafCompose.isSheaf sheafify_isSheaf CategoryTheory.Adjunction.mkOfHomEquiv_homEquiv sheafifyCompIso_inv_eq_sheafifyLift toSheafify_sheafifyLift CategoryTheory.Category.comp_id CategoryTheory.sheafComposeNatTrans_fac

CategoryTheory.GrothendieckTopology.PreservesSheafification

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le 📖	mathematical	—	CategoryTheory.MorphismProperty CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.GrothendieckTopology.W CategoryTheory.MorphismProperty.inverseImage CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight	—	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
composeAndSheafify 📖	CompOp	6 math math: CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app, adjunction_counit_app_val, adjunction_unit_app_val, CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app, instIsLeftAdjointComposeAndSheafify, CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify

---

← Back to Index