Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-11-08 02:28
f384f5d1
View on Github →
refactor(topology/sheaf_condition): remove has_products for restriction to open subspace (
#17361
)
Estimated changes
Modified
src/algebraic_geometry/open_immersion.lean
modified
def
algebraic_geometry.SheafedSpace.is_open_immersion
Modified
src/algebraic_geometry/sheafed_space.lean
Modified
src/category_theory/sites/cover_preserving.lean
added
theorem
category_theory.compatible_preserving_of_downwards_closed
Modified
src/topology/sheaves/sheaf_condition/equalizer_products.lean
deleted
def
Top.presheaf.sheaf_condition_equalizer_products.cover.of_open_embedding
deleted
def
Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_open_embedding
deleted
def
Top.presheaf.sheaf_condition_equalizer_products.fork.iso_of_open_embedding
deleted
def
Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_open_embedding
deleted
def
Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_open_embedding
Modified
src/topology/sheaves/sheaf_condition/opens_le_cover.lean
Modified
src/topology/sheaves/sheaf_condition/pairwise_intersections.lean
Modified
src/topology/sheaves/sheaf_condition/sites.lean
added
theorem
Top.presheaf.is_sheaf_of_open_embedding
added
theorem
is_open_map.cover_preserving
added
theorem
open_embedding.compatible_preserving