Affine comparison for exterior powers

Exterior powers of quasicoherent modules on a spectrum are computed by exterior powers of modules. The comparison sends a wedge of module elements to the sheafified wedge of their associated global sections.

The affine computation uses the localization of exterior powers on basic opens and Mathlib's equivalence between morphisms into a sheaf and their restrictions to a basis. The local scalar-linearity argument adapts AlgebraicGeometry.SpecModulesToSheafFullyFaithful to a presheaf source.

References

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

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

Exterior 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.tildeExteriorPowerIso_inv_toOpen_mk {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens) (m : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom ((tildeExteriorPowerIso n M).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.exteriorPowerIso n (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.exteriorPower n).obj (AlgebraicGeometry.tilde M).val)).app (Opposite.op U))) (ModuleCat.exteriorPower.mk fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M U)) (m i)))) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen (M.exteriorPower n) U)) (ModuleCat.exteriorPower.mk m)

On sections over any open, the inverse affine comparison sends the sheafified wedge of the associated sections of m₁, …, mₙ to the associated section of their wedge. The sheafification unit is necessary: exterior-power sections are sheafified sections, rather than exterior powers of sections on arbitrary opens.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeExteriorPowerIso_hom_toOpen_mk {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opens) (m : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom ((tildeExteriorPowerIso n M).hom.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen (M.exteriorPower n) U)) (ModuleCat.exteriorPower.mk m)) = (CategoryTheory.ConcreteCategory.hom ((SheafOfModules.exteriorPowerIso n (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.exteriorPower n).obj (AlgebraicGeometry.tilde M).val)).app (Opposite.op U))) (ModuleCat.exteriorPower.mk fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M U)) (m i)))

The affine comparison sends the associated section of a wedge to the sheafified wedge of its associated sections, over every open.

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeExteriorPowerNatIso_hom_app {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) : (tildeExteriorPowerNatIso n).hom.app M = (tildeExteriorPowerIso n M).hom

The forward components of the natural affine comparison.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeExteriorPowerNatIso_inv_app {R : CommRingCat} (n : ℕ) (M : ModuleCat ↑R) : (tildeExteriorPowerNatIso n).inv.app M = (tildeExteriorPowerIso n M).inv

The inverse components of the natural affine comparison.