Plus

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

Statistics

Metric	Count
Definitions diagram, diagramFunctor, diagramNatTrans, diagramPullback, isoToPlus, plusFunctor, plusLift, plusMap, plusObj, toPlus, toPlusNatTrans	11
Theorems diagramFunctor_map, diagramFunctor_obj, diagramNatTrans_app, diagramNatTrans_comp, diagramNatTrans_id, diagramNatTrans_zero, diagramPullback_app, diagram_map, diagram_obj, isIso_toPlus_of_isSheaf, isoToPlus_hom, isoToPlus_inv, plusFunctor_map, plusFunctor_obj, plusFunctor_preservesZeroMorphisms, plusLift_unique, plusMap_comp, plusMap_comp_assoc, plusMap_id, plusMap_plusLift, plusMap_toPlus, plusMap_zero, plus_hom_ext, toPlusNatTrans_app, toPlus_naturality, toPlus_naturality_assoc, toPlus_plusLift, toPlus_plusLift_assoc	28
Total	39

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
diagram 📖	CompOp	12 math math: diagram_obj, ι_plusCompIso_hom_assoc, diagramCompIso_hom_ι, diagramCompIso_hom_ι_assoc, diagram_map, diagramPullback_app, diagramFunctor_obj, diagramNatTrans_app, ι_plusCompIso_hom, diagramNatTrans_id, diagramNatTrans_zero, diagramNatTrans_comp
diagramFunctor 📖	CompOp	9 math math: coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt, liftToDiagramLimitObjAux_fac, liftToDiagramLimitObjAux_fac_assoc, preservesLimitsOfShape_diagramFunctor, diagramFunctor_map, diagramFunctor_obj, preservesLimits_diagramFunctor, coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app, preservesLimit_diagramFunctor
diagramNatTrans 📖	CompOp	5 math math: diagramFunctor_map, diagramNatTrans_app, diagramNatTrans_id, diagramNatTrans_zero, diagramNatTrans_comp
diagramPullback 📖	CompOp	1 math math: diagramPullback_app
isoToPlus 📖	CompOp	2 math math: isoToPlus_hom, isoToPlus_inv
plusFunctor 📖	CompOp	11 math math: plusFunctorWhiskerLeftIso_inv_app, plusFunctorWhiskerRightIso_hom_app, preservesLimitsOfShape_plusFunctor, preserveFiniteLimits_plusFunctor, plusFunctor_obj, plusFunctorWhiskerLeftIso_hom_app, plusFunctorWhiskerRightIso_inv_app, toPlusNatTrans_app, plusFunctor_map, plusFunctor_preservesZeroMorphisms, liftToPlusObjLimitObj_fac
plusLift 📖	CompOp	6 math math: toPlus_plusLift_assoc, plusMap_plusLift, isoToPlus_inv, plusLift_unique, toPlus_plusLift, plusCompIso_inv_eq_plusLift
plusMap 📖	CompOp	14 math math: plusCompIso_whiskerRight, plusMap_id, plusMap_toPlus, plusMap_plusLift, plusCompIso_whiskerLeft_assoc, plusMap_comp_assoc, plusFunctor_map, plusCompIso_whiskerRight_assoc, toPlus_naturality_assoc, toPlus_naturality, plusCompIso_whiskerLeft, liftToPlusObjLimitObj_fac, plusMap_zero, plusMap_comp
plusObj 📖	CompOp	38 math math: plusFunctorWhiskerLeftIso_inv_app, Plus.toPlus_mk, toPlus_plusLift_assoc, plusFunctorWhiskerRightIso_hom_app, plusCompIso_whiskerRight, ι_plusCompIso_hom_assoc, plusMap_id, Plus.toPlus_eq_mk, Plus.res_mk_eq_mk_pullback, whiskerRight_toPlus_comp_plusCompIso_hom, plusMap_toPlus, isoToPlus_hom, plusFunctor_obj, plusMap_plusLift, plusCompIso_whiskerLeft_assoc, plusFunctorWhiskerLeftIso_hom_app, plusFunctorWhiskerRightIso_inv_app, toPlus_comp_plusCompIso_inv, plusMap_comp_assoc, Plus.exists_of_sep, isoToPlus_inv, plusCompIso_whiskerRight_assoc, CategoryTheory.Presheaf.isLocallySurjective_toPlus, whiskerRight_toPlus_comp_plusCompIso_hom_assoc, toPlus_naturality_assoc, Plus.inj_of_sep, Plus.isSheaf_plus_plus, toPlus_naturality, Plus.isSheaf_of_sep, ι_plusCompIso_hom, plusCompIso_whiskerLeft, liftToPlusObjLimitObj_fac, toPlus_plusLift, CategoryTheory.Presheaf.isLocallyInjective_toPlus, plusMap_zero, Plus.toPlus_apply, plusMap_comp, isIso_toPlus_of_isSheaf
toPlus 📖	CompOp	18 math math: Plus.toPlus_mk, toPlus_plusLift_assoc, Plus.toPlus_eq_mk, whiskerRight_toPlus_comp_plusCompIso_hom, plusMap_toPlus, isoToPlus_hom, toPlus_comp_plusCompIso_inv, toPlusNatTrans_app, CategoryTheory.Presheaf.isLocallySurjective_toPlus, whiskerRight_toPlus_comp_plusCompIso_hom_assoc, toPlus_naturality_assoc, Plus.inj_of_sep, toPlus_naturality, toPlus_plusLift, CategoryTheory.Presheaf.isLocallyInjective_toPlus, Plus.toPlus_apply, isIso_toPlus_of_isSheaf, plusCompIso_inv_eq_plusLift
toPlusNatTrans 📖	CompOp	1 math math: toPlusNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
diagramFunctor_map 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Functor.map CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor diagramNatTrans	—	—
diagramFunctor_obj 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagramFunctor diagram	—	—
diagramNatTrans_app 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.NatTrans.app Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover diagram diagramNatTrans CategoryTheory.Limits.Multiequalizer.lift Opposite.unop CategoryTheory.Functor.obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.MulticospanIndex.left CategoryTheory.Limits.Multiequalizer.ι Opposite.op Cover.Arrow.Y	—	—
diagramNatTrans_comp 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	diagramNatTrans CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagram	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π_assoc
diagramNatTrans_id 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	diagramNatTrans CategoryTheory.CategoryStruct.id CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Cover Preorder.smallCategory instPreorderCover diagram	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Limits.Multiequalizer.lift.congr_simp CategoryTheory.Limits.limit.lift_π CategoryTheory.Category.id_comp
diagramNatTrans_zero 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	diagramNatTrans Quiver.Hom CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.instZeroHomFunctor Cover Preorder.smallCategory instPreorderCover diagram	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Limits.comp_zero CategoryTheory.Limits.Multiequalizer.lift.congr_simp CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.zero_comp
diagramPullback_app 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.NatTrans.app Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover diagram CategoryTheory.Functor.comp CategoryTheory.Functor.op pullback diagramPullback CategoryTheory.Limits.Multiequalizer.lift Opposite.unop CategoryTheory.Functor.obj CategoryTheory.Limits.Multiequalizer.ι Cover.Arrow.base	—	—
diagram_map 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Functor.map Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover diagram CategoryTheory.Limits.Multiequalizer.lift Opposite.unop CategoryTheory.Limits.multiequalizer CategoryTheory.Limits.Multiequalizer.ι Cover.Arrow.map Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
diagram_obj 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index	CategoryTheory.Functor.obj Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover diagram CategoryTheory.Limits.multiequalizer Opposite.unop	—	—
isIso_toPlus_of_isSheaf 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category plusObj toPlus	—	CategoryTheory.IsIso.comp_isIso' CategoryTheory.Presheaf.isSheaf_iff_multiequalizer CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.limit.lift_π CategoryTheory.IsIso.inv_hom_id_assoc CategoryTheory.IsIso.comp_isIso CategoryTheory.IsIso.inv_isIso CategoryTheory.Limits.isIso_ι_of_isInitial CategoryTheory.NatIso.isIso_of_isIso_app
isoToPlus_hom 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category plusObj isoToPlus toPlus	—	—
isoToPlus_inv 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category plusObj isoToPlus plusLift CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	plusLift_unique CategoryTheory.Iso.comp_inv_eq CategoryTheory.Category.id_comp
plusFunctor_map 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category plusFunctor plusMap	—	—
plusFunctor_obj 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category plusFunctor plusObj	—	—
plusFunctor_preservesZeroMorphisms 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms plusFunctor	—	CategoryTheory.NatTrans.ext' plusMap_zero CategoryTheory.NatTrans.app_zero
plusLift_unique 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus	plusLift	—	CategoryTheory.Iso.eq_comp_inv plusMap_comp toPlus_naturality plusMap_toPlus
plusMap_comp 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	plusMap CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.colimit.hom_ext diagramNatTrans_comp CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap_assoc
plusMap_comp_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj plusMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' plusMap_comp
plusMap_id 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	plusMap CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj	—	CategoryTheory.NatTrans.ext' diagramNatTrans_id CategoryTheory.NatTrans.id_app CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
plusMap_plusLift 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj plusMap plusLift	—	plusLift_unique CategoryTheory.Category.assoc toPlus_naturality toPlus_plusLift
plusMap_toPlus 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	plusMap plusObj toPlus	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.colimit.hom_ext OrderTop.le_top CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.colimit.w CategoryTheory.Category.assoc CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Limits.Multiequalizer.lift_ι CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.ι_colimMap_assoc CategoryTheory.Limits.colimit.ι_pre diagramPullback_app CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.Multiequalizer.condition
plusMap_zero 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	plusMap Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.instZeroHomFunctor plusObj	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.colimit.hom_ext diagramNatTrans_zero CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
plus_hom_ext 📖	—	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus	—	—	plusLift_unique
toPlusNatTrans_app 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id plusFunctor toPlusNatTrans toPlus	—	—
toPlus_naturality 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus plusMap	—	CategoryTheory.NatTrans.ext' CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.Multiequalizer.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.limit.lift_π_assoc CategoryTheory.NatTrans.naturality
toPlus_naturality_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus plusMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPlus_naturality
toPlus_plusLift 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus plusLift	—	CategoryTheory.Category.assoc CategoryTheory.Iso.comp_inv_eq toPlus_naturality
toPlus_plusLift_assoc 📖	mathematical	CategoryTheory.Limits.HasMultiequalizer Cover.shape Cover.index CategoryTheory.Limits.HasColimitsOfShape Opposite Cover CategoryTheory.Category.opposite Preorder.smallCategory instPreorderCover CategoryTheory.Presheaf.IsSheaf	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category plusObj toPlus plusLift	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toPlus_plusLift

---

← Back to Index