Documentation

TauCeti.AlgebraicGeometry.Scheme.SpecOver

Morphisms of affine schemes over an affine base #

For commutative R-algebras A and B, the scheme Spec B is a scheme over Spec R through Mathlib's AlgebraicGeometry.specOverSpec. This file identifies the morphisms Spec B ⟶ Spec A over Spec R, in the vocabulary Scheme.Hom.IsOver of schemes over a base, with the R-algebra homomorphisms A →ₐ[R] B. It is the OverClass form of Mathlib's AlgebraicGeometry.Spec.homEquivAlgHom, whose compatibility condition is the explicit equation of structure morphisms.

In particular, for a field K, the K-points of an affine K-scheme Spec A in the functor-of-points sense, the morphisms Spec K ⟶ Spec A over Spec K, are the K-algebra homomorphisms A →ₐ[K] K. A bare scheme morphism Spec K ⟶ Spec A is a ring homomorphism A →+* K and need not be K-linear.

A morphism Spec B ⟶ X over Spec R whose image lies in an affine open Spec A ⟶ X over Spec R factors through it by an R-algebra homomorphism A →ₐ[R] B.

Main declarations #

source
noncomputable def TauCeti.AlgebraicGeometry.specOverHomEquivAlgHom {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] :
{ f : AlgebraicGeometry.Spec ↧B ⟶ AlgebraicGeometry.Spec ↧A // AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R) } ≃ (A →ₐ[R] B)

Morphisms Spec B ⟶ Spec A over Spec R are the R-algebra homomorphisms A →ₐ[R] B. This is Mathlib's AlgebraicGeometry.Spec.homEquivAlgHom, with the compatibility with the structure morphisms expressed by Scheme.Hom.IsOver.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.coe_specOverHomEquivAlgHom_symm_apply {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) :
    ↑(specOverHomEquivAlgHom.symm φ) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑φ)

    The inverse of specOverHomEquivAlgHom applies Spec to an algebra homomorphism.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.spec_map_specOverHomEquivAlgHom {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : { f : AlgebraicGeometry.Spec ↧B ⟶ AlgebraicGeometry.Spec ↧A // AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R) }) :
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(specOverHomEquivAlgHom f)) = ↑f

    Applying Spec to the algebra homomorphism of a morphism over Spec R recovers the morphism.

    source
    theorem TauCeti.AlgebraicGeometry.exists_spec_map_comp_eq_of_range_subset {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] (f : AlgebraicGeometry.Spec ↧A ⟶ X) [AlgebraicGeometry.IsOpenImmersion f] [AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧R)] (p : AlgebraicGeometry.Spec ↧B ⟶ X) [AlgebraicGeometry.Scheme.Hom.IsOver p (AlgebraicGeometry.Spec ↧R)] (h : Set.range ⇑p ⊆ Set.range ⇑f) :
    ∃ (φ : A →ₐ[R] B), CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom φ.toRingHom)) f = p

    A morphism p : Spec B ⟶ X over Spec R whose image lies in the image of an open immersion f : Spec A ⟶ X over Spec R factors through f by an R-algebra homomorphism A →ₐ[R] B.