Affine comparison for symmetric powers

Symmetric powers of quasicoherent modules on a spectrum are computed by symmetric powers of modules. The comparison sends a product of module elements to the sheafified product of their associated global sections.

References

• The Stacks Project, Lemma 10.13.6.
• R. Hartshorne, Algebraic Geometry, Proposition II.5.2.

noncomputable def TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) : AlgebraicGeometry.tilde (M.symmetricPower n) ≅ (SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).obj (AlgebraicGeometry.tilde M)

Symmetric powers commute with the affine tilde construction over arbitrary commutative rings and modules. No finite-generation, freeness or flatness assumption is needed.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_inv_toOpen_prod {R : CommRingCat} (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens) (l : List ↑M) : (CategoryTheory.ConcreteCategory.hom ((tildeSymmetricPowerIso l.length M).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso l.length (AlgebraicGeometry.tilde M)).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R).ringCatSheaf.obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower l.length).obj (AlgebraicGeometry.tilde M).val)).app (Opposite.op U))) ⟨(List.map (fun (m : ↑M) => (SymmetricAlgebra.ι ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op U)) ↑(PresheafOfModulesOfCommRing.obj (AlgebraicGeometry.tilde M).val (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M U)) m)) l).prod, ⋯⟩)) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen (M.symmetricPower l.length) U)) ⟨(List.map (⇑(SymmetricAlgebra.ι ↑R ↑M)) l).prod, ⋯⟩

On every open, the inverse affine comparison sends a sheafified monomial in associated sections to the associated section of the same monomial. The empty list includes degree zero.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_hom_toOpen_prod {R : CommRingCat} (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens) (l : List ↑M) : (CategoryTheory.ConcreteCategory.hom ((tildeSymmetricPowerIso l.length M).hom.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen (M.symmetricPower l.length) U)) ⟨(List.map (⇑(SymmetricAlgebra.ι ↑R ↑M)) l).prod, ⋯⟩) = (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso l.length (AlgebraicGeometry.tilde M)).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R).ringCatSheaf.obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower l.length).obj (AlgebraicGeometry.tilde M).val)).app (Opposite.op U))) ⟨(List.map (fun (m : ↑M) => (SymmetricAlgebra.ι ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op U)) ↑(PresheafOfModulesOfCommRing.obj (AlgebraicGeometry.tilde M).val (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M U)) m)) l).prod, ⋯⟩)

On every open, the affine comparison sends the associated section of a monomial to the sheafified monomial in its associated sections.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_inv_naturality {R : CommRingCat} (n : ℕ) {M N : ModuleCat ↑R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).map (AlgebraicGeometry.tilde.map φ)) (tildeSymmetricPowerIso n N).inv = CategoryTheory.CategoryStruct.comp (tildeSymmetricPowerIso n M).inv (AlgebraicGeometry.tilde.map (ModuleCat.symmetricPower.map φ n))

The inverse affine symmetric-power comparison is natural in the module.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_inv_naturality_assoc {R : CommRingCat} (n : ℕ) {M N : ModuleCat ↑R} (φ : M ⟶ N) {Z : SheafOfModules (SheafOfModules.ringCatSheaf (AlgebraicGeometry.Spec R).sheaf)} (h : AlgebraicGeometry.tilde (N.symmetricPower n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).map (AlgebraicGeometry.tilde.map φ)) (tildeSymmetricPowerIso n N).inv) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (tildeSymmetricPowerIso n M).inv (AlgebraicGeometry.tilde.map (ModuleCat.symmetricPower.map φ n))) h

The inverse affine symmetric-power comparison is natural in the module.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_hom_naturality {R : CommRingCat} (n : ℕ) {M N : ModuleCat ↑R} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (ModuleCat.symmetricPower.map φ n)) (tildeSymmetricPowerIso n N).hom = CategoryTheory.CategoryStruct.comp (tildeSymmetricPowerIso n M).hom ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).map (AlgebraicGeometry.tilde.map φ))

The affine symmetric-power comparison is natural in the module.

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerIso_hom_naturality_assoc {R : CommRingCat} (n : ℕ) {M N : ModuleCat ↑R} (φ : M ⟶ N) {Z : (AlgebraicGeometry.Spec R).Modules} (h : (SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).obj (AlgebraicGeometry.tilde N) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (ModuleCat.symmetricPower.map φ n)) (tildeSymmetricPowerIso n N).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (tildeSymmetricPowerIso n M).hom ((SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n).map (AlgebraicGeometry.tilde.map φ))) h

The affine symmetric-power comparison is natural in the module.

noncomputable def TauCeti.AlgebraicGeometry.tildeSymmetricPowerNatIso {R : CommRingCat} (n : ℕ) : (ModuleCat.symmetricPower.functor (↑R) n).comp (AlgebraicGeometry.tilde.functor R) ≅ (AlgebraicGeometry.tilde.functor R).comp (SheafOfModules.symmetricPower (AlgebraicGeometry.Spec R).sheaf n)

The affine symmetric-power comparisons form a natural isomorphism between taking the symmetric power before and after associating a sheaf to a module.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerNatIso_hom_app {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) : (tildeSymmetricPowerNatIso n).hom.app M = (tildeSymmetricPowerIso n M).hom

The forward components of the natural affine comparison.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeSymmetricPowerNatIso_inv_app {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) : (tildeSymmetricPowerNatIso n).inv.app M = (tildeSymmetricPowerIso n M).inv

The inverse components of the natural affine comparison.