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 #
AlgebraicGeometry.AffineScheme
: The category of affine schemes.AlgebraicGeometry.IsAffine
: A scheme is affine if the canonical mapX ⟶ Spec Γ(X)
is an isomorphism.AlgebraicGeometry.Scheme.isoSpec
: The canonical isomorphismX ≅ Spec Γ(X)
for an affine scheme.AlgebraicGeometry.AffineScheme.equivCommRingCat
: The equivalence of categoriesAffineScheme ≌ CommRingᵒᵖ
given byAffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme
andAffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRingCat
.AlgebraicGeometry.IsAffineOpen
: An open subset of a scheme is affine if the open subscheme is affine.AlgebraicGeometry.IsAffineOpen.fromSpec
: The immersionSpec 𝒪ₓ(U) ⟶ X
for an affineU
.
The category of affine schemes
Equations
- AlgebraicGeometry.AffineScheme = AlgebraicGeometry.Scheme.Spec.EssImageSubcategory
Instances For
A Scheme is affine if the canonical map X ⟶ Spec Γ(X)
is an isomorphism.
- affine : CategoryTheory.IsIso X.toSpecΓ
Instances
Equations
- ⋯ = ⋯
The canonical isomorphism X ≅ Spec Γ(X)
for an affine scheme.
Equations
- X.isoSpec = CategoryTheory.asIso X.toSpecΓ
Instances For
Construct an affine scheme from a scheme and the information that it is affine.
Also see AffineScheme.of
for a typeclass version.
Equations
- AlgebraicGeometry.AffineScheme.mk X x = { obj := X, property := ⋯ }
Instances For
Construct an affine scheme from a scheme. Also see AffineScheme.mk
for a non-typeclass
version.
Equations
Instances For
Type check a morphism of schemes as a morphism in AffineScheme
.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If f : X ⟶ Y
is a morphism between affine schemes, the corresponding arrow is isomorphic
to the arrow of the morphism on prime spectra induced by the map on global sections.
Equations
- AlgebraicGeometry.arrowIsoSpecΓOfIsAffine f = CategoryTheory.Arrow.isoMk X.isoSpec Y.isoSpec ⋯
Instances For
If f : A ⟶ B
is a ring homomorphism, the corresponding arrow is isomorphic
to the arrow of the morphism induced on global sections by the map on prime spectra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Spec
functor into the category of affine schemes.
Equations
Instances For
The forgetful functor AffineScheme ⥤ Scheme
.
Equations
- AlgebraicGeometry.AffineScheme.forgetToScheme = AlgebraicGeometry.Scheme.Spec.essImageInclusion
Instances For
The global section functor of an affine scheme.
Equations
Instances For
The category of affine schemes is equivalent to the category of commutative rings.
Equations
- AlgebraicGeometry.AffineScheme.equivCommRingCat = CategoryTheory.equivEssImageOfReflective.symm
Instances For
Equations
Equations
- AlgebraicGeometry.AffineScheme.Γ_preservesLimits = inferInstance
Equations
- One or more equations did not get rendered due to their size.
An open subset of a scheme is affine if the open subscheme is affine.
Equations
Instances For
The set of affine opens as a subset of opens X
.
Equations
- X.affineOpens = {U : X.Opens | AlgebraicGeometry.IsAffineOpen U}
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The open immersion Spec Γ(X, U) ⟶ X
for an affine U
.
Equations
- hU.fromSpec = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)) (CategoryTheory.CategoryStruct.comp (↑U).isoSpec.inv U.ι)
Instances For
Equations
- ⋯ = ⋯
The affine open sets of an open subscheme corresponds to the affine open sets containing in the image.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The affine open sets of an open subscheme corresponds to the affine open sets containing in the subset.
Equations
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Given an affine open U and some f : U
,
this is the canonical map Γ(𝒪ₓ, D(f)) ⟶ Γ(Spec 𝒪ₓ(U), D(f))
This is an isomorphism, as witnessed by an IsIso
instance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The prime ideal of 𝒪ₓ(U)
corresponding to a point x : U
.
Equations
- hU.primeIdealOf x = (CategoryTheory.CategoryStruct.comp (↑U).isoSpec.hom (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))).val.base x
Instances For
The basic open set of a section f
on an affine open as an X.affineOpens
.
Equations
- X.affineBasicOpen f = ⟨X.basicOpen f, ⋯⟩
Instances For
In an affine open set U
, a family of basic open covers U
iff the sections span Γ(X, U)
.
See iSup_basicOpen_of_span_eq_top
for the inverse direction without the affine-ness assumption.
Given a spanning set of Γ(X, U)
, the corresponding basic open sets cover U
.
See IsAffineOpen.basicOpen_union_eq_self_iff
for the inverse direction for affine open sets.
Let P
be a predicate on the affine open sets of X
satisfying
- If
P
holds onU
, thenP
holds on the basic open set of every section onU
. - If
P
holds for a family of basic open sets coveringU
, thenP
holds forU
. - There exists an affine open cover of
X
each satisfyingP
.
Then P
holds for every affine open of X
.
This is also known as the Affine communication lemma in The rising sea.
On a locally ringed space X
, the preimage of the zero locus of the prime spectrum
of Γ(X, ⊤)
under toΓSpecFun
agrees with the associated zero locus on X
.
If X
is affine, the image of the zero locus of global sections of X
under toΓSpecFun
is the zero locus in terms of the prime spectrum of Γ(X, ⊤)
.
If X
is an affine scheme, every closed set of X
is the zero locus
of a set of global sections.
If X ⟶ Spec A
is a morphism of schemes, then Spec
of A ⧸ specTargetImage f
is the scheme-theoretic image of f
. For this quotient as an object of CommRingCat
see
specTargetImage
below.
Equations
- AlgebraicGeometry.specTargetImageIdeal f = RingHom.ker ((AlgebraicGeometry.ΓSpec.adjunction.homEquiv X (Opposite.op A)).symm f).unop
Instances For
If X ⟶ Spec A
is a morphism of schemes, then Spec
of specTargetImage f
is the
scheme-theoretic image of f
and f
factors as
specTargetImageFactorization f ≫ Spec.map (specTargetImageRingHom f)
(see specTargetImageFactorization_comp
).
Equations
Instances For
If f : X ⟶ Spec A
is a morphism of schemes, then f
factors via
the inclusion of Spec (specTargetImage f)
into X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f : X ⟶ Spec A
is a morphism of schemes, the induced morphism on spectra of
specTargetImageRingHom f
is the inclusion of the scheme-theoretic image of f
into Spec A
.
Equations
Instances For
The scheme-theoretic image of a morphism f : X ⟶ Y
with affine target.
f
factors as affineTargetImageFactorization f ≫ affineTargetImageInclusion f
(see affineTargetImageFactorization_comp
).
Equations
Instances For
Equations
- ⋯ = ⋯
The inclusion of the scheme-theoretic image of a morphism with affine target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The induced morphism from X
to the scheme-theoretic image
of a morphism f : X ⟶ Y
with affine target.
Equations
Instances For
Variant of AlgebraicGeometry.localRingHom_comp_stalkIso
for Spec.map
.
Given a morphism of rings f : R ⟶ S
, the stalk map of Spec S ⟶ Spec R
at
a prime of S
is isomorphic to the localized ring homomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of AlgebraicGeometry.isAffine_affineScheme
.
Instances For
Alias of AlgebraicGeometry.isAffine_Spec
.
Instances For
Alias of AlgebraicGeometry.isAffine_of_isIso
.
Alias of AlgebraicGeometry.isAffineOpen_top
.
Alias of AlgebraicGeometry.Scheme.isAffine_affineCover
.
Equations
Instances For
Alias of AlgebraicGeometry.Scheme.isAffine_affineBasisCover
.
Equations
Instances For
Alias of AlgebraicGeometry.IsAffineOpen.image_of_isOpenImmersion
.
Alias of AlgebraicGeometry.Scheme.compactSpace_of_isAffine
.
Equations
Instances For
Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self
.
Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen'
.
Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen
.
Alias of AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen
.
Alias of AlgebraicGeometry.IsAffineOpen.basicOpen
.
Alias of AlgebraicGeometry.IsAffineOpen.ι_basicOpen_preimage
.