Commit 2020-08-31 05:09 b79fc037

View on Github →

feature(algebraic_geometry/Scheme): the category of schemes (#3961) The definition of a Scheme, and the category of schemes as the full subcategory of locally ringed spaces.

Estimated changes

Modified src/algebra/ring/basic.lean

added theorem ring_hom.is_unit_map

Created src/algebraic_geometry/Scheme.lean

added def algebraic_geometry.Scheme.empty

added def algebraic_geometry.Scheme.to_LocallyRingedSpace

added structure algebraic_geometry.Scheme

Created src/algebraic_geometry/Spec.lean

added def algebraic_geometry.Spec.PresheafedSpace

added def algebraic_geometry.Spec.SheafedSpace

Created src/algebraic_geometry/locally_ringed_space.lean

added def algebraic_geometry.LocallyRingedSpace.comp

added def algebraic_geometry.LocallyRingedSpace.forget_to_SheafedSpace

added def algebraic_geometry.LocallyRingedSpace.hom

added theorem algebraic_geometry.LocallyRingedSpace.hom_ext

added def algebraic_geometry.LocallyRingedSpace.id

added def algebraic_geometry.LocallyRingedSpace.stalk

added def algebraic_geometry.LocallyRingedSpace.stalk_map

added def algebraic_geometry.LocallyRingedSpace.to_Top

added def algebraic_geometry.LocallyRingedSpace.𝒪

added structure algebraic_geometry.LocallyRingedSpace

Modified src/algebraic_geometry/presheafed_space.lean

modified theorem algebraic_geometry.PresheafedSpace.as_coe

added def algebraic_geometry.PresheafedSpace.const

modified theorem algebraic_geometry.PresheafedSpace.mk_coe

added def algebraic_geometry.PresheafedSpace.restrict

added theorem category_theory.functor.map_presheaf_obj_presheaf

deleted theorem category_theory.functor.map_presheaf_obj_𝒪

Modified src/algebraic_geometry/prime_spectrum.lean

added def prime_spectrum.basic_open

added theorem prime_spectrum.basic_open_open

added theorem prime_spectrum.punit

Created src/algebraic_geometry/sheafed_space.lean

added theorem algebraic_geometry.SheafedSpace.as_coe

added theorem algebraic_geometry.SheafedSpace.comp_base

added theorem algebraic_geometry.SheafedSpace.comp_c_app

added def algebraic_geometry.SheafedSpace.forget

added def algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace

added theorem algebraic_geometry.SheafedSpace.id_base

added theorem algebraic_geometry.SheafedSpace.id_c

added theorem algebraic_geometry.SheafedSpace.id_c_app

added theorem algebraic_geometry.SheafedSpace.mk_coe

added def algebraic_geometry.SheafedSpace.punit

added def algebraic_geometry.SheafedSpace.restrict

added def algebraic_geometry.SheafedSpace.sheaf

added structure algebraic_geometry.SheafedSpace

Modified src/algebraic_geometry/stalks.lean

modified def algebraic_geometry.PresheafedSpace.stalk

Modified src/algebraic_geometry/structure_sheaf.lean

added def algebraic_geometry.stalk_iso

added def algebraic_geometry.stalk_iso_Type

added def algebraic_geometry.stalk_to_fiber_ring_hom

added theorem algebraic_geometry.structure_sheaf_stalk_to_fiber_injective

added theorem algebraic_geometry.structure_sheaf_stalk_to_fiber_surjective

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.jointly_surjective'

Modified src/data/equiv/transfer_instance.lean

Modified src/ring_theory/ideal/basic.lean

added theorem is_unit_map_iff

added theorem local_of_surjective

Modified src/ring_theory/localization.lean

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

added def is_open_map.functor

added def topological_space.opens.inclusion

added theorem topological_space.opens.inclusion_open_embedding

Modified src/topology/opens.lean

added theorem topological_space.opens.coe_inf

added theorem topological_space.opens.le_def

added theorem topological_space.opens.mk_inf_mk

added theorem topological_space.opens.supr_mk

Modified src/topology/sheaves/local_predicate.lean

added theorem Top.prelocal_predicate.sheafify_of

Modified src/topology/sheaves/sheaf.lean

added def Top.sheaf_condition.cover.of_open_embedding

added def Top.sheaf_condition.diagram.iso_of_open_embedding

added def Top.sheaf_condition.fork.iso_of_open_embedding

added def Top.sheaf_condition.pi_inters.iso_of_open_embedding

added def Top.sheaf_condition.pi_opens.iso_of_open_embedding

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.germ_exist