CompatiblePlus

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

Statistics

Metric	Count
Definitions diagramCompIso, plusCompIso, plusFunctorWhiskerLeftIso, plusFunctorWhiskerRightIso	4
Theorems diagramCompIso_hom_ι, diagramCompIso_hom_ι_assoc, plusCompIso_inv_eq_plusLift, plusCompIso_whiskerLeft, plusCompIso_whiskerLeft_assoc, plusCompIso_whiskerRight, plusCompIso_whiskerRight_assoc, plusFunctorWhiskerLeftIso_hom_app, plusFunctorWhiskerLeftIso_inv_app, plusFunctorWhiskerRightIso_hom_app, plusFunctorWhiskerRightIso_inv_app, toPlus_comp_plusCompIso_inv, whiskerRight_toPlus_comp_plusCompIso_hom, whiskerRight_toPlus_comp_plusCompIso_hom_assoc, ι_plusCompIso_hom, ι_plusCompIso_hom_assoc	16
Total	20

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
diagramCompIso 📖	CompOp	4 math math: ι_plusCompIso_hom_assoc, diagramCompIso_hom_ι, diagramCompIso_hom_ι_assoc, ι_plusCompIso_hom
plusCompIso 📖	CompOp	14 math math: plusFunctorWhiskerLeftIso_inv_app, plusFunctorWhiskerRightIso_hom_app, plusCompIso_whiskerRight, ι_plusCompIso_hom_assoc, whiskerRight_toPlus_comp_plusCompIso_hom, plusCompIso_whiskerLeft_assoc, plusFunctorWhiskerLeftIso_hom_app, plusFunctorWhiskerRightIso_inv_app, toPlus_comp_plusCompIso_inv, plusCompIso_whiskerRight_assoc, whiskerRight_toPlus_comp_plusCompIso_hom_assoc, ι_plusCompIso_hom, plusCompIso_whiskerLeft, plusCompIso_inv_eq_plusLift
plusFunctorWhiskerLeftIso 📖	CompOp	2 math math: plusFunctorWhiskerLeftIso_inv_app, plusFunctorWhiskerLeftIso_hom_app
plusFunctorWhiskerRightIso 📖	CompOp	2 math math: plusFunctorWhiskerRightIso_hom_app, plusFunctorWhiskerRightIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagramCompIso_hom_ι 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Functor.comp diagram CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.MulticospanIndex.left Opposite.unop CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category diagramCompIso CategoryTheory.Limits.Multiequalizer.ι CategoryTheory.Functor.map CategoryTheory.Limits.multiequalizer	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π CategoryTheory.Category.comp_id CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp
diagramCompIso_hom_ι_assoc 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover diagram CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category diagramCompIso CategoryTheory.Limits.MulticospanIndex.left Opposite.unop CategoryTheory.Limits.Multiequalizer.ι CategoryTheory.Functor.map CategoryTheory.Limits.multiequalizer	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' diagramCompIso_hom_ι
plusCompIso_inv_eq_plusLift 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category plusCompIso plusLift CategoryTheory.Functor.whiskerRight toPlus	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape plusLift_unique toPlus_comp_plusCompIso_inv
plusCompIso_whiskerLeft 📖	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 plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom plusCompIso plusMap	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.NatTrans.naturality_assoc ι_plusCompIso_hom ι_plusCompIso_hom_assoc CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Category.assoc diagramCompIso_hom_ι CategoryTheory.Limits.limit.lift_π diagramCompIso_hom_ι_assoc CategoryTheory.NatTrans.naturality
plusCompIso_whiskerLeft_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 plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.hom plusCompIso plusMap	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' plusCompIso_whiskerLeft
plusCompIso_whiskerRight 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight plusMap CategoryTheory.Iso.hom plusCompIso	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit ι_plusCompIso_hom_assoc CategoryTheory.Limits.ι_colimMap CategoryTheory.Functor.map_comp CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Category.assoc ι_plusCompIso_hom CategoryTheory.Limits.Multiequalizer.hom_ext diagramCompIso_hom_ι CategoryTheory.Limits.Multiequalizer.lift_ι diagramCompIso_hom_ι_assoc
plusCompIso_whiskerRight_assoc 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight plusMap CategoryTheory.Iso.hom plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' plusCompIso_whiskerRight
plusFunctorWhiskerLeftIso_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 plusObj CategoryTheory.Functor.comp plusFunctor CategoryTheory.Iso.hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape plusFunctorWhiskerLeftIso plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
plusFunctorWhiskerLeftIso_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 plusFunctor plusObj CategoryTheory.Iso.inv CategoryTheory.Limits.hasLimitOfHasLimitsOfShape plusFunctorWhiskerLeftIso plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
plusFunctorWhiskerRightIso_hom_app 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp plusFunctor CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight CategoryTheory.Iso.hom CategoryTheory.Limits.hasLimitOfHasLimitsOfShape plusFunctorWhiskerRightIso plusObj plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
plusFunctorWhiskerRightIso_inv_app 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringRight plusFunctor CategoryTheory.Iso.inv CategoryTheory.Limits.hasLimitOfHasLimitsOfShape plusFunctorWhiskerRightIso plusObj plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
toPlus_comp_plusCompIso_inv 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape toPlus CategoryTheory.Iso.inv plusCompIso CategoryTheory.Functor.whiskerRight	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape whiskerRight_toPlus_comp_plusCompIso_hom
whiskerRight_toPlus_comp_plusCompIso_hom 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight toPlus CategoryTheory.Iso.hom plusCompIso	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc ι_plusCompIso_hom CategoryTheory.Limits.Multiequalizer.hom_ext diagramCompIso_hom_ι CategoryTheory.Limits.limit.lift_π
whiskerRight_toPlus_comp_plusCompIso_hom_assoc 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp plusObj CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Functor.whiskerRight toPlus CategoryTheory.Iso.hom plusCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_toPlus_comp_plusCompIso_hom
ι_plusCompIso_hom 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.unop diagram CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.colimit plusObj CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Limits.colimit.ι CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category plusCompIso CategoryTheory.Limits.hasColimitOfHasColimitsOfShape diagramCompIso	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.IsColimit.fac CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom CategoryTheory.Category.assoc
ι_plusCompIso_hom_assoc 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingMulticospan CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.PreservesLimit Cover.shape CategoryTheory.Limits.MulticospanIndex.multicospan Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Limits.PreservesColimitsOfShape	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite.unop diagram CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.colimit CategoryTheory.Functor.map CategoryTheory.Limits.colimit.ι plusObj CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category plusCompIso diagramCompIso CategoryTheory.Limits.hasColimitOfHasColimitsOfShape	—	CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_plusCompIso_hom

---

← Back to Index