Affine schemes: the spectrum, fixed points, and actions on global sections

For an affine scheme X, Mathlib's AlgebraicGeometry.Scheme.isoSpec is the isomorphism X ≅ Spec Γ(X, ⊤). This file computes the map of global sections of its inverse: it is the inverse of Mathlib's AlgebraicGeometry.Scheme.ΓSpecIso. It is the scheme-level companion of Mathlib's AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop for an affine open.

Through this isomorphism, the scheme-theoretic fixed locus of an endomorphism f of X is the closed subscheme cut out by the elements f^*(a) - a of Γ(X, ⊤). Hence these elements generate the unit ideal exactly when f fixes no point of X with values in a nonempty scheme. This is the form in which a free action of a finite group on an affine scheme enters the theory of invariant quotients (TauCeti.AffineInvariantQuotient.etale_projection), once the group acts on Γ(X, ⊤) by pullback along inverses (AlgebraicGeometry.Scheme.globalSectionsMulSemiringAction).

Morphisms into an affine scheme are determined by their effect on global sections. Hence, over an affine base S, base change along j : T ⟶ S is bijective on morphisms Y ⟶ Y' into an affine Y' whenever it does not change the global sections of Y.

It also shows that for a compatible tower R → B ↪ R_a, localizing B at a gives R_a, so Spec B ⟶ Spec R is an isomorphism over the basic open D(a). The map from R need not be injective. This is the local reason why an affine blowup changes nothing away from its center.

Main definitions

• AlgebraicGeometry.Scheme.globalSectionsMulSemiringAction: a group acting on a scheme X acts on Γ(X, ⊤) by g • a = (σ g⁻¹)^*(a).

Main results

• AlgebraicGeometry.Scheme.isoSpec_inv_appTop: the global sections of X.isoSpec.inv are (Scheme.ΓSpecIso Γ(X, ⊤)).inv.
• AlgebraicGeometry.IsAffineOpen.fromSpec_comp_eq_SpecMap: on an affine open U of X, a morphism X ⟶ Spec R restricted along Spec Γ(X, U) ⟶ X is the spectrum of the ring map R → Γ(X, U) it induces.
• AlgebraicGeometry.IsAffineOpen.isOpenImmersion_SpecMap_presheaf_map: for affine opens V ≤ U, restriction induces an open immersion Spec Γ(X, V) ⟶ Spec Γ(X, U).
• AlgebraicGeometry.IsAffineOpen.exists_SpecMap_comp_fromSpec_eq: a morphism Spec R ⟶ X with image in an affine open U is the spectrum of a ring map Γ(X, U) ⟶ R followed by Spec Γ(X, U) ⟶ X.
• AlgebraicGeometry.Scheme.Opens.ΓSpecIso_inv_comp_toSpecΓ_appLE: on an open U of X, the morphism U ⟶ Spec Γ(X, U) induces restriction of functions on the sections over opens of U.
• AlgebraicGeometry.Scheme.Hom.ΓSpecIso_inv_comp_resLE_isoSpec_appLE: the map Γ(B, V) ⟶ Γ(U, T) induced by the structure morphism of an open subscheme U of Z over an affine open V of B is k.appLE followed by restriction to T.
• AlgebraicGeometry.Scheme.Hom.isBasis_range_affineOpens_le_preimage: for g : S' ⟶ S, the affine opens of S' lying over affine opens of S form a basis.
• AlgebraicGeometry.Scheme.toSpecΓ_apply_asIdeal_eq_smul: for this action, the prime ideal of Γ(X, ⊤) at the point σ g x is the translate by g of the prime ideal at x.
• AlgebraicGeometry.Scheme.Hom.span_range_appTop_sub_eq_top_iff: for an endomorphism f of an affine scheme, the elements f^*(a) - a generate the unit ideal if and only if every point of X fixed by f has values in an empty scheme.
• AlgebraicGeometry.isIso_SpecMap_morphismRestrict_basicOpen_of_injective: for an R-algebra B embedded in a localization of R away from a, the morphism Spec B ⟶ Spec R restricts to an isomorphism over D(a).
• AlgebraicGeometry.IsAffineOpen.mem_basicOpen_iff_notMem_primeIdealOf: on an affine open, a point lies in the basic open of a section iff the section is not in the point's prime ideal.
• AlgebraicGeometry.IsAffineOpen.span_setOf_basicOpen_mem_sieve_eq_top: the basic opens of an affine open U lying in a covering sieve of U are defined by functions generating the unit ideal of Γ(X, U).
• TauCeti.AlgebraicGeometry.overPullback_map_bijective_of_isIso_appTop: over an affine base, base change along j : T ⟶ S is a bijection on morphisms Y ⟶ Y' into an affine Y' when Γ(Y, 𝒪) → Γ(Y ×_S T, 𝒪) is an isomorphism.
• TauCeti.AlgebraicGeometry.Spec.exists_isIso_appTop_eq_comp_of_bijective: when S is recovered from its sections over an open W of Spec S, the sections of a scheme identified with W over Spec R are S, compatibly with the maps from R.
• TauCeti.AlgebraicGeometry.exists_affine_pair_comp_eq: for a morphism f : T' ⟶ T of affine S-schemes, the affine S-scheme Spec (Γ(T', 𝒪) ⊗[Γ(T, 𝒪)] Γ(T', 𝒪)) carries two maps to T' that agree after composing with f and induce the two tensor factor inclusions.

theorem AlgebraicGeometry.Scheme.isoSpec_inv_appTop (X : Scheme) [IsAffine X] : Hom.appTop X.isoSpec.inv = (ΓSpecIso (X.presheaf.obj (Opposite.op ⊤))).inv

The global sections of the inverse of X ≅ Spec Γ(X, ⊤), for an affine scheme X.

theorem AlgebraicGeometry.IsAffineOpen.fromSpec_comp_eq_SpecMap {X : Scheme} {R : CommRingCat} (f : X ⟶ Spec R) {U : X.Opens} (hU : IsAffineOpen U) : CategoryTheory.CategoryStruct.comp hU.fromSpec f = Spec.map (CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso R).inv (Scheme.Hom.appLE f ⊤ U ⋯))

On an affine open U of X, the morphism f : X ⟶ Spec R restricted along Spec Γ(X, U) ⟶ X is the spectrum of the ring map R → Γ(X, U) induced by f.

theorem AlgebraicGeometry.IsAffineOpen.map_fromSpec_apply {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) (p : ↥(Spec (X.presheaf.obj (Opposite.op V)))) : hU.fromSpec ((Spec.map (X.presheaf.map f)) p) = hV.fromSpec p

Pointwise form of AlgebraicGeometry.IsAffineOpen.map_fromSpec: for affine opens V ≤ U, the point of Spec Γ(X, U) induced by restriction from a point p of Spec Γ(X, V) is the same point of X as p.

theorem AlgebraicGeometry.IsAffineOpen.isOpenImmersion_SpecMap_presheaf_map {X : Scheme} {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V) : IsOpenImmersion (Spec.map (X.presheaf.map f))

For affine opens V ≤ U, restriction of sections induces an open immersion Spec Γ(X, V) ⟶ Spec Γ(X, U).

theorem AlgebraicGeometry.IsAffineOpen.exists_SpecMap_comp_fromSpec_eq {X : Scheme} {R : CommRingCat} (f : Spec R ⟶ X) {U : X.Opens} (hU : IsAffineOpen U) (hf : Set.range ⇑f ⊆ ↑U) : ∃ (φ : X.presheaf.obj (Opposite.op U) ⟶ R), CategoryTheory.CategoryStruct.comp (Spec.map φ) hU.fromSpec = f

A morphism f : Spec R ⟶ X whose image lies in an affine open U of X is the spectrum of a ring map Γ(X, U) ⟶ R followed by Spec Γ(X, U) ⟶ X.

theorem AlgebraicGeometry.Scheme.Opens.ΓSpecIso_inv_comp_toSpecΓ_appLE {X : Scheme} (U : X.Opens) (T : (↑U).Opens) : CategoryTheory.CategoryStruct.comp (ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv (Hom.appLE U.toSpecΓ ⊤ T ⋯) = Hom.appLE U.ι U T ⋯

For an open U of X, the map Γ(X, U) ≅ Γ(Spec Γ(X, U), ⊤) ⟶ Γ(U, T) induced on the sections over an open T of U by the canonical morphism U ⟶ Spec Γ(X, U) is restriction of functions from U to T.

theorem AlgebraicGeometry.Scheme.Hom.ΓSpecIso_inv_comp_resLE_isoSpec_appLE {Z B : Scheme} (k : Z ⟶ B) {V : B.Opens} (hV : IsAffineOpen V) (U : Z.Opens) (e : U ≤ (TopologicalSpace.Opens.map k.base).obj V) (T : (↑U).Opens) : CategoryTheory.CategoryStruct.comp (ΓSpecIso (B.presheaf.obj (Opposite.op V))).inv (appLE (CategoryTheory.CategoryStruct.comp (resLE k V U e) hV.isoSpec.hom) ⊤ T ⋯) = CategoryTheory.CategoryStruct.comp (appLE k V U e) (appLE U.ι U T ⋯)

The map Γ(B, V) ⟶ Γ(U, T) induced by the structure morphism U ⟶ Spec Γ(B, V) of an open subscheme U of Z over the affine open V of B is k.appLE followed by restriction to T.

theorem AlgebraicGeometry.Scheme.Hom.isBasis_range_affineOpens_le_preimage {S S' : Scheme} (g : S' ⟶ S) : TopologicalSpace.Opens.IsBasis (Set.range fun (i : { p : ↑S'.affineOpens × ↑S.affineOpens // ↑p.1 ≤ (TopologicalSpace.Opens.map g.base).obj ↑p.2 }) => ↑(↑i).1)

For a morphism g : S' ⟶ S, the affine opens of S' contained in the preimage of an affine open of S form a basis of the topology of S'.

theorem AlgebraicGeometry.Scheme.Hom.span_range_appTop_sub_eq_top_iff {X : Scheme} [IsAffine X] (f : X ⟶ X) : Ideal.span (Set.range fun (a : ↑(X.presheaf.obj (Opposite.op ⊤))) => (CategoryTheory.ConcreteCategory.hom (appTop f)) a - a) = ⊤ ↔ ∀ (T : Scheme) (x : T ⟶ X), CategoryTheory.CategoryStruct.comp x f = x → IsEmpty ↥T

Fixed points of an endomorphism of an affine scheme. For an endomorphism f of an affine scheme X, the elements f^*(a) - a of Γ(X, ⊤) generate the unit ideal if and only if f fixes no point of X with values in a nonempty scheme: a point x : T ⟶ X with x ≫ f = x forces T to be empty. The ideal generated by these elements cuts out the scheme-theoretic fixed locus of f.

@[instance_reducible]

noncomputable def AlgebraicGeometry.Scheme.globalSectionsMulSemiringAction {X : Scheme} {G : Type u_1} [Group G] (σ : G →* CategoryTheory.Aut X) : MulSemiringAction G ↑(X.presheaf.obj (Opposite.op ⊤))

A group acting on a scheme acts on its global functions, by pullback along inverses: g • a = (σ g⁻¹)^*(a). Pullback reverses composition, so pulling back along inverses makes this a left action. For affine X, this is the ring action whose invariant quotient TauCeti.AffineInvariantQuotient forms.

@[simp]

theorem AlgebraicGeometry.Scheme.globalSectionsMulSemiringAction_smul_def {X : Scheme} {G : Type u_1} [Group G] (σ : G →* CategoryTheory.Aut X) (g : G) (a : ↑(X.presheaf.obj (Opposite.op ⊤))) : g • a = (CategoryTheory.ConcreteCategory.hom (Hom.appTop (σ g⁻¹).asIso.hom)) a

Under Scheme.globalSectionsMulSemiringAction σ, g acts on a global function by pullback along σ g⁻¹.

theorem AlgebraicGeometry.Scheme.toSpecΓ_apply_asIdeal_eq_smul {X : Scheme} {G : Type u_1} [Group G] (σ : G →* CategoryTheory.Aut X) (g : G) (x : ↥X) : (X.toSpecΓ ((σ g).asIso.hom x)).asIdeal = g • (X.toSpecΓ x).asIdeal

For the action of G on global functions by g • a = (σ g⁻¹)^*(a), the point of Spec Γ(X, ⊤) under σ g x has prime ideal the translate by g of that of x: a function vanishes at σ g x exactly when its translate by g⁻¹ vanishes at x.

theorem AlgebraicGeometry.isIso_SpecMap_morphismRestrict_basicOpen_of_injective {R B : Type u} {S : Type u_1} [CommRing R] [CommRing B] [CommSemiring S] [Algebra R B] [Algebra B S] [Algebra R S] [IsScalarTower R B S] (a : R) [IsLocalization.Away a S] (h : Function.Injective ⇑(algebraMap B S)) : CategoryTheory.IsIso (Spec.map (CommRingCat.ofHom (algebraMap R B)) ∣_ PrimeSpectrum.basicOpen a)

Spec of an intermediate ring of a localization. Let S be a localization of R away from a, and let B be an R-algebra whose map to S is injective, for instance an R-subalgebra of S. Then Spec B ⟶ Spec R restricts to an isomorphism over the basic open D(a).

theorem AlgebraicGeometry.IsAffineOpen.mem_basicOpen_iff_notMem_primeIdealOf {X : Scheme} {x : ↥X} {V : X.Opens} (hV : IsAffineOpen V) (hx : x ∈ V) (r : ↑(X.presheaf.obj (Opposite.op V))) : x ∈ X.basicOpen r ↔ r ∉ (hV.primeIdealOf ⟨x, hx⟩).asIdeal

On an affine open V, a point x ∈ V lies in the basic open of a section r iff r is not in the prime ideal of Γ(X, V) corresponding to x.

theorem AlgebraicGeometry.IsAffineOpen.span_setOf_basicOpen_mem_sieve_eq_top {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {S : CategoryTheory.Sieve U} (hS : S ∈ (Opens.grothendieckTopology ↥X) U) : Ideal.span {f : ↑(X.presheaf.obj (Opposite.op U)) | S.arrows (CategoryTheory.homOfLE ⋯)} = ⊤

The basic opens of an affine open U that lie in a covering sieve of U (for the Zariski topology) are defined by functions generating the unit ideal of Γ(X, U).

theorem AlgebraicGeometry.IsAffineOpen.spec_algebraMap_comp_fromSpec_apply {S : Scheme} {U : S.Opens} (hU : IsAffineOpen U) {s : ↥S} (hs : s ∈ U) (R : Type u) [CommRing R] [Algebra (↑(S.presheaf.obj (Opposite.op U))) R] (u : ↥(Spec ↧R)) [u.asIdeal.LiesOver (hU.primeIdealOf ⟨s, hs⟩).asIdeal] : (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (algebraMap (↑(S.presheaf.obj (Opposite.op U))) R))) hU.fromSpec) u = s

The map Spec R ⟶ U ⊆ S induced by the structure map of a Γ(S, U)-algebra R on an affine open U sends a point u of Spec R over the prime s of Γ(S, U) to s.

theorem AlgebraicGeometry.Scheme.Hom.eq_of_comp_eq_of_forall_liesOver_eq {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {Y : Scheme} (p : Y ⟶ Spec ↧R) (g : Spec ↧A ⟶ Y) [IsOpenImmersion g] (hgp : CategoryTheory.CategoryStruct.comp g p = Spec.map (CommRingCat.ofHom (algebraMap R A))) (e : A) (u : ↥(Spec ↧R)) (v : ↥(Spec ↧A)) (huniq : ∀ (P'' : Ideal A), P''.IsPrime → P''.LiesOver u.asIdeal → e ∉ P'' → P'' = v.asIdeal) (hv : g v ∈ (opensFunctor g).obj (PrimeSpectrum.basicOpen e)) (w : ↥((opensFunctor g).obj (PrimeSpectrum.basicOpen e))) (hw : p ↑w = u) : w = ⟨g v, hv⟩

Uniqueness of the point g v of g(D(e)) over u: if an open immersion g from Spec A into a scheme Y over Spec R is compatible with R → A, a point g z of g(D(e)) over u has z over the prime u with e ∉ z, so z = v if v is the only such prime.

theorem TauCeti.AlgebraicGeometry.overPullback_map_bijective_of_isIso_appTop {S T : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine S] (j : T ⟶ S) {Y Y' : CategoryTheory.Over S} [AlgebraicGeometry.IsAffine Y'.left] (h : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.fst Y.hom j))) : Function.Bijective fun (g : Y ⟶ Y') => (CategoryTheory.Over.pullback j).map g

Let j : T ⟶ S be a morphism to an affine scheme, Y a scheme over S and Y' an affine scheme over S. If restriction of global sections Γ(Y, 𝒪) → Γ(Y ×_S T, 𝒪) is an isomorphism, then base change along j is a bijection from morphisms Y ⟶ Y' over S to morphisms Y ×_S T ⟶ Y' ×_S T over T.

theorem TauCeti.AlgebraicGeometry.Spec.exists_isIso_appTop_eq_comp_of_bijective {R S : CommRingCat} (f : R ⟶ S) {X : AlgebraicGeometry.Scheme} (p : X ⟶ AlgebraicGeometry.Spec R) (W : (AlgebraicGeometry.Spec S).Opens) (hW : Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop W.ι))) (e : X ≅ ↑W) (he : CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp W.ι (AlgebraicGeometry.Spec.map f)) = p) : ∃ (σ : S ⟶ X.presheaf.obj (Opposite.op ⊤)), CategoryTheory.IsIso σ ∧ CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv (AlgebraicGeometry.Scheme.Hom.appTop p) = CategoryTheory.CategoryStruct.comp f σ

Let f : R ⟶ S be a ring map and W an open of Spec S from which S is recovered: the restriction Γ(Spec S, ⊤) → Γ(W, ⊤) is bijective. If a scheme X over Spec R is identified with W over Spec R, then the map R → Γ(X, ⊤) induced by X ⟶ Spec R is f followed by an isomorphism.

theorem TauCeti.AlgebraicGeometry.exists_affine_pair_comp_eq {S : AlgebraicGeometry.Scheme} {T T' : CategoryTheory.Over S} (f : T' ⟶ T) [AlgebraicGeometry.IsAffine T.left] [AlgebraicGeometry.IsAffine T'.left] : ∃ (Z : CategoryTheory.Over S) (_ : AlgebraicGeometry.IsAffine Z.left) (g₁ : Z ⟶ T') (g₂ : Z ⟶ T') (κ : ↑(Z.left.presheaf.obj (Opposite.op ⊤)) →+* TensorProduct ↑(T.left.presheaf.obj (Opposite.op ⊤)) ↑(T'.left.presheaf.obj (Opposite.op ⊤)) ↑(T'.left.presheaf.obj (Opposite.op ⊤))), CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f ∧ (∀ (a : ↑(T'.left.presheaf.obj (Opposite.op ⊤))), κ ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Over.Hom.left g₁))) a) = a ⊗ₜ[↑(T.left.presheaf.obj (Opposite.op ⊤))] 1) ∧ ∀ (a : ↑(T'.left.presheaf.obj (Opposite.op ⊤))), κ ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Over.Hom.left g₂))) a) = 1 ⊗ₜ[↑(T.left.presheaf.obj (Opposite.op ⊤))] a

For a morphism f : T' ⟶ T of affine S-schemes, the scheme Spec (Γ(T', 𝒪) ⊗[Γ(T, 𝒪)] Γ(T', 𝒪)) is an affine S-scheme with two maps g₁, g₂ to T' that agree after composing with f. Under the identification κ of its global sections with the tensor product, they induce the two inclusions of the factors.