Extension of scalars and exterior powers

Exterior powers commute with extension of scalars along an arbitrary map of commutative rings. This file packages TauCeti.exteriorPower.equivBaseChange as a natural isomorphism of module functors. Its forward map sends a scalar tensored with a wedge to the scalar multiple of the wedge of the base-changed vectors. This is the module calculation for pullback of exterior powers of quasicoherent sheaves on affine schemes.

References

• The Stacks Project, Lemma 10.13.6 (Tag 0C6F).

noncomputable def TauCeti.extendScalarsExteriorPowerIso {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (ModuleCat.extendScalars f).obj (M.exteriorPower n) ≅ ((ModuleCat.extendScalars f).obj M).exteriorPower n

Exterior powers commute with extension of scalars, without a flatness or finiteness assumption.

@[simp]

theorem TauCeti.extendScalarsExteriorPowerIso_hom_tmul_mk {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) (s : S) (m : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom (extendScalarsExteriorPowerIso f n M).hom) (s ⊗ₜ[R] ModuleCat.exteriorPower.mk m) = s • ModuleCat.exteriorPower.mk fun (i : Fin n) => 1 ⊗ₜ[R] m i

The forward comparison on a pure tensor with a decomposable wedge.

@[simp]

theorem TauCeti.extendScalarsExteriorPowerIso_inv_mk_tmul {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) (s : Fin n → S) (m : Fin n → ↑M) : (CategoryTheory.ConcreteCategory.hom (extendScalarsExteriorPowerIso f n M).inv) (ModuleCat.exteriorPower.mk fun (i : Fin n) => s i ⊗ₜ[R] m i) = (∏ i : Fin n, s i) ⊗ₜ[R] ModuleCat.exteriorPower.mk m

The inverse comparison on a wedge of pure tensors.

theorem TauCeti.extendScalarsExteriorPowerIso_hom_naturality {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) {M N : ModuleCat R} (g : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f).map (ModuleCat.exteriorPower.map g n)) (extendScalarsExteriorPowerIso f n N).hom = CategoryTheory.CategoryStruct.comp (extendScalarsExteriorPowerIso f n M).hom (ModuleCat.exteriorPower.map ((ModuleCat.extendScalars f).map g) n)

The scalar-extension comparison is natural in the module.

theorem TauCeti.extendScalarsExteriorPowerIso_hom_naturality_assoc {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) {M N : ModuleCat R} (g : M ⟶ N) {Z : ModuleCat S} (h : ((ModuleCat.extendScalars f).obj N).exteriorPower n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((ModuleCat.extendScalars f).map (ModuleCat.exteriorPower.map g n)) (CategoryTheory.CategoryStruct.comp (extendScalarsExteriorPowerIso f n N).hom h) = CategoryTheory.CategoryStruct.comp (extendScalarsExteriorPowerIso f n M).hom (CategoryTheory.CategoryStruct.comp (ModuleCat.exteriorPower.map ((ModuleCat.extendScalars f).map g) n) h)

The scalar-extension comparison is natural in the module.

noncomputable def TauCeti.extendScalarsExteriorPowerNatIso {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) : (ModuleCat.exteriorPower.functor R n).comp (ModuleCat.extendScalars f) ≅ (ModuleCat.extendScalars f).comp (ModuleCat.exteriorPower.functor S n)

The natural scalar-extension comparison for the n-th exterior power.

@[simp]

theorem TauCeti.extendScalarsExteriorPowerNatIso_hom_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (extendScalarsExteriorPowerNatIso f n).hom.app M = (extendScalarsExteriorPowerIso f n M).hom

The forward components of the natural scalar-extension comparison.

@[simp]

theorem TauCeti.extendScalarsExteriorPowerNatIso_inv_app {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ) (M : ModuleCat R) : (extendScalarsExteriorPowerNatIso f n).inv.app M = (extendScalarsExteriorPowerIso f n M).inv

The inverse components of the natural scalar-extension comparison.