Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-11 14:46 233a802c

View on Github →

feat(algebraic_geometry/Scheme): Spec as Scheme (#4104)

def Spec (R : CommRing) : Scheme

Estimated changes

Modified src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.Spec

Modified src/algebraic_geometry/Spec.lean

added def algebraic_geometry.Spec.LocallyRingedSpace

Modified src/algebraic_geometry/presheafed_space.lean

added def algebraic_geometry.PresheafedSpace.of_restrict

added def algebraic_geometry.PresheafedSpace.restrict_top_iso

added def algebraic_geometry.PresheafedSpace.to_restrict_top

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

added def is_open_map.adjunction