Sections of pushed-forward commutative algebras

The lax symmetric monoidal pushforward of module sheaves carries commutative algebras to commutative algebras. On each open, its sections are the sections of the original algebra on the inverse image, with the same ring operations and compatible restrictions. The tensor-unit algebra has the structure presheaf as its presheaf of sections.

The comparisons use Mathlib's Functor.mapCommMon, CommMon.trivial, RingEquiv.ofBijective and NatIso.ofComponents, together with the canonical lax monoidal pushforward of module sheaves.

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardSectionsRingEquiv {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) (U : Y.Opens) : ↑(((Modules.pushforward f).mapCommMon.obj A).X.presheaf.obj (Opposite.op U)) ≃+* ↑(A.X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))

Sections of a pushed-forward commutative algebra have exactly the ring structure of the sections of the original algebra on the inverse image.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardSectionsRingEquiv_apply {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) (U : Y.Opens) (x : ↑(((Modules.pushforward f).mapCommMon.obj A).X.presheaf.obj (Opposite.op U))) : (pushforwardSectionsRingEquiv f A U) x = x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardSectionsRingEquiv_symm_apply {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) (U : Y.Opens) (x : ↑(A.X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))) : (pushforwardSectionsRingEquiv f A U).symm x = x

theorem AlgebraicGeometry.Scheme.Hom.pushforwardSectionsRingEquiv_restrictSections {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) {U V : Y.Opens} (i : V ⟶ U) (x : ↑(((Modules.pushforward f).mapCommMon.obj A).X.presheaf.obj (Opposite.op U))) : (pushforwardSectionsRingEquiv f A V) ((((Modules.pushforward f).mapCommMon.obj A).restrictSections i) x) = (A.restrictSections ((TopologicalSpace.Opens.map f.base).map i)) ((pushforwardSectionsRingEquiv f A U) x)

The section-ring comparison for pushforward commutes with restriction to smaller opens.

noncomputable def AlgebraicGeometry.Scheme.Hom.pushforwardSectionsPresheafIso {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) : ((Modules.pushforward f).mapCommMon.obj A).sectionsPresheaf ≅ (TopologicalSpace.Opens.map f.base).op.comp A.sectionsPresheaf

The presheaf of sections of a pushed-forward commutative algebra is naturally the direct image of its presheaf of sections.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardSectionsPresheafIso_hom_app {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) (U : Y.Opensᵒᵖ) : (pushforwardSectionsPresheafIso f A).hom.app U = (pushforwardSectionsRingEquiv f A (Opposite.unop U)).toCommRingCatIso.hom

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.pushforwardSectionsPresheafIso_inv_app {X Y : Scheme} (f : X ⟶ Y) (A : CategoryTheory.CommMon X.Modules) (U : Y.Opensᵒᵖ) : (pushforwardSectionsPresheafIso f A).inv.app U = (pushforwardSectionsRingEquiv f A (Opposite.unop U)).toCommRingCatIso.inv

@[simp]

theorem AlgebraicGeometry.Scheme.structureAlgebraSections_algebraMap (X : Scheme) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : (algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↑((CategoryTheory.CommMon.trivial X.Modules).X.presheaf.obj (Opposite.op U))) r = r

The structure map of the tensor-unit algebra acts identically on regular functions.

noncomputable def AlgebraicGeometry.Scheme.structureAlgebraSectionsRingEquiv (X : Scheme) (U : X.Opens) : ↑((CategoryTheory.CommMon.trivial X.Modules).X.presheaf.obj (Opposite.op U)) ≃+* ↑(X.presheaf.obj (Opposite.op U))

The tensor-unit algebra has the ordinary ring of regular functions as its sections.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.structureAlgebraSectionsRingEquiv_apply (X : Scheme) (U : X.Opens) (x : ↑((CategoryTheory.CommMon.trivial X.Modules).X.presheaf.obj (Opposite.op U))) : (X.structureAlgebraSectionsRingEquiv U) x = x

@[simp]

theorem AlgebraicGeometry.Scheme.structureAlgebraSectionsRingEquiv_symm_apply (X : Scheme) (U : X.Opens) (x : ↑(X.presheaf.obj (Opposite.op U))) : (X.structureAlgebraSectionsRingEquiv U).symm x = x

noncomputable def AlgebraicGeometry.Scheme.structureAlgebraSectionsPresheafIso (X : Scheme) : (CategoryTheory.CommMon.trivial X.Modules).sectionsPresheaf ≅ X.presheaf

The presheaf of sections of the tensor-unit algebra is the structure presheaf.

Equations

• X.structureAlgebraSectionsPresheafIso = CategoryTheory.NatIso.ofComponents (fun (U : X.Opensᵒᵖ) => (X.structureAlgebraSectionsRingEquiv (Opposite.unop U)).toCommRingCatIso) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.structureAlgebraSectionsPresheafIso_hom_app (X : Scheme) (U : X.Opensᵒᵖ) : X.structureAlgebraSectionsPresheafIso.hom.app U = (X.structureAlgebraSectionsRingEquiv (Opposite.unop U)).toCommRingCatIso.hom

@[simp]

theorem AlgebraicGeometry.Scheme.structureAlgebraSectionsPresheafIso_inv_app (X : Scheme) (U : X.Opensᵒᵖ) : X.structureAlgebraSectionsPresheafIso.inv.app U = (X.structureAlgebraSectionsRingEquiv (Opposite.unop U)).toCommRingCatIso.inv