Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-20 13:26 6cfc8d82

View on Github →

feat(algebraic_geometry/locally_ringed_space): LocallyRingedSpace is cocomplete. (#10791)

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/locally_ringed_space/has_colimits.lean

added def algebraic_geometry.LocallyRingedSpace.coequalizer

added def algebraic_geometry.LocallyRingedSpace.coequalizer_cofork

added def algebraic_geometry.LocallyRingedSpace.coequalizer_cofork_is_colimit

added def algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open

added theorem algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open_image_open

added theorem algebraic_geometry.LocallyRingedSpace.has_coequalizer.image_basic_open_image_preimage

added theorem algebraic_geometry.LocallyRingedSpace.is_local_ring_hom_stalk_map_congr

Modified src/algebraic_geometry/sheafed_space.lean

added theorem algebraic_geometry.SheafedSpace.comp_c_app'

added theorem algebraic_geometry.SheafedSpace.congr_app

Modified src/category_theory/limits/shapes/types.lean

added theorem category_theory.limits.types.coequalizer_preimage_image_eq_of_preimage_eq

Modified src/ring_theory/ideal/local_ring.lean

added theorem is_local_ring_hom_of_comp

added theorem ring_hom.domain_local_ring