Exterior powers and restriction of scalars

Restriction of scalars has a natural exterior-power comparison, sending a wedge over the source ring to the same wedge over the target ring. It is an isomorphism when the coefficient map is bijective, though not for an arbitrary ring map. This gives exterior-power restriction isomorphisms for module presheaves with isomorphic coefficient maps, and for module sheaves when the coefficient map is an isomorphism and the site functor is also cocontinuous. The construction uses Mathlib's ModuleCat.exteriorPower.desc and supplies the sectionwise maps for exterior powers of pushforwards of module presheaves.

noncomputable def TauCeti.ModuleCat.restrictScalarsExteriorPowerComparison {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (n : ℕ) : (ModuleCat.restrictScalars f).comp (ModuleCat.exteriorPower.functor S n) ⟶ (ModuleCat.exteriorPower.functor R n).comp (ModuleCat.restrictScalars f)

Restriction of scalars carries the natural exterior-power comparison, changing the coefficient ring of a wedge without changing its factors.

@[simp]

theorem TauCeti.ModuleCat.restrictScalarsExteriorPowerComparison_app_mk {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (n : ℕ) (M : ModuleCat R) (m : Fin n → ↑((ModuleCat.restrictScalars f).obj M)) : (CategoryTheory.ConcreteCategory.hom ((restrictScalarsExteriorPowerComparison f n).app M)) (ModuleCat.exteriorPower.mk m) = ModuleCat.exteriorPower.mk m

The restriction-of-scalars comparison preserves the factors of a decomposable wedge.

theorem TauCeti.ModuleCat.isIso_restrictScalarsExteriorPowerComparison_app_of_bijective {S : Type u} {R : Type v} [CommRing S] [CommRing R] (f : S →+* R) (hf : Function.Bijective ⇑f) (n : ℕ) (M : ModuleCat R) : CategoryTheory.IsIso ((restrictScalarsExteriorPowerComparison f n).app M)

Restriction along an isomorphism of coefficient rings preserves exterior powers.