The universal property of relative Spec #
Let A be a quasi-coherent commutative algebra on a scheme X and let q : T ⟶ X be an
arbitrary scheme over X. Morphisms T ⟶ Spec_X A over X correspond to morphisms of
𝒪_X-algebras A ⟶ q_* 𝒪_T (CommMon.relativeSpecHomEquiv). This is the functor-of-points
description of relative Spec; no affineness, quasi-compactness or separation hypothesis on q is
needed.
A morphism t : T ⟶ Spec_X A over X pulls back regular functions, which gives the algebra map
A ≅ p_* 𝒪_{Spec_X A} ⟶ q_* 𝒪_T. Conversely, an algebra map φ : A ⟶ q_* 𝒪_T induces, over
each affine open U of X, a ring map Γ(A.X, U) ⟶ Γ(T, q⁻¹ U) and hence a morphism
q⁻¹ U ⟶ Spec Γ(A.X, U) into the chart of Spec_X A over U. These charts are compatible with
restriction and glue to CommMon.relativeSpecLift φ, along the cover of T by the inverse images
of the affine opens of X. Both constructions are natural in T and in A.
Composing with the adjunction between pullback and pushforward of algebras gives the universal
property in pullback form: morphisms T ⟶ Spec_X A over X correspond to morphisms of
𝒪_T-algebras q^* A ⟶ 𝒪_T (TauCeti.AlgebraicGeometry.relativeSpecPullbackHomEquiv).
Main declarations #
CategoryTheory.CommMon.relativeSpecLift: the morphismT ⟶ Spec_X Ainduced by an algebra mapA ⟶ q_* 𝒪_T, characterized on charts byCommMon.ι_relativeSpecLift;CategoryTheory.CommMon.relativeSpecHomEquiv: the bijection between morphisms overXand algebra maps;CategoryTheory.CommMon.relativeSpecLift_comp_pushforwardStructureAlgebraMap,CategoryTheory.CommMon.relativeSpecLift_compandCategoryTheory.CommMon.relativeSpecHomEquiv_comp_relativeSpecMap: naturality in the test scheme and in the algebra;TauCeti.AlgebraicGeometry.relativeSpecHomIso X: the bijection as a natural isomorphism of functors of quasi-coherent algebras and schemes overX(whose target uses the function-algebra functorTauCeti.AlgebraicGeometry.overFunctions X), with componentsCommMon.relativeSpecHomEquiv;TauCeti.AlgebraicGeometry.relativeSpecPullbackHomEquiv: the bijection between morphisms overXand algebra mapsq^* A ⟶ 𝒪_T, natural in the algebra.
References #
- The Stacks Project, Tag 01LQ (relative spectrum as a functor).
- The gluing of the charts follows Mathlib's
AlgebraicGeometry.Scheme.Hom.toNormalization, which glues maps into the relative normalization along the same pulled-back directed affine cover.
The morphism T ⟶ Spec_X A over X induced by a morphism of 𝒪_X-algebras
φ : A ⟶ q_* 𝒪_T. Over an affine open U of X, it maps q⁻¹ U to the chart Spec Γ(A.X, U)
by the spectrum of the ring map Γ(A.X, U) ⟶ Γ(T, q⁻¹ U) induced by φ
(CommMon.ι_relativeSpecLift).
Instances For
The lift is a morphism over X.
The lift is a morphism over X.
On the inverse image of an affine open U of X, the lift is the spectrum of the ring map
Γ(A.X, U) ⟶ Γ(T, q⁻¹ U) induced by φ, followed by the chart of Spec_X A over U.
On the inverse image of an affine open U of X, the lift is the spectrum of the ring map
Γ(A.X, U) ⟶ Γ(T, q⁻¹ U) induced by φ, followed by the chart of Spec_X A over U.
The lift is natural in the test scheme: precomposing it with g : T' ⟶ T over X
corresponds to composing the algebra map with pullback of regular functions along g.
On sections over the inverse image of an affine open U of X, the lift sends a function
on Spec_X A, read as a section of A over U through its chart, to its image under φ.
The algebra map recovered from the lift of φ is φ: pulling back regular functions along
CommMon.relativeSpecLift φ and identifying A with the functions on Spec_X A gives φ.
A morphism over X is the lift of its own algebra map.
The universal property of relative Spec. Morphisms T ⟶ Spec_X A over X correspond
to morphisms of 𝒪_X-algebras A ⟶ q_* 𝒪_T. A morphism t gives pullback of regular functions
along t, after identifying A with the functions on Spec_X A; conversely an algebra map
gives CommMon.relativeSpecLift. No hypothesis on q is needed.
Instances For
The algebra map of a morphism over X is pullback of regular functions along it.
The morphism over X of an algebra map is its lift.
The algebra map of the identity of Spec_X A is the inverse identification of A with the
functions on Spec_X A.
The lift is natural in the algebra: precomposing the algebra map with f : B ⟶ A
corresponds to composing with the relative-spectrum map of f.
The bijection CommMon.relativeSpecHomEquiv is natural in the algebra: composing with the
relative-spectrum map of f : B ⟶ A corresponds to precomposing the algebra map with f.
The functor-of-points universal property of relative Spec, natural in the algebra A
and in the scheme T over X: morphisms T ⟶ Spec_X A over X correspond to morphisms of
𝒪_X-algebras A ⟶ q_* 𝒪_T. Its components are CommMon.relativeSpecHomEquiv.
Instances For
The components of relativeSpecHomIso are CommMon.relativeSpecHomEquiv.
The inverse components of relativeSpecHomIso are given by CommMon.relativeSpecLift.
The universal property of relative Spec, in pullback form. For a quasicoherent algebra
A on X and a scheme q : T ⟶ X, morphisms T ⟶ Spec_X A over X correspond to morphisms
of 𝒪_T-algebras q^* A ⟶ 𝒪_T. It is CommMon.relativeSpecHomEquiv followed by the
adjunction between pullback and pushforward of algebras,
QuasicoherentAlgebra.pullbackHomEquiv.
Instances For
The algebra map q^* A ⟶ 𝒪_T of a morphism over X is the transpose of its pullback of
regular functions A ⟶ q_* 𝒪_T.
The morphism over X of an algebra map q^* A ⟶ 𝒪_T is the lift of its transpose
A ⟶ q_* 𝒪_T.
The pullback form of the universal property is natural in the algebra: precomposing an
algebra map q^* A ⟶ 𝒪_T with the pullback of a : B ⟶ A corresponds to composing with the
relative-spectrum map of a.