Affine schemes #
We define the category of AffineScheme
s as the essential image of Spec
.
We also define predicates about affine schemes and affine open sets.
Main definitions #
algebraic_geometry.AffineScheme
: The category of affine schemes.algebraic_geometry.is_affine
: A scheme is affine if the canonical mapX ⟶ Spec Γ(X)
is an isomorphism.algebraic_geometry.Scheme.iso_Spec
: The canonical isomorphismX ≅ Spec Γ(X)
for an affine scheme.algebraic_geometry.AffineScheme.equiv_CommRing
: The equivalence of categoriesAffineScheme ≌ CommRingᵒᵖ
given byAffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme
andAffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRing
.algebraic_geometry.is_affine_open
: An open subset of a scheme is affine if the open subscheme is affine.algebraic_geometry.is_affine_open.from_Spec
: The immersionSpec 𝒪ₓ(U) ⟶ X
for an affineU
.
The category of affine schemes
Instances for ↥algebraic_geometry.AffineScheme
@[class]
A Scheme is affine if the canonical map X ⟶ Spec Γ(X)
is an isomorphism.
noncomputable
def
algebraic_geometry.Scheme.iso_Spec
(X : algebraic_geometry.Scheme)
[algebraic_geometry.is_affine X] :
The canonical isomorphism X ≅ Spec Γ(X)
for an affine scheme.
Equations
@[protected, instance]
@[protected, instance]
theorem
algebraic_geometry.is_affine_of_iso
{X Y : algebraic_geometry.Scheme}
(f : X ⟶ Y)
[category_theory.is_iso f]
[h : algebraic_geometry.is_affine Y] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
The Spec
functor into the category of affine schemes.
Instances for algebraic_geometry.AffineScheme.Spec
@[protected, instance]
@[simp]
The forgetful functor AffineScheme ⥤ Scheme
.
Equations
Instances for algebraic_geometry.AffineScheme.forget_to_Scheme
@[simp]
theorem
algebraic_geometry.AffineScheme.forget_to_Scheme_obj
(self : {X // (λ (x : algebraic_geometry.Scheme), x ∈ algebraic_geometry.Scheme.Spec.ess_image) X}) :
The global section functor of an affine scheme.
Equations
Instances for algebraic_geometry.AffineScheme.Γ
The category of affine schemes is equivalent to the category of commutative rings.
@[protected, instance]
def
algebraic_geometry.is_affine_open
{X : algebraic_geometry.Scheme}
(U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :
Prop
An open subset of a scheme is affine if the open subscheme is affine.
Equations
theorem
algebraic_geometry.range_is_affine_open_of_open_immersion
{X Y : algebraic_geometry.Scheme}
[algebraic_geometry.is_affine X]
(f : X ⟶ Y)
[H : algebraic_geometry.is_open_immersion f] :
@[protected, instance]
noncomputable
def
algebraic_geometry.is_affine_open.from_Spec
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U) :
The open immersion Spec 𝒪ₓ(U) ⟶ X
for an affine U
.
Equations
- hU.from_Spec = algebraic_geometry.Scheme.Spec.map (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom algebraic_geometry.is_affine_open.from_Spec._proof_4).op).op ≫ (X.restrict algebraic_geometry.is_affine_open.from_Spec._proof_5).iso_Spec.inv ≫ X.of_restrict algebraic_geometry.is_affine_open.from_Spec._proof_6
@[protected, instance]
@[protected, instance]
theorem
algebraic_geometry.Scheme.Spec_map_presheaf_map_eq_to_hom
{X : algebraic_geometry.Scheme}
{U V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(h : U = V)
(W : (topological_space.opens ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op V)))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))ᵒᵖ) :
theorem
algebraic_geometry.is_affine_open.Spec_Γ_identity_hom_app_from_Spec
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U) :
algebraic_geometry.Spec_Γ_identity.hom.app (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)) ≫ hU.from_Spec.val.c.app (opposite.op U) = (algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op
theorem
algebraic_geometry.is_affine_open.from_Spec_app_eq
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U) :
hU.from_Spec.val.c.app (opposite.op U) = algebraic_geometry.Spec_Γ_identity.inv.app (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)) ≫ (algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op
theorem
algebraic_geometry.is_affine_open.from_Spec_app_eq_apply
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U)
(x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
⇑(hU.from_Spec.val.c.app (opposite.op U)) x = ⇑((algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U)))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op) (⇑(algebraic_geometry.Spec_Γ_identity.inv.app (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) x)
theorem
algebraic_geometry.is_affine_open.basic_open_is_affine
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U)
(f : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :
noncomputable
def
algebraic_geometry.is_affine_open.prime_ideal_of
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U)
(x : ↥U) :
The prime ideal of 𝒪ₓ(U)
corresponding to a point x : U
.
Equations
- hU.prime_ideal_of x = ⇑((algebraic_geometry.Scheme.Spec.map (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom algebraic_geometry.is_affine_open.prime_ideal_of._proof_4).op).op).val.base) (⇑((X.restrict algebraic_geometry.is_affine_open.prime_ideal_of._proof_5).iso_Spec.hom.val.base) x)
theorem
algebraic_geometry.is_affine_open.is_localization_stalk_aux
{X : algebraic_geometry.Scheme}
(U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier))
[algebraic_geometry.is_affine (X.restrict _)] :
(category_theory.inv (algebraic_geometry.Γ_Spec.adjunction.unit.app (X.restrict _))).val.c.app (opposite.op ((topological_space.opens.map U.inclusion).obj U)) = X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op ≫ algebraic_geometry.to_Spec_Γ (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (_.functor.obj ⊤))) ≫ (algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op (_.functor.obj ⊤))))).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.map (category_theory.eq_to_hom _).op
theorem
algebraic_geometry.is_affine_open.is_localization_stalk
{X : algebraic_geometry.Scheme}
{U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)}
(hU : algebraic_geometry.is_affine_open U)
(x : ↥U) :