The canonical exterior-power comparison on affine spectra

For an arbitrary ring map φ : R ⟶ S, the canonical comparison (Spec φ)^* (⋀ⁿ M) ⟶ ⋀ⁿ ((Spec φ)^* M) is invertible for every quasicoherent module sheaf M on Spec R. There are no flatness, finite-presentation or local-freeness hypotheses.

The comparison is the mate of the pushforward map on sheafified wedges, not a separately chosen isomorphism. We identify it with tildePullbackExteriorPowerIso, obtained from the scalar-extension isomorphism for modules. The identification follows by evaluating the pullback and tilde adjunctions on decomposable wedges. It supplies the affine computation needed to check invertibility of the canonical comparison locally on schemes.

References

• The Stacks Project, Lemma 10.13.6 (Tag 0C6F).
• R. Hartshorne, Algebraic Geometry, Proposition II.5.2(e).

theorem TauCeti.AlgebraicGeometry.pullback_tildeExteriorPowerIso_hom {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeExteriorPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M)) ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).hom.app M))) = CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.exteriorPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (extendScalarsExteriorPowerIso (CommRingCat.Hom.hom φ) n M).hom) (tildeExteriorPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom)

Under the affine tilde and pullback comparisons, the canonical exterior-power pullback map is the scalar-extension map for exterior powers.

theorem TauCeti.AlgebraicGeometry.pullback_tildeExteriorPowerIso_hom_assoc {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) {Z : (AlgebraicGeometry.Spec S).Modules} (h : (SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).obj ((AlgebraicGeometry.tilde.functor S).obj ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).map (tildeExteriorPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M)) ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).map ((tildeFunctorCompPullbackIso φ).hom.app M)))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((tildeFunctorCompPullbackIso φ).hom.app (M.exteriorPower n)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.map (extendScalarsExteriorPowerIso (CommRingCat.Hom.hom φ) n M).hom) (tildeExteriorPowerIso n ((ModuleCat.extendScalars (CommRingCat.Hom.hom φ)).obj M)).hom)) h

Under the affine tilde and pullback comparisons, the canonical exterior-power pullback map is the scalar-extension map for exterior powers.

theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerComparison_tilde {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : ModuleCat ↑R) : (AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (AlgebraicGeometry.Spec.map φ) n).app (AlgebraicGeometry.tilde M) = (tildePullbackExteriorPowerIso φ n).hom.app M

The canonical exterior-power pullback map on an associated sheaf is exactly the forward map of the affine scalar-extension isomorphism.

instance TauCeti.AlgebraicGeometry.isIso_pullbackExteriorPowerComparison_of_spec {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : CategoryTheory.IsIso ((AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (AlgebraicGeometry.Spec.map φ) n).app M)

The canonical exterior-power pullback comparison is invertible for every quasicoherent sheaf on an affine spectrum and every ring map, including nonflat maps.

noncomputable def TauCeti.AlgebraicGeometry.pullbackExteriorPowerIsoOfSpec {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : (AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj ((SheafOfModules.exteriorPower (AlgebraicGeometry.Spec R).sheaf n).obj M) ≅ (SheafOfModules.exteriorPower (AlgebraicGeometry.Spec S).sheaf n).obj ((AlgebraicGeometry.Scheme.Modules.pullback (AlgebraicGeometry.Spec.map φ)).obj M)

Exterior powers commute with pullback of a quasicoherent sheaf along a ring map. The forward map is the canonical mate of the pushforward comparison on sheafified wedges.

@[simp]

theorem TauCeti.AlgebraicGeometry.pullbackExteriorPowerIsoOfSpec_hom {R S : CommRingCat} (φ : R ⟶ S) (n : ℕ) (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M] : (pullbackExteriorPowerIsoOfSpec φ n M).hom = (AlgebraicGeometry.Scheme.Modules.pullbackExteriorPowerComparison (AlgebraicGeometry.Spec.map φ) n).app M

The forward affine comparison is the canonical exterior-power pullback map.