The relative spectrum of a symmetric algebra

For a quasicoherent sheaf F on a scheme X, the relative spectrum Spec_X (Sym F) of its symmetric algebra is the scheme over X that represents 𝒪-linear functionals on F (Stacks Project, Tag 01M1, and EGA II, §1.7). For a scheme q : T ⟶ X, morphisms T ⟶ Spec_X (Sym F) over X correspond to

• morphisms of 𝒪_X-modules F ⟶ q_* 𝒪_T (relativeSpecSymmetricAlgebraHomEquiv), naturally in F and in T (relativeSpecSymmetricAlgebraHomIso); and
• morphisms of 𝒪_T-modules q^* F ⟶ 𝒪_T (relativeSpecSymmetricAlgebraPullbackHomEquiv), naturally in F, and in T through pullback of linear functionals.

The first is the universal property of relative Spec, relativeSpecHomIso, followed by the universal property of the symmetric algebra as the free commutative algebra, symmetricAlgebraHomEquiv; the second follows from the first by the adjunction between pullback and pushforward of modules. This is the contravariant linear scheme 𝕍(F) of a quasicoherent sheaf; for a finite locally free E, the total space of the vector bundle E is the relative spectrum of the symmetric algebra of the dual of E.

The relative spectrum of a symmetric algebra commutes with base change: for f : Y ⟶ X, Spec_Y (Sym (f^* F)) is the fibre product Y ×_X Spec_X (Sym F), naturally in F (relativeSpecSymmetricAlgebraBaseChangeIso). This is base change of relative Spec, relativeSpecBaseChangeIso, applied to the identification f^* (Sym F) ≅ Sym (f^* F) (pullbackSymmetricAlgebraIso). On points, the projection Spec_Y (Sym (f^* F)) ⟶ Spec_X (Sym F) (relativeSpecSymmetricAlgebraPullbackFst) sends a point over q : T ⟶ Y with linear functional q^* f^* F ⟶ 𝒪_T to the point over q ≫ f with the same functional on (q ≫ f)^* F ≅ q^* f^* F (relativeSpecSymmetricAlgebraPullbackHomEquiv_map_comp_relativeSpecSymmetricAlgebraPullbackFst).

Main declarations

• TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv: morphisms T ⟶ Spec_X (Sym F) over X are module maps F ⟶ q_* 𝒪_T, with naturality in the scheme (relativeSpecSymmetricAlgebraHomEquiv_comp) and in the sheaf (relativeSpecSymmetricAlgebraHomEquiv_comp_relativeSpec_map);
• TauCeti.AlgebraicGeometry.relativeSpecHomIso_hom_app_app_eq_symmetricAlgebraLift: the algebra map Sym F ⟶ q_* 𝒪_T pulling back regular functions along a point extends its module map;
• TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomIso: the same bijection as a natural isomorphism of functors of points;
• TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv: morphisms T ⟶ Spec_X (Sym F) over X are linear functionals q^* F ⟶ 𝒪_T, with naturality in the scheme (relativeSpecSymmetricAlgebraPullbackHomEquiv_comp) and in the sheaf (relativeSpecSymmetricAlgebraPullbackHomEquiv_comp_relativeSpec_map);
• TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraBaseChangeIso: base change of Spec_X (Sym F), naturally in F.
• TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackFst: the projection Spec_Y (Sym (f^* F)) ⟶ Spec_X (Sym F), with its action on module maps (relativeSpecSymmetricAlgebraHomEquiv_map_comp_relativeSpecSymmetricAlgebraPullbackFst) and on linear functionals (relativeSpecSymmetricAlgebraPullbackHomEquiv_map_comp_relativeSpecSymmetricAlgebraPullbackFst).

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.relativeSpecSymmetricAlgebraHomEquiv {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) : (T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) ≃ (F.obj ⟶ (AlgebraicGeometry.Scheme.Modules.pushforward T.hom).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules))

The universal property of the relative spectrum of a symmetric algebra. For a quasicoherent sheaf F on X and a scheme q : T ⟶ X over X, morphisms T ⟶ Spec_X (Sym F) over X correspond to morphisms of 𝒪_X-modules F ⟶ q_* 𝒪_T.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv_apply {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraHomEquiv F T) t = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) ((((symmetricAlgebra X).obj F).obj.relativeSpecHomEquiv T.hom) ⟨CategoryTheory.Over.Hom.left t, ⋯⟩).hom.hom

The module map F ⟶ q_* 𝒪_T of a morphism t : T ⟶ Spec_X (Sym F) over X is the restriction to F of its pullback of regular functions Sym F ⟶ q_* 𝒪_T.

theorem TauCeti.AlgebraicGeometry.relativeSpecHomIso_hom_app_app_eq_symmetricAlgebraLift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {T : CategoryTheory.Over X} (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (CategoryTheory.ConcreteCategory.hom (((relativeSpecHomIso X).hom.app (Opposite.op ((symmetricAlgebra X).obj F))).app (Opposite.op T))) t = symmetricAlgebraLift ((relativeSpecSymmetricAlgebraHomEquiv F T) t)

The algebra map Sym F ⟶ q_* 𝒪_T of a point t : T ⟶ Spec_X (Sym F) over X, by which regular functions are pulled back along t, is the algebra map extending the module map F ⟶ q_* 𝒪_T of t.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv_symm_apply_left {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) (φ : F.obj ⟶ (AlgebraicGeometry.Scheme.Modules.pushforward T.hom).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules)) : CategoryTheory.Over.Hom.left ((relativeSpecSymmetricAlgebraHomEquiv F T).symm φ) = CategoryTheory.CommMon.relativeSpecLift (symmetricAlgebraLift φ)

The morphism over X of a module map φ : F ⟶ q_* 𝒪_T is the relative-spectrum lift of the algebra map Sym F ⟶ q_* 𝒪_T extending φ.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv_comp {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) {T' T : CategoryTheory.Over X} (g : T' ⟶ T) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraHomEquiv F T') (CategoryTheory.CategoryStruct.comp g t) = CategoryTheory.CategoryStruct.comp ((relativeSpecSymmetricAlgebraHomEquiv F T) t) (AlgebraicGeometry.Scheme.Hom.pushforwardStructureAlgebraMap (CategoryTheory.Over.Hom.left g) ⋯).hom.hom

The bijection relativeSpecSymmetricAlgebraHomEquiv is natural in the scheme over X: composing with g : T' ⟶ T over X corresponds to composing the module map F ⟶ q_* 𝒪_T with pullback of regular functions along g.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv_comp_relativeSpec_map {X : AlgebraicGeometry.Scheme} {F' F : QuasicoherentSheaf X} (a : F' ⟶ F) (T : CategoryTheory.Over X) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraHomEquiv F' T) (CategoryTheory.CategoryStruct.comp t ((CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).map ((relativeSpec X).map ((symmetricAlgebra X).map a).op))) = CategoryTheory.CategoryStruct.comp a.hom ((relativeSpecSymmetricAlgebraHomEquiv F T) t)

The bijection relativeSpecSymmetricAlgebraHomEquiv is natural in the quasicoherent sheaf: composing with the relative-spectrum map of Sym a for a : F' ⟶ F corresponds to precomposing the module map with a.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomIso (X : AlgebraicGeometry.Scheme) : (symmetricAlgebra X).op.comp ((relativeSpec X).comp ((CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).comp CategoryTheory.yoneda)) ≅ (SheafOfModules.isQuasicoherent X.ringCatSheaf).ι.op.comp (CategoryTheory.coyoneda.comp ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Over X)ᵒᵖ (SheafOfModules X.ringCatSheaf) (Type u)).obj ((overFunctions X).comp (CategoryTheory.CommMon.forget X.Modules))))

The functor-of-points universal property of Spec_X (Sym F), natural in the quasicoherent sheaf F and in the scheme T over X: morphisms T ⟶ Spec_X (Sym F) over X correspond to morphisms of 𝒪_X-modules F ⟶ q_* 𝒪_T. Its components are relativeSpecSymmetricAlgebraHomEquiv.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomIso_hom_app_app {X : AlgebraicGeometry.Scheme} (F : (QuasicoherentSheaf X)ᵒᵖ) (T : (CategoryTheory.Over X)ᵒᵖ) (t : Opposite.unop T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj (Opposite.unop F))))) : (CategoryTheory.ConcreteCategory.hom (((relativeSpecSymmetricAlgebraHomIso X).hom.app F).app T)) t = (relativeSpecSymmetricAlgebraHomEquiv (Opposite.unop F) (Opposite.unop T)) t

The components of relativeSpecSymmetricAlgebraHomIso are relativeSpecSymmetricAlgebraHomEquiv.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomIso_inv_app_app {X : AlgebraicGeometry.Scheme} (F : (QuasicoherentSheaf X)ᵒᵖ) (T : (CategoryTheory.Over X)ᵒᵖ) (φ : (Opposite.unop F).obj ⟶ (AlgebraicGeometry.Scheme.Modules.pushforward (Opposite.unop T).hom).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Opposite.unop T).left.Modules)) : (CategoryTheory.ConcreteCategory.hom (((relativeSpecSymmetricAlgebraHomIso X).inv.app F).app T)) φ = (relativeSpecSymmetricAlgebraHomEquiv (Opposite.unop F) (Opposite.unop T)).symm φ

The inverse components of relativeSpecSymmetricAlgebraHomIso are the inverse of relativeSpecSymmetricAlgebraHomEquiv.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) : (T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) ≃ ((AlgebraicGeometry.Scheme.Modules.pullback T.hom).obj F.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules)

Spec_X (Sym F) represents linear functionals. For a quasicoherent sheaf F on X and a scheme q : T ⟶ X over X, morphisms T ⟶ Spec_X (Sym F) over X correspond to morphisms of 𝒪_T-modules q^* F ⟶ 𝒪_T. It is relativeSpecSymmetricAlgebraHomEquiv followed by the adjunction between pullback and pushforward of modules.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv_apply {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraPullbackHomEquiv F T) t = ((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction T.hom).homEquiv F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules)).symm ((relativeSpecSymmetricAlgebraHomEquiv F T) t)

The linear functional q^* F ⟶ 𝒪_T of a morphism T ⟶ Spec_X (Sym F) over X is the transpose of its module map F ⟶ q_* 𝒪_T.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv_symm_apply {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (T : CategoryTheory.Over X) (φ : (AlgebraicGeometry.Scheme.Modules.pullback T.hom).obj F.obj ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules) : (relativeSpecSymmetricAlgebraPullbackHomEquiv F T).symm φ = (relativeSpecSymmetricAlgebraHomEquiv F T).symm (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction T.hom).homEquiv F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules)) φ)

The morphism over X of a linear functional q^* F ⟶ 𝒪_T is the morphism of its transpose F ⟶ q_* 𝒪_T.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv_comp_relativeSpec_map {X : AlgebraicGeometry.Scheme} {F' F : QuasicoherentSheaf X} (a : F' ⟶ F) (T : CategoryTheory.Over X) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraPullbackHomEquiv F' T) (CategoryTheory.CategoryStruct.comp t ((CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).map ((relativeSpec X).map ((symmetricAlgebra X).map a).op))) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback T.hom).map a.hom) ((relativeSpecSymmetricAlgebraPullbackHomEquiv F T) t)

The linear-functional form of the universal property is natural in the quasicoherent sheaf: composing with the relative-spectrum map of Sym a for a : F' ⟶ F corresponds to precomposing the linear functional with q^* a.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv_comp {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) {T' T : CategoryTheory.Over X} (g : T' ⟶ T) (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))) : (relativeSpecSymmetricAlgebraPullbackHomEquiv F T') (CategoryTheory.CategoryStruct.comp g t) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackCongr ⋯).inv.app F.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.Over.Hom.left g) T.hom).inv.app F.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (CategoryTheory.Over.Hom.left g)).map ((relativeSpecSymmetricAlgebraPullbackHomEquiv F T) t)) (AlgebraicGeometry.Scheme.Modules.pullbackObjUnitIso (CategoryTheory.Over.Hom.left g)).hom))

The linear-functional form of the universal property is natural in the scheme over X: composing with g : T' ⟶ T over X corresponds to pulling the linear functional q^* F ⟶ 𝒪_T back along g, through the identifications q'^* F ≅ g^* q^* F (the composition isomorphism of pullback, as q' = g ≫ q) and g^* 𝒪_T ≅ 𝒪_{T'}.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraBaseChangeIso {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) : (QuasicoherentSheaf.pullback f).op.comp ((symmetricAlgebra Y).op.comp (relativeSpec Y)) ≅ (symmetricAlgebra X).op.comp ((relativeSpec X).comp (baseChangeAffineSchemeOver f))

Base change of the relative spectrum of a symmetric algebra. For a morphism of schemes f : Y ⟶ X and a quasicoherent sheaf F on X, the relative spectrum Spec_Y (Sym (f^* F)) is the base change Y ×_X Spec_X (Sym F), as affine schemes over Y and naturally in F. It is relative Spec of the identification f^* (Sym F) ≅ Sym (f^* F) (pullbackSymmetricAlgebraIso), followed by the base-change isomorphism relativeSpecBaseChangeIso of relative Spec.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraBaseChangeIso_hom_app {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : (QuasicoherentSheaf X)ᵒᵖ) : (relativeSpecSymmetricAlgebraBaseChangeIso f).hom.app F = CategoryTheory.CategoryStruct.comp ((relativeSpec Y).map (pullbackSymmetricAlgebraIso f (Opposite.unop F)).hom.op) ((relativeSpecBaseChangeIso f).hom.app (Opposite.op ((symmetricAlgebra X).obj (Opposite.unop F))))

The component of relativeSpecSymmetricAlgebraBaseChangeIso at F is relative Spec of pullbackSymmetricAlgebraIso, followed by the component of relativeSpecBaseChangeIso at Sym F.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraBaseChangeIso_inv_app {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : (QuasicoherentSheaf X)ᵒᵖ) : (relativeSpecSymmetricAlgebraBaseChangeIso f).inv.app F = CategoryTheory.CategoryStruct.comp ((relativeSpecBaseChangeIso f).inv.app (Opposite.op ((symmetricAlgebra X).obj (Opposite.unop F)))) ((relativeSpec Y).map (pullbackSymmetricAlgebraIso f (Opposite.unop F)).inv.op)

The inverse component of relativeSpecSymmetricAlgebraBaseChangeIso at F is the inverse component of relativeSpecBaseChangeIso at Sym F, followed by relative Spec of the inverse of pullbackSymmetricAlgebraIso.

noncomputable def TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackFst {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : QuasicoherentSheaf X) : (CategoryTheory.Over.map f).obj ((CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ Y).obj ((relativeSpec Y).obj (Opposite.op ((symmetricAlgebra Y).obj ((QuasicoherentSheaf.pullback f).obj F))))) ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ X).obj ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F)))

The projection Spec_Y (Sym (f^* F)) ⟶ Spec_X (Sym F) from the base change, as a morphism of schemes over X: relative Spec of pullbackSymmetricAlgebraIso, followed by the projection relativeSpecPullbackFst of base change of relative Spec. Under relativeSpecSymmetricAlgebraBaseChangeIso it is the first projection of the fibre product Y ×_X Spec_X (Sym F) (relativeSpecSymmetricAlgebraBaseChangeIso_hom_app_left_fst).

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackFst_left {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : QuasicoherentSheaf X) : CategoryTheory.Over.Hom.left (relativeSpecSymmetricAlgebraPullbackFst f F) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CommMon.relativeSpecMap (pullbackSymmetricAlgebraIso f F).hom.hom) (relativeSpecPullbackFst ((symmetricAlgebra X).obj F) f)

The underlying morphism of relativeSpecSymmetricAlgebraPullbackFst is relative Spec of pullbackSymmetricAlgebraIso followed by relativeSpecPullbackFst.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraBaseChangeIso_hom_app_left_fst {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : QuasicoherentSheaf X) : CategoryTheory.CategoryStruct.comp ((relativeSpecSymmetricAlgebraBaseChangeIso f).hom.app (Opposite.op F)).left (CategoryTheory.Limits.pullback.fst ((relativeSpec X).obj (Opposite.op ((symmetricAlgebra X).obj F))).hom f) = CategoryTheory.Over.Hom.left (relativeSpecSymmetricAlgebraPullbackFst f F)

The isomorphism relativeSpecSymmetricAlgebraBaseChangeIso followed by the first projection of the fibre product Y ×_X Spec_X (Sym F) is the projection relativeSpecSymmetricAlgebraPullbackFst.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraHomEquiv_map_comp_relativeSpecSymmetricAlgebraPullbackFst {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : QuasicoherentSheaf X) {T : CategoryTheory.Over Y} (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ Y).obj ((relativeSpec Y).obj (Opposite.op ((symmetricAlgebra Y).obj ((QuasicoherentSheaf.pullback f).obj F))))) : (relativeSpecSymmetricAlgebraHomEquiv F ((CategoryTheory.Over.map f).obj T)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.map f).map t) (relativeSpecSymmetricAlgebraPullbackFst f F)) = CategoryTheory.CategoryStruct.comp (((AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f).homEquiv F.obj ((AlgebraicGeometry.Scheme.Modules.pushforward T.hom).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((relativeSpecSymmetricAlgebraHomEquiv ((QuasicoherentSheaf.pullback f).obj F) T) t))) ((AlgebraicGeometry.Scheme.Modules.pushforwardComp T.hom f).hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit T.left.Modules))

Base change of Spec_X (Sym F) on points, as module maps. For a scheme q : T ⟶ Y over Y and a morphism t : T ⟶ Spec_Y (Sym (f^* F)) over Y, the module map F ⟶ (q ≫ f)_* 𝒪_T of the composite of t with the projection to Spec_X (Sym F) is the transpose along f of the module map f^* F ⟶ q_* 𝒪_T of t, followed by the identification f_* q_* ≅ (q ≫ f)_*.

theorem TauCeti.AlgebraicGeometry.relativeSpecSymmetricAlgebraPullbackHomEquiv_map_comp_relativeSpecSymmetricAlgebraPullbackFst {X Y : AlgebraicGeometry.Scheme} (f : Y ⟶ X) (F : QuasicoherentSheaf X) {T : CategoryTheory.Over Y} (t : T ⟶ (CategoryTheory.MorphismProperty.Over.forget @AlgebraicGeometry.IsAffineHom ⊤ Y).obj ((relativeSpec Y).obj (Opposite.op ((symmetricAlgebra Y).obj ((QuasicoherentSheaf.pullback f).obj F))))) : (relativeSpecSymmetricAlgebraPullbackHomEquiv F ((CategoryTheory.Over.map f).obj T)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.map f).map t) (relativeSpecSymmetricAlgebraPullbackFst f F)) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackComp T.hom f).inv.app F.obj) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback T.hom).map (CategoryTheory.eqToHom ⋯)) ((relativeSpecSymmetricAlgebraPullbackHomEquiv ((QuasicoherentSheaf.pullback f).obj F) T) t))

Base change of Spec_X (Sym F) on points, as linear functionals. For a scheme q : T ⟶ Y over Y and a morphism t : T ⟶ Spec_Y (Sym (f^* F)) over Y, the linear functional (q ≫ f)^* F ⟶ 𝒪_T of the composite of t with the projection to Spec_X (Sym F) is the linear functional q^* f^* F ⟶ 𝒪_T of t, through the composition isomorphism of pullback.