Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-14 12:57 1367c19b

View on Github →

feat(algebraic_geometry): LocallyRingedSpace has coproducts. (#10665)

Estimated changes

Created src/algebraic_geometry/locally_ringed_space/has_colimits.lean

added def algebraic_geometry.LocallyRingedSpace.coproduct

added def algebraic_geometry.LocallyRingedSpace.coproduct_cofan

added def algebraic_geometry.LocallyRingedSpace.coproduct_cofan_is_colimit

added theorem algebraic_geometry.SheafedSpace.colimit_exists_rep

added theorem algebraic_geometry.SheafedSpace.is_colimit_exists_rep

Modified src/algebraic_geometry/open_immersion.lean

added theorem algebraic_geometry.SheafedSpace.is_open_immersion.image_preimage_is_empty

added theorem algebraic_geometry.SheafedSpace.is_open_immersion.sigma_ι_open_embedding

Modified src/algebraic_geometry/sheafed_space.lean

Modified src/topology/category/Top/basic.lean

added theorem Top.open_embedding_iff_comp_is_iso

added theorem Top.open_embedding_iff_is_iso_comp

Modified src/topology/maps.lean

added theorem open_embedding_iff_open_embedding_compose

added theorem open_embedding_of_open_embedding_compose