The category of schemes #
A scheme is a locally ringed space such that every point is contained in some open set
where there is an isomorphism of presheaves between the restriction to that open set,
and the structure sheaf of Spec R
, for some commutative ring R
.
A morphism of schemes is just a morphism of the underlying locally ringed spaces.
We define Scheme
as an X : LocallyRingedSpace
,
along with a proof that every point has an open neighbourhood U
so that the restriction of X
to U
is isomorphic,
as a locally ringed space, to Spec.toLocallyRingedSpace.obj (op R)
for some R : CommRingCat
.
- local_affine (x : ↑self.toTopCat) : ∃ (U : TopologicalSpace.OpenNhds x) (R : CommRingCat), Nonempty (self.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (Opposite.op R))
Equations
- AlgebraicGeometry.Scheme.instCoeSortType = { coe := fun (X : AlgebraicGeometry.Scheme) => ↥X }
Pretty printer for coercing schemes to types.
Equations
- One or more equations did not get rendered due to their size.
A morphism between schemes is a morphism between the underlying locally ringed spaces.
Cast a morphism of schemes into morphisms of local ringed spaces.
See Note [custom simps projection]
Equations
Schemes are a full subcategory of locally ringed spaces.
Equations
- One or more equations did not get rendered due to their size.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
f ⁻¹ᵁ U
is notation for (Opens.map f.base).obj U
,
the preimage of an open set U
under f
.
Equations
- One or more equations did not get rendered due to their size.
Γ(X, U)
is notation for X.presheaf.obj (op U)
.
Equations
- One or more equations did not get rendered due to their size.
Pretty printer defined by notation3
command.
Equations
- One or more equations did not get rendered due to their size.
The structure sheaf of a scheme.
Given a morphism of schemes f : X ⟶ Y
, and open U ⊆ Y
,
this is the induced map Γ(Y, U) ⟶ Γ(X, f ⁻¹ᵁ U)
.
Equations
- f.app U = f.c.app (Opposite.op U)
Given a morphism of schemes f : X ⟶ Y
, and open sets U ⊆ Y
, V ⊆ f ⁻¹' U
,
this is the induced map Γ(Y, U) ⟶ Γ(X, V)
.
Equations
- f.appLE U V e = CategoryTheory.CategoryStruct.comp (f.app U) (X.presheaf.map (CategoryTheory.homOfLE e).op)
A morphism of schemes f : X ⟶ Y
induces a local ring homomorphism from
Y.presheaf.stalk (f x)
to X.presheaf.stalk x
for any x : X
.
Equations
The forgetful functor from Scheme
to LocallyRingedSpace
.
Equations
- One or more equations did not get rendered due to their size.
The forget functor Scheme ⥤ LocallyRingedSpace
is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.
Alias of AlgebraicGeometry.Scheme.homeoOfIso
.
An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.
An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.
Equations
Equations
- AlgebraicGeometry.Scheme.hasCoeToTopCat = { coe := fun (X : AlgebraicGeometry.Scheme) => ↑X.toPresheafedSpace }
forgetful functor to TopCat
is the same as coercion
Equations
Alias of AlgebraicGeometry.Scheme.inv_appTop
.
Copies a morphism with a different underlying map
Equations
- f.copyBase g h = { base := TopCat.ofHom { toFun := g, continuous_toFun := ⋯ }, c := CategoryTheory.CategoryStruct.comp f.c (TopCat.Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ }
The spectrum of a commutative ring, as a scheme.
Equations
- AlgebraicGeometry.Spec R = { toLocallyRingedSpace := AlgebraicGeometry.Spec.locallyRingedSpaceObj R, local_affine := ⋯ }
The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.
Equations
- AlgebraicGeometry.Spec.map f = { toLRSHom' := AlgebraicGeometry.Spec.locallyRingedSpaceMap f }
The spectrum, as a contravariant functor from commutative rings to schemes.
Equations
- One or more equations did not get rendered due to their size.
The empty scheme.
Equations
- One or more equations did not get rendered due to their size.
Equations
- AlgebraicGeometry.Scheme.instEmptyCollection = { emptyCollection := AlgebraicGeometry.Scheme.empty }
Equations
- AlgebraicGeometry.Scheme.instInhabited = { default := ∅ }
The global sections, notated Gamma.
The counit (SpecΓIdentity.inv.op
) of the adjunction Γ ⊣ Spec
as an isomorphism.
This is almost never needed in practical use cases. Use ΓSpecIso
instead.
Equations
- One or more equations did not get rendered due to their size.
The global sections of Spec R
is isomorphic to R
.
The subset of the underlying space where the given section does not vanish.
Equations
- X.basicOpen f = X.toRingedSpace.basicOpen f
A variant of mem_basicOpen
for bundled x : U
.
A variant of mem_basicOpen
without the x ∈ U
assumption.
The zero locus of a set of sections s
over an open set U
is the closed set consisting of
the complement of U
and of all points of U
, where all elements of f
vanish.
Equations
- X.zeroLocus s = X.toRingedSpace.zeroLocus s
If x = y
, the stalk maps are isomorphic.