CompatibleSheafification

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

Statistics

Metric	Count
Definitions sheafificationWhiskerLeftIso, sheafificationWhiskerRightIso, sheafifyCompIso	3
Theorems sheafificationWhiskerLeftIso_hom_app, sheafificationWhiskerLeftIso_inv_app, sheafificationWhiskerRightIso_hom_app, sheafificationWhiskerRightIso_inv_app, sheafifyCompIso_inv_eq_sheafifyLift, toSheafify_comp_sheafifyCompIso_inv, toSheafify_comp_sheafifyCompIso_inv_assoc, whiskerRight_toSheafify_sheafifyCompIso_hom, whiskerRight_toSheafify_sheafifyCompIso_hom_assoc	9
Total	12

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
sheafificationWhiskerLeftIso 📖	CompOp	2 math math: sheafificationWhiskerLeftIso_hom_app, sheafificationWhiskerLeftIso_inv_app
sheafificationWhiskerRightIso 📖	CompOp	2 math math: sheafificationWhiskerRightIso_hom_app, sheafificationWhiskerRightIso_inv_app
sheafifyCompIso 📖	CompOp	10 math math: whiskerRight_toSheafify_sheafifyCompIso_hom_assoc, sheafificationWhiskerRightIso_hom_app, sheafifyCompIso_inv_eq_sheafifyLift, toSheafify_comp_sheafifyCompIso_inv_assoc, sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv, toSheafify_comp_sheafifyCompIso_inv, sheafificationWhiskerLeftIso_hom_app, sheafificationWhiskerLeftIso_inv_app, whiskerRight_toSheafify_sheafifyCompIso_hom, sheafificationWhiskerRightIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sheafificationWhiskerLeftIso_hom_app 📖	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.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.comp sheafification CategoryTheory.Iso.hom sheafificationWhiskerLeftIso sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.comp_id
sheafificationWhiskerLeftIso_inv_app 📖	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.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft sheafification CategoryTheory.Limits.hasLimitOfHasLimitsOfShape sheafify CategoryTheory.Iso.inv sheafificationWhiskerLeftIso sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.id_comp
sheafificationWhiskerRightIso_hom_app 📖	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.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafification CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom sheafificationWhiskerRightIso sheafify sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
sheafificationWhiskerRightIso_inv_app 📖	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.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight sheafification CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Iso.inv sheafificationWhiskerRightIso sheafify sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
sheafifyCompIso_inv_eq_sheafifyLift 📖	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.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape sheafifyCompIso sheafifyLift CategoryTheory.Functor.whiskerRight toSheafify HasSheafCompose.isSheaf CategoryTheory.hasSheafCompose_of_preservesMulticospan sheafify_isSheaf CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape	—	sheafifyLift_unique CategoryTheory.Limits.hasLimitOfHasLimitsOfShape HasSheafCompose.isSheaf CategoryTheory.hasSheafCompose_of_preservesMulticospan sheafify_isSheaf CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Iso.comp_inv_eq whiskerRight_toSheafify_sheafifyCompIso_hom
toSheafify_comp_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.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape toSheafify CategoryTheory.Iso.inv sheafifyCompIso CategoryTheory.Functor.whiskerRight	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Iso.comp_inv_eq whiskerRight_toSheafify_sheafifyCompIso_hom
toSheafify_comp_sheafifyCompIso_inv_assoc 📖	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.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape toSheafify CategoryTheory.Iso.inv sheafifyCompIso CategoryTheory.Functor.whiskerRight	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_comp_sheafifyCompIso_inv
whiskerRight_toSheafify_sheafifyCompIso_hom 📖	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.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight toSheafify CategoryTheory.Iso.hom sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight_comp CategoryTheory.Category.assoc plusCompIso_whiskerRight plusMap_comp whiskerRight_toPlus_comp_plusCompIso_hom
whiskerRight_toSheafify_sheafifyCompIso_hom_assoc 📖	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.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp sheafify CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight toSheafify CategoryTheory.Iso.hom sheafifyCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_toSheafify_sheafifyCompIso_hom

---

← Back to Index