Pullback of the symmetric algebra

For a morphism of schemes f : X ⟶ Y and a quasicoherent sheaf F on Y, the pullback of the symmetric algebra of F is the symmetric algebra of the pullback of F:

f^* (Sym F) ≅ Sym (f^* F)

as quasicoherent commutative 𝒪_X-algebras, naturally in F.

Both sides are free constructions with the same universal property. Algebra maps f^* (Sym F) ⟶ B into a commutative 𝒪_X-algebra B are algebra maps Sym F ⟶ f_* B (QuasicoherentAlgebra.pullbackHomEquiv), hence module maps F ⟶ f_* B (symmetricAlgebraHomEquiv). Algebra maps Sym (f^* F) ⟶ B are module maps f^* F ⟶ B, hence module maps F ⟶ f_* B by the pullback–pushforward adjunction. The two bijections are natural in B, and the isomorphism is the one they induce. On generators it is the pullback of the inclusion F ⟶ Sym F (symmetricAlgebraι_comp_pullbackSymmetricAlgebraIso_inv).

Main declarations

• TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraIso: the isomorphism f^* (Sym F) ≅ Sym (f^* F) of quasicoherent algebras;
• TauCeti.AlgebraicGeometry.symmetricAlgebraι_comp_pullbackSymmetricAlgebraIso_inv and TauCeti.AlgebraicGeometry.pullback_map_symmetricAlgebraι_comp_pullbackSymmetricAlgebraIso_hom: on generators it identifies the pullback of the inclusion F ⟶ Sym F with the inclusion f^* F ⟶ Sym (f^* F);
• TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraNatIso: the isomorphism is natural in F.

References

• The Stacks Project, Tag 01M1.
• A. Grothendieck, J. Dieudonné, Éléments de géométrie algébrique II, 1.7.

noncomputable def TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) : (QuasicoherentAlgebra.pullback f).obj ((symmetricAlgebra Y).obj F) ≅ (symmetricAlgebra X).obj ((QuasicoherentSheaf.pullback f).obj F)

Pullback of the symmetric algebra. For a morphism of schemes f : X ⟶ Y and a quasicoherent sheaf F on Y, the pullback f^* (Sym F) of the symmetric algebra of F is isomorphic, as a quasicoherent commutative 𝒪_X-algebra, to the symmetric algebra Sym (f^* F) of the pullback of F.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_comp_pullbackSymmetricAlgebraIso_inv {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) : CategoryTheory.CategoryStruct.comp (symmetricAlgebraι ((QuasicoherentSheaf.pullback f).obj F)) (pullbackSymmetricAlgebraIso f F).inv.hom.hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map (symmetricAlgebraι F)) (CategoryTheory.eqToHom ⋯))

On generators, the inverse of pullbackSymmetricAlgebraIso is the pullback of the inclusion F ⟶ Sym F: it restricts on f^* F to f^* F ⟶ f^* (Sym F).

theorem TauCeti.AlgebraicGeometry.pullback_map_symmetricAlgebraι_comp_pullbackSymmetricAlgebraIso_hom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback f).map (symmetricAlgebraι F)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (pullbackSymmetricAlgebraIso f F).hom.hom.hom.hom)) = symmetricAlgebraι ((QuasicoherentSheaf.pullback f).obj F)

On generators, pullbackSymmetricAlgebraIso sends the pullback of the inclusion F ⟶ Sym F to the inclusion f^* F ⟶ Sym (f^* F).

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraIso_hom_naturality {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) {F' : QuasicoherentSheaf Y} (g : F' ⟶ F) : CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullback f).map ((symmetricAlgebra Y).map g)) (pullbackSymmetricAlgebraIso f F).hom = CategoryTheory.CategoryStruct.comp (pullbackSymmetricAlgebraIso f F').hom ((symmetricAlgebra X).map ((QuasicoherentSheaf.pullback f).map g))

The isomorphism pullbackSymmetricAlgebraIso is natural in the quasicoherent sheaf.

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraIso_hom_naturality_assoc {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) {F' : QuasicoherentSheaf Y} (g : F' ⟶ F) {Z : QuasicoherentAlgebra X} (h : GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.obj ((gradedSymmetricAlgebra X).obj ((QuasicoherentSheaf.pullback f).obj F)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((QuasicoherentAlgebra.pullback f).map (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map ((gradedSymmetricAlgebra Y).map g))) (CategoryTheory.CategoryStruct.comp (pullbackSymmetricAlgebraIso f F).hom h) = CategoryTheory.CategoryStruct.comp (pullbackSymmetricAlgebraIso f F').hom (CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map ((gradedSymmetricAlgebra X).map ((QuasicoherentSheaf.pullback f).map g))) h)

The isomorphism pullbackSymmetricAlgebraIso is natural in the quasicoherent sheaf.

noncomputable def TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraNatIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : (symmetricAlgebra Y).comp (QuasicoherentAlgebra.pullback f) ≅ (QuasicoherentSheaf.pullback f).comp (symmetricAlgebra X)

Pullback of the symmetric algebra, naturally. For a morphism of schemes f : X ⟶ Y, pulling back the symmetric algebra of a quasicoherent sheaf on Y is naturally isomorphic to taking the symmetric algebra of its pullback.

@[simp]

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraNatIso_hom_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) : (pullbackSymmetricAlgebraNatIso f).hom.app F = (pullbackSymmetricAlgebraIso f F).hom

The components of pullbackSymmetricAlgebraNatIso are pullbackSymmetricAlgebraIso.

@[simp]

theorem TauCeti.AlgebraicGeometry.pullbackSymmetricAlgebraNatIso_inv_app {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (F : QuasicoherentSheaf Y) : (pullbackSymmetricAlgebraNatIso f).inv.app F = (pullbackSymmetricAlgebraIso f F).inv

The inverse components of pullbackSymmetricAlgebraNatIso are the inverses of pullbackSymmetricAlgebraIso.