Algebras of functions under pushforward

The lax symmetric monoidal pushforward of module sheaves carries commutative algebras to commutative algebras. Its sections on an open are the sections of the original algebra on the inverse image, with the same ring operations. In particular, pushing forward the tensor-unit algebra gives the algebra of regular functions of a scheme over its base, on the actual pushforward of its structure sheaf.

The construction uses Mathlib's Functor.mapCommMon and CommMon.trivial, together with the canonical lax monoidal pushforward of sheaves of modules. The section calculation identifies its multiplication with multiplication of regular functions; it is needed to recover coordinate algebras from affine morphisms.

References

• The Stacks Project, Tag 01LL (quasi-coherent algebras and relative spectra).

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CommMon Y.Modules

The algebra of regular functions of X over Y, carried by the actual pushforward f_* 𝒪_X. The algebra structure is induced by lax symmetric monoidal pushforward.

Equations

• AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra f = (AlgebraicGeometry.Scheme.Modules.pushforward f).mapCommMon.obj (CategoryTheory.CommMon.trivial X.Modules)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra_X {X Y : Scheme} (f : X ⟶ Y) : (pushforwardStructureAlgebra f).X = (Modules.pushforward f).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit X.Modules)

The underlying module of the function algebra is the pushforward of the structure sheaf.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra_one {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.MonObj.one = SheafOfModules.unitToPushforwardObjUnit (toRingCatSheafHom f)

The unit of the function algebra is the map on regular functions induced by f.

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraSectionsRingEquiv {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : ↑((pushforwardStructureAlgebra f).X.presheaf.obj (Opposite.op U)) ≃+* ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))

On each open of the base, the function algebra is the ordinary ring of regular functions on the inverse image.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraSectionsRingEquiv_apply {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↑((pushforwardStructureAlgebra f).X.presheaf.obj (Opposite.op U))) : (pushforwardStructureAlgebraSectionsRingEquiv f U) x = x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraSectionsRingEquiv_symm_apply {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))) : (pushforwardStructureAlgebraSectionsRingEquiv f U).symm x = x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra_algebraMap {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (r : ↑(Y.presheaf.obj (Opposite.op U))) : (algebraMap ↑(Y.presheaf.obj (Opposite.op U)) ↑((pushforwardStructureAlgebra f).X.presheaf.obj (Opposite.op U))) r = (CategoryTheory.ConcreteCategory.hom (app f U)) r

The structure map on sections of the function algebra is pullback of regular functions along the scheme morphism.

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraPresheafIso {X Y : Scheme} (f : X ⟶ Y) : (pushforwardStructureAlgebra f).sectionsPresheaf ≅ (TopologicalSpace.Opens.map f.base).op.comp X.presheaf

The presheaf of rings underlying the function algebra is naturally the direct image of the structure presheaf.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraPresheafIso_hom_app {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opensᵒᵖ) : (pushforwardStructureAlgebraPresheafIso f).hom.app U = (pushforwardStructureAlgebraSectionsRingEquiv f (Opposite.unop U)).toCommRingCatIso.hom

The comparison with regular functions is given on each open by the section-ring equivalence of the function algebra.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraPresheafIso_inv_app {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opensᵒᵖ) : (pushforwardStructureAlgebraPresheafIso f).inv.app U = (pushforwardStructureAlgebraSectionsRingEquiv f (Opposite.unop U)).toCommRingCatIso.inv

The inverse comparison with regular functions is given on each open by the inverse section-ring equivalence of the function algebra.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra_toSectionsPresheaf_comp {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (pushforwardStructureAlgebra f).toSectionsPresheaf (pushforwardStructureAlgebraPresheafIso f).hom = f.c

The presheaf comparison identifies the algebra's structure map with the actual structure-presheaf morphism of the scheme map.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebra_toSectionsPresheaf_comp_assoc {X Y : Scheme} (f : X ⟶ Y) {Z : TopCat.Presheaf CommRingCat ↑Y.toPresheafedSpace} (h : (TopologicalSpace.Opens.map f.base).op.comp X.presheaf ⟶ Z) : CategoryTheory.CategoryStruct.comp (pushforwardStructureAlgebra f).toSectionsPresheaf (CategoryTheory.CategoryStruct.comp (pushforwardStructureAlgebraPresheafIso f).hom h) = CategoryTheory.CategoryStruct.comp f.c h

The presheaf comparison identifies the algebra's structure map with the actual structure-presheaf morphism of the scheme map.