Commit 2023-11-13 10:29 a5f84091

View on Github →

feat(CategoryTheory/Sites): the topology on Over categories (#8329) Given a Grothendieck topology on a category C, this PR constructs the induced Grothendieck topology on the category Over X for any X : C.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.GrothendieckTopology.mem_over_iff

added def CategoryTheory.GrothendieckTopology.over

added theorem CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over

added theorem CategoryTheory.GrothendieckTopology.over_forget_compatiblePreserving

added theorem CategoryTheory.GrothendieckTopology.over_forget_coverLifting

added theorem CategoryTheory.GrothendieckTopology.over_forget_coverPreserving

added def CategoryTheory.Sieve.overEquiv

added theorem CategoryTheory.Sieve.overEquiv_iff

added theorem CategoryTheory.Sieve.overEquiv_pullback

added theorem CategoryTheory.Sieve.overEquiv_symm_iff

added theorem CategoryTheory.Sieve.overEquiv_symm_top

added theorem CategoryTheory.Sieve.overEquiv_top