Sections of commutative algebras of modules on schemes #
A commutative monoid object in X.Modules has a commutative ฮ(X, U)-algebra of sections
on each open U. Restriction is a ring homomorphism, giving a presheaf of commutative rings
under the structure presheaf of X.
These constructions use Mathlib's Functor.mapCommMon and the equivalence between monoid
objects in modules and algebras, applied to the lax braided sections functor.
The sections over U of a commutative ๐ชโ-algebra, as a commutative monoid object in
ฮ(X, U)-modules: the image of A under the lax braided sections functor.
Equations
Instances For
The sections of a commutative ๐ชโ-algebra over an open form a commutative ring. Its
multiplication is the monoid multiplication of A applied to the image of x โโ y in the sections
of the tensor product (CategoryTheory.CommMon.sections_mul_def).
Equations
The sections of a commutative ๐ชโ-algebra over an open U form a ฮ(X, U)-algebra, whose
scalar multiplication is that of the sections of the underlying ๐ชโ-module.
Equations
The product of two sections of a commutative ๐ชโ-algebra is the multiplication of A
applied to the image of their tensor product under the tensor map of the sections functor.
The structure map ฮ(X, U) โ ฮ(A.X, U) of a commutative ๐ชโ-algebra is the unit of A on
sections over U.
Restriction of sections of a commutative ๐ชโ-algebra along an inclusion of opens V โค U,
as a ring homomorphism.
Equations
- A.restrictSections i = { toFun := โ(CategoryTheory.ConcreteCategory.hom (A.X.presheaf.map i.op)), map_one' := โฏ, map_mul' := โฏ, map_zero' := โฏ, map_add' := โฏ }
Instances For
The presheaf of commutative rings of sections of a commutative ๐ชโ-algebra.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure morphism from the structure presheaf of X to the presheaf of sections of a
commutative ๐ชโ-algebra, given on each open by the algebra map.
Equations
- One or more equations did not get rendered due to their size.