Commit 2023-04-10 18:08 9b532968

View on Github →

feat: port CategoryTheory.Sites.Plus (#3352)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Plus.lean

added def CategoryTheory.GrothendieckTopology.diagram

added def CategoryTheory.GrothendieckTopology.diagramFunctor

added def CategoryTheory.GrothendieckTopology.diagramNatTrans

added theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_comp

added theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_id

added theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_zero

added def CategoryTheory.GrothendieckTopology.diagramPullback

added theorem CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf

added def CategoryTheory.GrothendieckTopology.isoToPlus

added theorem CategoryTheory.GrothendieckTopology.isoToPlus_hom

added theorem CategoryTheory.GrothendieckTopology.isoToPlus_inv

added def CategoryTheory.GrothendieckTopology.plusFunctor

added def CategoryTheory.GrothendieckTopology.plusLift

added theorem CategoryTheory.GrothendieckTopology.plusLift_unique

added def CategoryTheory.GrothendieckTopology.plusMap

added theorem CategoryTheory.GrothendieckTopology.plusMap_comp

added theorem CategoryTheory.GrothendieckTopology.plusMap_id

added theorem CategoryTheory.GrothendieckTopology.plusMap_plusLift

added theorem CategoryTheory.GrothendieckTopology.plusMap_toPlus

added theorem CategoryTheory.GrothendieckTopology.plusMap_zero

added def CategoryTheory.GrothendieckTopology.plusObj

added theorem CategoryTheory.GrothendieckTopology.plus_hom_ext

added def CategoryTheory.GrothendieckTopology.toPlus

added def CategoryTheory.GrothendieckTopology.toPlusNatTrans

added theorem CategoryTheory.GrothendieckTopology.toPlus_naturality

added theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift