Commit 2021-06-16 04:52 b8658928

View on Github →

feat(algebraic_geometry/Spec): Make Spec a functor. (#7790)

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

modified def algebraic_geometry.Scheme.Spec

added def algebraic_geometry.Scheme.Spec_map

added theorem algebraic_geometry.Scheme.Spec_map_comp

added theorem algebraic_geometry.Scheme.Spec_map_id

added def algebraic_geometry.Scheme.Spec_obj

added theorem algebraic_geometry.Scheme.Spec_obj_to_LocallyRingedSpace

Modified src/algebraic_geometry/Spec.lean

deleted def algebraic_geometry.Spec.LocallyRingedSpace

added def algebraic_geometry.Spec.LocallyRingedSpace_map

added theorem algebraic_geometry.Spec.LocallyRingedSpace_map_comp

added theorem algebraic_geometry.Spec.LocallyRingedSpace_map_id

added def algebraic_geometry.Spec.LocallyRingedSpace_obj

deleted def algebraic_geometry.Spec.PresheafedSpace

deleted def algebraic_geometry.Spec.SheafedSpace

added def algebraic_geometry.Spec.SheafedSpace_map

added theorem algebraic_geometry.Spec.SheafedSpace_map_comp

added theorem algebraic_geometry.Spec.SheafedSpace_map_id

added def algebraic_geometry.Spec.SheafedSpace_obj

added def algebraic_geometry.Spec.Top_map

added theorem algebraic_geometry.Spec.Top_map_comp

added theorem algebraic_geometry.Spec.Top_map_id

added def algebraic_geometry.Spec.Top_obj

added def algebraic_geometry.Spec.to_LocallyRingedSpace

added def algebraic_geometry.Spec.to_PresheafedSpace

added theorem algebraic_geometry.Spec.to_PresheafedSpace_map

added theorem algebraic_geometry.Spec.to_PresheafedSpace_map_op

added theorem algebraic_geometry.Spec.to_PresheafedSpace_obj

added theorem algebraic_geometry.Spec.to_PresheafedSpace_obj_op

added def algebraic_geometry.Spec.to_SheafedSpace

added def algebraic_geometry.Spec.to_Top

added theorem algebraic_geometry.local_ring_hom_comp_stalk_iso

added theorem algebraic_geometry.stalk_map_to_stalk