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 (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)
Instances
The canonical isomorphism X ≅ Spec Γ(X)
for an affine scheme.
Equations
- X.isoSpec = CategoryTheory.asIso (AlgebraicGeometry.ΓSpec.adjunction.unit.app X)
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
- ⋯ = ⋯
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
- AlgebraicGeometry.IsAffineOpen U = AlgebraicGeometry.IsAffine (X.restrict ⋯)
Instances For
The set of affine opens as a subset of opens X
.
Equations
- X.affineOpens = {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace | AlgebraicGeometry.IsAffineOpen U}
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The open immersion Spec Γ(X, U) ⟶ X
for an affine U
.
Equations
- One or more equations did not get rendered due to their size.
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
- ⋯ = ⋯
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 (X.restrict ⋯).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
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][RisingSea].
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.ιOpens_basicOpen_preimage
.