Coherence of internal Hom under pullback #
The canonical internal-Hom comparison respects the identity and composition isomorphisms of module pullback. These equations allow base change of internal Hom to be iterated without choosing new comparison maps. The source is quasicoherent and the target is arbitrary; these coherence equations assume neither flatness nor invertibility of the internal-Hom comparison.
If the comparison along f is invertible, the composition criterion identifies invertibility
along f ≫ g with invertibility of the pullback along f of the comparison along g. This
allows invertibility to be checked on open covers.
Composed with the identification f^* 𝒪_Y ≅ 𝒪_X, the comparison at the structure sheaf is the
base-change map f^* 𝓗om(M, 𝒪_Y) ⟶ 𝓗om(f^* M, 𝒪_X) of linear functionals. It is compatible with
composites and with replacing f by an equal morphism, and it carries the pullback of evaluation
at a global section s of M to evaluation at the pulled-back section of f^* M. For finite
locally free M, the compatibility with composites matches the identifications of functionals on
duals with sections (Scheme.Hom.dualHomUnitEquiv_inv_pullbackIhomComparison_app_unit_comp).
These are the inputs for the naturality, in the test scheme, of descriptions of points by sections
or by linear functionals.
The equations use Mathlib's Scheme.Modules.pullbackId and pullbackComp, and the canonical
tensor comparison of module pullback. For finite locally free sources they also describe the
coherence of the resulting internal-Hom base-change isomorphisms.
References #
- The Stacks Project, Tag 0C6I (base change for sheaf Hom).
The internal-Hom comparison along the identity is the internal-Hom map induced by the canonical identity isomorphism of module pullback.
The internal-Hom comparison along the identity is the internal-Hom map induced by the canonical identity isomorphism of module pullback.
The internal-Hom comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism on its source, target, and argument.
The internal-Hom comparison for a composite agrees with the two successive comparisons, using the canonical composition isomorphism on its source, target, and argument.
If the internal-Hom comparison along f is invertible on the pullbacks of M and N,
then invertibility along f ≫ g is equivalent to invertibility of the pullback along f
of the comparison along g. This allows invertibility to be checked on open covers.
The base-change map f^* 𝓗om(M, 𝒪_Y) ⟶ 𝓗om(f^* M, 𝒪_X) of linear functionals, the
internal-Hom comparison at the structure sheaf followed by f^* 𝒪_Y ≅ 𝒪_X, is compatible with
composites: along f ≫ g it is the pullback along f of the map along g followed by the map
along f, through the composition isomorphism of pullback.
The base-change map f^* 𝓗om(M, 𝒪_Y) ⟶ 𝓗om(f^* M, 𝒪_X) of linear functionals, the
internal-Hom comparison at the structure sheaf followed by f^* 𝒪_Y ≅ 𝒪_X, is compatible with
composites: along f ≫ g it is the pullback along f of the map along g followed by the map
along f, through the composition isomorphism of pullback.
For finite locally free M, base change of linear functionals along f ≫ g is compatible
with the identifications Scheme.Modules.dualHomUnitEquiv of functionals on duals with sections:
the functional on (f ≫ g)^* M^∨ obtained from a functional ψ on f^* (g^* M)^∨ corresponds to
the section of f^* g^* M of ψ, through f^* g^* M ≅ (f ≫ g)^* M.
The base-change map of linear functionals is unchanged, up to the canonical identifications, when the scheme morphism is replaced by an equal one.
The base-change map of linear functionals is unchanged, up to the canonical identifications, when the scheme morphism is replaced by an equal one.
Evaluation at a section commutes with pullback. For a global section s : 𝒪_Y ⟶ M, the
pullback along f of evaluation 𝓗om(M, 𝒪_Y) ⟶ 𝒪_Y at s, followed by f^* 𝒪_Y ≅ 𝒪_X, is the
base-change map f^* 𝓗om(M, 𝒪_Y) ⟶ 𝓗om(f^* M, 𝒪_X) followed by evaluation at the pulled-back
section 𝒪_X ≅ f^* 𝒪_Y ⟶ f^* M.
Evaluation at a section commutes with pullback. For a global section s : 𝒪_Y ⟶ M, the
pullback along f of evaluation 𝓗om(M, 𝒪_Y) ⟶ 𝒪_Y at s, followed by f^* 𝒪_Y ≅ 𝒪_X, is the
base-change map f^* 𝓗om(M, 𝒪_Y) ⟶ 𝓗om(f^* M, 𝒪_X) followed by evaluation at the pulled-back
section 𝒪_X ≅ f^* 𝒪_Y ⟶ f^* M.