Functoriality of the algebra of regular functions

A scheme p : V ⟶ X over X has a commutative 𝒪ₓ-algebra of regular functions, carried by the actual pushforward p_* 𝒪_V (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra). This file makes that algebra contravariantly functorial in schemes over X: a morphism g : V ⟶ W over X pulls back regular functions, giving a morphism of 𝒪ₓ-algebras q_* 𝒪_W ⟶ p_* 𝒪_V.

The morphism of algebras is the pushforward along q of the unit 𝒪_W ⟶ g_* 𝒪_V of the function algebra of g, transported along the identification q_* g_* ≅ (g ≫ q)_* = p_* of lax monoidal functors, using Mathlib's Functor.mapCommMon and Functor.mapCommMonNatTrans.

Main declarations

• AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap g h: the morphism of function algebras q_* 𝒪_W ⟶ p_* 𝒪_V induced by g : V ⟶ W with h : g ≫ q = p;
• AlgebraicGeometry.Scheme.Hom.sectionsAlgHom_pushforwardStructureAlgebraMap_apply: on sections over U, it is the map Γ(W, q⁻¹ U) ⟶ Γ(V, p⁻¹ U) induced by g;
• AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap_id and AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap_comp: functoriality.

References

• The Stacks Project, Tag 01LL (relative spectrum).
• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II, §1.3.

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap {X V W : Scheme} {p : V ⟶ X} {q : W ⟶ X} (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) : pushforwardStructureAlgebra q ⟶ pushforwardStructureAlgebra p

The morphism of function algebras q_* 𝒪_W ⟶ p_* 𝒪_V induced by a morphism g : V ⟶ W of schemes over X: pullback of regular functions along g. It is the pushforward along q of the unit 𝒪_W ⟶ g_* 𝒪_V of the function algebra of g, followed by the identification q_* g_* ≅ (g ≫ q)_* = p_* of lax monoidal functors.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap_hom {X V W : Scheme} {p : V ⟶ X} {q : W ⟶ X} (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) : (pushforwardStructureAlgebraMap g h).hom.hom = CategoryTheory.CategoryStruct.comp ((Modules.pushforward q).map (SheafOfModules.unitToPushforwardObjUnit (toRingCatSheafHom g))) (CategoryTheory.CategoryStruct.comp ((Modules.pushforwardComp g q).hom.app (SheafOfModules.unit V.ringCatSheaf)) ((Modules.pushforwardCongr h).hom.app (SheafOfModules.unit V.ringCatSheaf)))

As a morphism of modules, the morphism of function algebras induced by g is the pushforward along q of the map 𝒪_W ⟶ g_* 𝒪_V given by g on sections, followed by the identification q_* g_* ≅ (g ≫ q)_* = p_*.

theorem AlgebraicGeometry.Scheme.Hom.sectionsAlgHom_pushforwardStructureAlgebraMap_apply {X V W : Scheme} {p : V ⟶ X} {q : W ⟶ X} (g : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g q = p) (U : X.Opens) (x : ↑((pushforwardStructureAlgebra q).X.presheaf.obj (Opposite.op U))) : (CategoryTheory.CommMon.sectionsAlgHom (pushforwardStructureAlgebraMap g h) U) x = (pushforwardStructureAlgebraSectionsRingEquiv p U).symm ((CategoryTheory.ConcreteCategory.hom (appLE g ((TopologicalSpace.Opens.map q.base).obj U) ((TopologicalSpace.Opens.map p.base).obj U) ⋯)) ((pushforwardStructureAlgebraSectionsRingEquiv q U) x))

On sections over an open U of the base, the morphism of function algebras induced by g is the pullback Γ(W, q⁻¹ U) ⟶ Γ(V, p⁻¹ U) of regular functions along g.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap_id {X V : Scheme} {p : V ⟶ X} : pushforwardStructureAlgebraMap (CategoryTheory.CategoryStruct.id V) ⋯ = CategoryTheory.CategoryStruct.id (pushforwardStructureAlgebra p)

The identity of a scheme over X induces the identity of its function algebra.

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap_comp {X V W : Scheme} {p : V ⟶ X} {q : W ⟶ X} {V' : Scheme} {p' : V' ⟶ X} (g : V' ⟶ V) (g' : V ⟶ W) (h : CategoryTheory.CategoryStruct.comp g p = p') (h' : CategoryTheory.CategoryStruct.comp g' q = p) : pushforwardStructureAlgebraMap (CategoryTheory.CategoryStruct.comp g g') ⋯ = CategoryTheory.CategoryStruct.comp (pushforwardStructureAlgebraMap g' h') (pushforwardStructureAlgebraMap g h)

Pullback of regular functions is contravariantly functorial in morphisms over X.