Commit 2023-03-23 19:08 6daa6eb0

View on Github →

feat: Port CategoryTheory.Sites.Grothendieck (#2795)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Grothendieck.lean

added def CategoryTheory.GrothendieckTopology.Cover.Arrow.base

added theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.from_middle_condition

added def CategoryTheory.GrothendieckTopology.Cover.Arrow.map

added theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec

added theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition

added structure CategoryTheory.GrothendieckTopology.Cover.Arrow

added def CategoryTheory.GrothendieckTopology.Cover.Relation.base

added theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_fst

added theorem CategoryTheory.GrothendieckTopology.Cover.Relation.base_snd

added def CategoryTheory.GrothendieckTopology.Cover.Relation.fst

added def CategoryTheory.GrothendieckTopology.Cover.Relation.map

added theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_fst

added theorem CategoryTheory.GrothendieckTopology.Cover.Relation.map_snd

added def CategoryTheory.GrothendieckTopology.Cover.Relation.snd

added structure CategoryTheory.GrothendieckTopology.Cover.Relation

added def CategoryTheory.GrothendieckTopology.Cover.bind

added def CategoryTheory.GrothendieckTopology.Cover.bindToBase

added theorem CategoryTheory.GrothendieckTopology.Cover.coe_pullback

added theorem CategoryTheory.GrothendieckTopology.Cover.condition

added theorem CategoryTheory.GrothendieckTopology.Cover.ext

added def CategoryTheory.GrothendieckTopology.Cover.index

added def CategoryTheory.GrothendieckTopology.Cover.pullback

added def CategoryTheory.GrothendieckTopology.Cover.pullbackComp

added def CategoryTheory.GrothendieckTopology.Cover.pullbackId

added def CategoryTheory.GrothendieckTopology.Cover.sieve

added def CategoryTheory.GrothendieckTopology.Cover

added def CategoryTheory.GrothendieckTopology.Covers

added def CategoryTheory.GrothendieckTopology.RightOreCondition

added theorem CategoryTheory.GrothendieckTopology.arrow_intersect

added theorem CategoryTheory.GrothendieckTopology.arrow_max

added theorem CategoryTheory.GrothendieckTopology.arrow_stable

added theorem CategoryTheory.GrothendieckTopology.arrow_trans

added def CategoryTheory.GrothendieckTopology.atomic

added theorem CategoryTheory.GrothendieckTopology.bind_covering

added theorem CategoryTheory.GrothendieckTopology.bot_covering

added theorem CategoryTheory.GrothendieckTopology.bot_covers

added theorem CategoryTheory.GrothendieckTopology.covering_iff_covers_id

added theorem CategoryTheory.GrothendieckTopology.covering_of_eq_top

added theorem CategoryTheory.GrothendieckTopology.covers_iff

added def CategoryTheory.GrothendieckTopology.dense

added theorem CategoryTheory.GrothendieckTopology.dense_covering

added def CategoryTheory.GrothendieckTopology.discrete

added theorem CategoryTheory.GrothendieckTopology.discrete_eq_top

added theorem CategoryTheory.GrothendieckTopology.ext

added theorem CategoryTheory.GrothendieckTopology.intersection_covering

added theorem CategoryTheory.GrothendieckTopology.intersection_covering_iff

added theorem CategoryTheory.GrothendieckTopology.isGLB_infₛ

added theorem CategoryTheory.GrothendieckTopology.le_def

added def CategoryTheory.GrothendieckTopology.pullback

added def CategoryTheory.GrothendieckTopology.pullbackComp

added def CategoryTheory.GrothendieckTopology.pullbackId

added theorem CategoryTheory.GrothendieckTopology.pullback_stable

added theorem CategoryTheory.GrothendieckTopology.right_ore_of_pullbacks

added theorem CategoryTheory.GrothendieckTopology.superset_covering

added theorem CategoryTheory.GrothendieckTopology.top_covering

added theorem CategoryTheory.GrothendieckTopology.top_covers

added theorem CategoryTheory.GrothendieckTopology.top_mem

added theorem CategoryTheory.GrothendieckTopology.transitive

added def CategoryTheory.GrothendieckTopology.trivial

added theorem CategoryTheory.GrothendieckTopology.trivial_covering

added theorem CategoryTheory.GrothendieckTopology.trivial_eq_bot

added structure CategoryTheory.GrothendieckTopology