Commit 2023-05-31 05:42 0cbb9b87

View on Github →

feat: port CategoryTheory.Sites.Closed (#3356)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Closed.lean

added def CategoryTheory.Functor.closedSieves

added def CategoryTheory.GrothendieckTopology.IsClosed

added def CategoryTheory.GrothendieckTopology.close

added theorem CategoryTheory.GrothendieckTopology.close_close

added theorem CategoryTheory.GrothendieckTopology.close_eq_self_of_isClosed

added theorem CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem

added theorem CategoryTheory.GrothendieckTopology.close_isClosed

added theorem CategoryTheory.GrothendieckTopology.closed_iff_closed

added def CategoryTheory.GrothendieckTopology.closureOperator

added theorem CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed

added theorem CategoryTheory.GrothendieckTopology.isClosed_iff_close_eq_self

added theorem CategoryTheory.GrothendieckTopology.isClosed_pullback

added theorem CategoryTheory.GrothendieckTopology.le_close

added theorem CategoryTheory.GrothendieckTopology.le_close_of_isClosed

added theorem CategoryTheory.GrothendieckTopology.monotone_close

added theorem CategoryTheory.GrothendieckTopology.pullback_close

added theorem CategoryTheory.classifier_isSheaf

added theorem CategoryTheory.le_topology_of_closedSieves_isSheaf

added def CategoryTheory.topologyOfClosureOperator

added theorem CategoryTheory.topologyOfClosureOperator_close

added theorem CategoryTheory.topologyOfClosureOperator_self

added theorem CategoryTheory.topology_eq_iff_same_sheaves