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