mathlib documentation

algebraic_geometry.AffineScheme

Affine schemes #

We define the category of AffineSchemes 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 map X ⟶ Spec Γ(X) is an isomorphism.
algebraic_geometry.Scheme.iso_Spec: The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.
algebraic_geometry.AffineScheme.equiv_CommRing: The equivalence of categories AffineScheme ≌ CommRingᵒᵖ given by AffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme and AffineScheme.Γ : 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 immersion Spec 𝒪ₓ(U) ⟶ X for an affine U.

def algebraic_geometry.AffineScheme :

set algebraic_geometry.Scheme

The category of affine schemes

Equations

algebraic_geometry.AffineScheme = algebraic_geometry.Scheme.Spec.ess_image

Instances for ↥algebraic_geometry.AffineScheme

@[class]

structure algebraic_geometry.is_affine (X : algebraic_geometry.Scheme) :

Prop

affine : category_theory.is_iso (algebraic_geometry.Γ_Spec.adjunction.unit.app X)

A Scheme is affine if the canonical map X ⟶ Spec Γ(X) is an isomorphism.

Instances of this typeclass

noncomputable def algebraic_geometry.Scheme.iso_Spec (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

X ≅ algebraic_geometry.Scheme.Spec.obj (opposite.op (algebraic_geometry.Scheme.Γ.obj (opposite.op X)))

The canonical isomorphism X ≅ Spec Γ(X) for an affine scheme.

Equations

X.iso_Spec = category_theory.as_iso (algebraic_geometry.Γ_Spec.adjunction.unit.app X)

theorem algebraic_geometry.mem_AffineScheme (X : algebraic_geometry.Scheme) :

X ∈ algebraic_geometry.AffineScheme ↔ algebraic_geometry.is_affine X

@[protected, instance]

def algebraic_geometry.is_affine_AffineScheme (X : ↥algebraic_geometry.AffineScheme) :

algebraic_geometry.is_affine ↑X

@[protected, instance]

def algebraic_geometry.Spec_is_affine (R : CommRing ᵒᵖ) :

algebraic_geometry.is_affine (algebraic_geometry.Scheme.Spec.obj R)

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] :

algebraic_geometry.is_affine X

@[protected, instance]

def algebraic_geometry.AffineScheme.Spec.ess_surj :

category_theory.ess_surj algebraic_geometry.AffineScheme.Spec

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.Spec.full :

category_theory.full algebraic_geometry.AffineScheme.Spec

@[protected, instance]

def algebraic_geometry.AffineScheme.Spec.faithful :

category_theory.faithful algebraic_geometry.AffineScheme.Spec

noncomputable def algebraic_geometry.AffineScheme.Spec :

CommRing ᵒᵖ ⥤ ↥algebraic_geometry.AffineScheme

The Spec functor into the category of affine schemes.

Equations

algebraic_geometry.AffineScheme.Spec = algebraic_geometry.Scheme.Spec.to_ess_image

Instances for algebraic_geometry.AffineScheme.Spec

@[protected, instance]

def algebraic_geometry.AffineScheme.forget_to_Scheme.faithful :

category_theory.faithful algebraic_geometry.AffineScheme.forget_to_Scheme

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.forget_to_Scheme.full :

category_theory.full algebraic_geometry.AffineScheme.forget_to_Scheme

@[simp]

theorem algebraic_geometry.AffineScheme.forget_to_Scheme_map (x y : category_theory.induced_category algebraic_geometry.Scheme subtype.val) (f : x ⟶ y) :

algebraic_geometry.AffineScheme.forget_to_Scheme.map f = f

noncomputable def algebraic_geometry.AffineScheme.forget_to_Scheme :

↥algebraic_geometry.AffineScheme ⥤ algebraic_geometry.Scheme

The forgetful functor AffineScheme ⥤ Scheme.

Equations

algebraic_geometry.AffineScheme.forget_to_Scheme = algebraic_geometry.Scheme.Spec.ess_image_inclusion

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}) :

algebraic_geometry.AffineScheme.forget_to_Scheme.obj self = ↑self

noncomputable def algebraic_geometry.AffineScheme.Γ :

(↥algebraic_geometry.AffineScheme)ᵒᵖ ⥤ CommRing

The global section functor of an affine scheme.

Equations

algebraic_geometry.AffineScheme.Γ = algebraic_geometry.AffineScheme.forget_to_Scheme.op ⋙ algebraic_geometry.Scheme.Γ

Instances for algebraic_geometry.AffineScheme.Γ

algebraic_geometry.AffineScheme.Γ_is_equiv

noncomputable def algebraic_geometry.AffineScheme.equiv_CommRing :

↥algebraic_geometry.AffineScheme ≌ CommRing ᵒᵖ

The category of affine schemes is equivalent to the category of commutative rings.

Equations

algebraic_geometry.AffineScheme.equiv_CommRing = category_theory.equiv_ess_image_of_reflective.symm

@[protected, instance]

noncomputable def algebraic_geometry.AffineScheme.Γ_is_equiv :

category_theory.is_equivalence algebraic_geometry.AffineScheme.Γ

Equations

algebraic_geometry.AffineScheme.Γ_is_equiv = algebraic_geometry.AffineScheme.Γ.right_op.op.is_equivalence_trans (category_theory.op_op_equivalence CommRing).functor

@[protected, instance]

def algebraic_geometry.AffineScheme.category_theory.limits.has_colimits :

category_theory.limits.has_colimits ↥algebraic_geometry.AffineScheme

@[protected, instance]

def algebraic_geometry.AffineScheme.category_theory.limits.has_limits :

category_theory.limits.has_limits ↥algebraic_geometry.AffineScheme

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

algebraic_geometry.is_affine_open U = algebraic_geometry.is_affine (X.restrict _)

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] :

algebraic_geometry.is_affine_open ⟨set.range ⇑(f.val.base), _⟩

theorem algebraic_geometry.top_is_affine_open (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

algebraic_geometry.is_affine_open ⊤

@[protected, instance]

def algebraic_geometry.Scheme.affine_basis_cover_is_affine (X : algebraic_geometry.Scheme) (i : X.affine_basis_cover.J) :

algebraic_geometry.is_affine (X.affine_basis_cover.obj i)

theorem algebraic_geometry.is_basis_affine_open (X : algebraic_geometry.Scheme) :

topological_space.opens.is_basis {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) | algebraic_geometry.is_affine_open U}

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) :

algebraic_geometry.Scheme.Spec.obj (opposite.op (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) ⟶ X

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]

def algebraic_geometry.is_affine_open.is_open_immersion_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.is_open_immersion hU.from_Spec

theorem algebraic_geometry.is_affine_open.from_Spec_range {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

set.range ⇑(hU.from_Spec.val.base) = ↑U

theorem algebraic_geometry.is_affine_open.from_Spec_image_top {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

_.functor.obj ⊤ = U

theorem algebraic_geometry.is_affine_open.is_compact {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

is_compact ↑U

@[protected, instance]

def algebraic_geometry.Scheme.quasi_compact_of_affine (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

compact_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

theorem algebraic_geometry.is_affine_open.from_Spec_base_preimage {X : algebraic_geometry.Scheme} {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (hU : algebraic_geometry.is_affine_open U) :

(topological_space.opens.map hU.from_Spec.val.base).obj U = ⊤

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))) :

algebraic_geometry.is_affine_open (X.basic_open f)

theorem algebraic_geometry.Scheme.map_prime_spectrum_basic_open_of_affine (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] (f : ↥(algebraic_geometry.Scheme.Γ.obj (opposite.op X))) :

(topological_space.opens.map X.iso_Spec.hom.val.base).obj (prime_spectrum.basic_open f) = X.basic_open f

theorem algebraic_geometry.is_basis_basic_open (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] :

topological_space.opens.is_basis (set.range X.basic_open)

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) :

prime_spectrum ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op 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.from_Spec_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) :

⇑(hU.from_Spec.val.base) (hU.prime_ideal_of x) = x.val

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 _)] :