Commit 2023-06-20 12:35 07d42215

View on Github →

feat: port AlgebraicGeometry.LocallyRingedSpace.HasColimits (#5260)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/LocallyRingedSpace/HasColimits.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_open

added theorem AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen_image_preimage

added theorem AlgebraicGeometry.LocallyRingedSpace.isLocalRingHom_stalkMap_congr

added theorem AlgebraicGeometry.SheafedSpace.colimit_exists_rep

added theorem AlgebraicGeometry.SheafedSpace.isColimit_exists_rep

Modified Mathlib/AlgebraicGeometry/SheafedSpace.lean