Pullback of local sections #
The unit of pullback and pushforward gives a semilinear map on sections over every open.
These maps commute with coefficient maps, restriction, and composition of scheme morphisms.
Scheme.Hom.pullbackSectionsLE also restricts the pullback to any smaller open in the source.
The composition equation identifies direct and iterated pullback through the canonical
pullback-composition isomorphism, so sections can be compared across successive morphisms.
Pullback of sections is also compatible with the oplax monoidal structure of pullback: the
tensor comparison g^* (M ⊗ N) ⟶ g^* M ⊗ g^* N sends the pullback of the image of x ⊗ y to the
image of the tensor product of the pullbacks of x and y, and the identification
g^* 𝒪_X ≅ 𝒪_Y sends the pullback of a function r to g^♯ r. These make pullback of sections
multiplicative on sections of algebras.
Along the inclusion U.ι of an open, pulling back sections over U is a bijection onto the global
sections of the pullback (Scheme.Modules.bijective_pullbackSectionsLE_ι). A morphism out of a
pullback is determined by its values on pulled-back sections (Scheme.Modules.pullback_hom_ext).
Pulling back sections along g, as a semilinear map over pullback of local functions.
Instances For
Pullback of sections is the component of the pullback--pushforward adjunction unit.
Pullback of sections is natural in the coefficient sheaf.
Pullback of sections commutes with restriction to smaller opens.
The tensor comparison g^* (M ⊗ N) ⟶ g^* M ⊗ g^* N of pullback sends the pullback of the
image of x ⊗ y in the sections of M ⊗ N to the image of the tensor product of the pullbacks of
x and y.
The identification g^* 𝒪_X ≅ 𝒪_Y sends the pullback of a function r on U to the
function g^♯ r on g⁻¹ U.
The composition comparison carries the pullback of a section to its iterated pullback.
Pull back a section along g and restrict it to an open contained in its inverse image.
Instances For
Pullback to a smaller open is restriction of the pullback to the full inverse image.
Pullback to a smaller open commutes with restriction of the section in the target.
Pullback to the full inverse image agrees with the canonical section pullback.
Pullback to a smaller open is natural in the coefficient sheaf.
The pullback comparison for equal scheme morphisms preserves pulled-back sections.
The composition comparison carries direct pullback to iterated pullback on smaller opens.
The forward composition comparison carries iterated pullback to direct pullback.
Pulling back sections over U along the open immersion U.ι : U ⟶ Y identifies them with the
global sections of the pullback to U. The global open is given as any T equal to ⊤, such as
the preimage of ⊤ under a morphism into U.
For h : f ≫ g = gf, pulling a global section back along gf and identifying
gf^* M ≅ f^* g^* M gives its iterated pullback along g and then f.
A morphism out of a pullback g^* M is determined by its values on the pullbacks of the
sections of M.
The pullback of the global section 1 of the structure sheaf is the global section 1,
under the identification g^* 𝒪_X ≅ 𝒪_Y.