Commit 2022-08-24 09:35 a9402e0a

View on Github →

refactor(algebraic_geometry/*): Make LocallyRingedSpace.hom a custom structure. (#15973) We also define algebraic_geometry.Scheme.hom as an type alias for morphisms between schemes to enable dot notation.

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

Modified src/algebraic_geometry/Gamma_Spec_adjunction.lean

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.hom

deleted theorem algebraic_geometry.Scheme.id_coe_base

modified theorem algebraic_geometry.Scheme.id_val_base

deleted theorem algebraic_geometry.Scheme.preimage_basic_open'

Modified src/algebraic_geometry/Spec.lean

Modified src/algebraic_geometry/gluing.lean

Modified src/algebraic_geometry/locally_ringed_space.lean

added structure algebraic_geometry.LocallyRingedSpace.hom

deleted def algebraic_geometry.LocallyRingedSpace.hom

deleted theorem algebraic_geometry.LocallyRingedSpace.hom_ext

Modified src/algebraic_geometry/locally_ringed_space/has_colimits.lean

Modified src/algebraic_geometry/morphisms/basic.lean

Modified src/algebraic_geometry/morphisms/ring_hom_properties.lean

Modified src/algebraic_geometry/open_immersion.lean

added def algebraic_geometry.Scheme.hom.opens_functor

added def algebraic_geometry.Scheme.hom.opens_range

added theorem algebraic_geometry.Scheme.image_basic_open

deleted theorem algebraic_geometry.is_open_immersion.image_basic_open

deleted def algebraic_geometry.is_open_immersion.opens_range