Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-16 18:01 86b298f2

View on Github →

feat(category_theory/sites): grothendieck topologies (#4577)

Estimated changes

Created src/category_theory/sites/grothendieck.lean

added theorem category_theory.grothendieck_topology.arrow_intersect

added theorem category_theory.grothendieck_topology.arrow_max

added theorem category_theory.grothendieck_topology.arrow_stable

added theorem category_theory.grothendieck_topology.arrow_trans

added def category_theory.grothendieck_topology.atomic

added theorem category_theory.grothendieck_topology.bot_covering

added theorem category_theory.grothendieck_topology.bot_covers

added theorem category_theory.grothendieck_topology.covering_iff_covers_id

added theorem category_theory.grothendieck_topology.covering_of_eq_top

added def category_theory.grothendieck_topology.covers

added theorem category_theory.grothendieck_topology.covers_iff

added def category_theory.grothendieck_topology.dense

added theorem category_theory.grothendieck_topology.dense_covering

added def category_theory.grothendieck_topology.discrete

added theorem category_theory.grothendieck_topology.discrete_eq_top

added theorem category_theory.grothendieck_topology.intersection_covering

added theorem category_theory.grothendieck_topology.intersection_covering_iff

added theorem category_theory.grothendieck_topology.is_glb_Inf

added theorem category_theory.grothendieck_topology.mem_sieves_iff_coe

added theorem category_theory.grothendieck_topology.pullback_stable

added def category_theory.grothendieck_topology.right_ore_condition

added theorem category_theory.grothendieck_topology.right_ore_of_pullbacks

added theorem category_theory.grothendieck_topology.superset_covering

added theorem category_theory.grothendieck_topology.top_covering

added theorem category_theory.grothendieck_topology.top_covers

added theorem category_theory.grothendieck_topology.top_mem

added theorem category_theory.grothendieck_topology.transitive

added def category_theory.grothendieck_topology.trivial

added theorem category_theory.grothendieck_topology.trivial_covering

added theorem category_theory.grothendieck_topology.trivial_eq_bot

added structure category_theory.grothendieck_topology

Modified src/category_theory/sites/sieves.lean

added theorem category_theory.sieve.pullback_eq_top_of_mem

added theorem category_theory.sieve.pullback_id