Commit 2023-06-14 15:16 1a0f4dea

View on Github →

feat: port AlgebraicGeometry.Scheme (#5040)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/Scheme.lean

added def AlgebraicGeometry.Scheme.Hom

added def AlgebraicGeometry.Scheme.Spec

added theorem AlgebraicGeometry.Scheme.app_eq

added def AlgebraicGeometry.Scheme.basicOpen

added theorem AlgebraicGeometry.Scheme.basicOpen_le

added theorem AlgebraicGeometry.Scheme.basicOpen_mul

added theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit

added theorem AlgebraicGeometry.Scheme.basicOpen_res

added theorem AlgebraicGeometry.Scheme.basicOpen_res_eq

added theorem AlgebraicGeometry.Scheme.basicOpen_zero

added theorem AlgebraicGeometry.Scheme.comp_coeBase

added theorem AlgebraicGeometry.Scheme.comp_val

added theorem AlgebraicGeometry.Scheme.comp_val_base

added theorem AlgebraicGeometry.Scheme.comp_val_c_app

added theorem AlgebraicGeometry.Scheme.congr_app

added def AlgebraicGeometry.Scheme.empty.{u}

added def AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace

added theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_preimage

added def AlgebraicGeometry.Scheme.forgetToTop

added theorem AlgebraicGeometry.Scheme.id_app

added theorem AlgebraicGeometry.Scheme.id_val_base

added theorem AlgebraicGeometry.Scheme.inv_val_c_app

added theorem AlgebraicGeometry.Scheme.mem_basicOpen

added theorem AlgebraicGeometry.Scheme.mem_basicOpen_top

added theorem AlgebraicGeometry.Scheme.preimage_basicOpen

added def AlgebraicGeometry.Scheme.specMap

added theorem AlgebraicGeometry.Scheme.specMap_comp

added theorem AlgebraicGeometry.Scheme.specMap_id

added def AlgebraicGeometry.Scheme.specObj

added theorem AlgebraicGeometry.Scheme.specObj_toLocallyRingedSpace

added def AlgebraicGeometry.Scheme.Γ

added theorem AlgebraicGeometry.Scheme.Γ_def

added theorem AlgebraicGeometry.Scheme.Γ_map

added theorem AlgebraicGeometry.Scheme.Γ_map_op

added theorem AlgebraicGeometry.Scheme.Γ_obj

added theorem AlgebraicGeometry.Scheme.Γ_obj_op

added structure AlgebraicGeometry.Scheme

added theorem AlgebraicGeometry.basicOpen_eq_of_affine'

added theorem AlgebraicGeometry.basicOpen_eq_of_affine