The slice equivalences and the structure sheaf

Mathlib's Scheme.Modules.overEquiv U identifies sheaves of modules on the slice of the Zariski site over U with module sheaves on the open subscheme U. This file records that both halves of the equivalence match the structure sheaves, in the shape unit ≅ F.obj unit that SheafOfModules.Presentation.map and its relatives take as their structure-sheaf identification.

Main definitions

• overEquivFunctorUnitIso, overEquivInverseUnitIso: the two identifications.

noncomputable def AlgebraicGeometry.Scheme.Modules.overEquivFunctorUnitIso {X : Scheme} (U : X.Opens) : SheafOfModules.unit (↑U).ringCatSheaf ≅ (overEquiv U).functor.obj (SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf U))

The structure sheaf of the open subscheme is the image of the slice's structure sheaf under the slice equivalence. Stated as unit ≅ F.obj unit, the shape Presentation.map takes for its η; it is the inverses of restrictUnitIso and of overFunctorEquiv at the structure sheaf.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.overEquivInverseUnitIso {X : Scheme} (V : X.Opens) : SheafOfModules.unit (CategoryTheory.Sheaf.over X.ringCatSheaf V) ≅ (overEquiv V).inverse.obj (SheafOfModules.unit (↑V).ringCatSheaf)

The slice's structure sheaf is the image of the open subscheme's under the inverse slice equivalence: overEquivFunctorUnitIso transported by the inverse, corrected by the unit of the equivalence.

Equations

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