The ring sheaf is the native pushforward of the structure sheaf and its structure morphism is the original morphism's sheaf map. Its underlying module is identified with the native direct image of the unit module, using identity maps on the actual section modules and their restrictions.
The native direct image of the source's sheaf of commutative rings.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X)def sheaf : TopCat.Sheaf CommRingCat.{u} XThe structure map is the original morphism's map on structure sheaves.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X)def structureMap : X.sheaf ⟶ sheaf g where
hom := g.cThe algebra's underlying module is the actual direct image of the source unit module, including its original scalar and restriction maps.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X)def underlyingModuleIso :
RelativeSpec.underlyingModule (structureMap g) ≅
(Modules.pushforward g).obj (SheafOfModules.unit T.ringCatSheaf)