Exterior powers of localized modules

If f : M →ₗ[R] N exhibits N as an extension of scalars to an R-algebra A, the exterior power of N is the scalar extension of the exterior power of M. The comparison sends a ⊗ (m₁ ∧ ⋯ ∧ mₙ) to a • (f m₁ ∧ ⋯ ∧ f mₙ) and is natural in maps commuting with f.

In particular, a map on exterior powers sending each wedge to the wedge of the images is a localization when f is a localization. This allows the sectionwise exterior power of a quasicoherent sheaf to be computed on basic affine opens.

The construction combines TauCeti.exteriorPower.equivBaseChange with Mathlib's IsBaseChange.equiv and IsLocalizedModule.isBaseChange.

References

• The Stacks Project, Lemma 10.13.6.

noncomputable def IsBaseChange.exteriorPowerEquiv {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) : TensorProduct R A ↥(⋀[R]^n M) ≃ₗ[A] ↥(⋀[A]^n N)

Exterior powers commute with a specified scalar extension.

@[simp]

theorem IsBaseChange.exteriorPowerEquiv_tmul_ιMulti {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) (a : A) (m : Fin n → M) : (h.exteriorPowerEquiv n) (a ⊗ₜ[R] (exteriorPower.ιMulti R n) m) = a • (exteriorPower.ιMulti A n) fun (i : Fin n) => f (m i)

The scalar-extension comparison sends a pure tensor of a wedge to the scaled wedge of the images.

@[simp]

theorem IsBaseChange.exteriorPowerEquiv_symm_ιMulti {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) (m : Fin n → M) : (h.exteriorPowerEquiv n).symm ((exteriorPower.ιMulti A n) fun (i : Fin n) => f (m i)) = 1 ⊗ₜ[R] (exteriorPower.ιMulti R n) m

The inverse comparison sends the wedge of the images to the tensor with coefficient one.

theorem IsBaseChange.exteriorPower {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (n : ℕ) : IsBaseChange A (↑R ↑(h.exteriorPowerEquiv n) ∘ₗ (TensorProduct.mk R A ↥(⋀[R]^n M)) 1)

The comparison map ⋀[R]^n M → ⋀[A]^n N, x ↦ h.exteriorPowerEquiv n (1 ⊗ x), which sends m₁ ∧ ⋯ ∧ mₙ to f m₁ ∧ ⋯ ∧ f mₙ, exhibits ⋀[A]^n N as the base change of ⋀[R]^n M to A.

theorem IsBaseChange.exteriorPowerEquiv_naturality {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {f : M →ₗ[R] N} {M' : Type u_5} {N' : Type u_6} [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] {f' : M' →ₗ[R] N'} (h : IsBaseChange A f) (h' : IsBaseChange A f') (n : ℕ) (g : M →ₗ[R] M') (g' : N →ₗ[A] N') (comm : ↑R g' ∘ₗ f = f' ∘ₗ g) : exteriorPower.map n g' ∘ₗ ↑(h.exteriorPowerEquiv n) = ↑(h'.exteriorPowerEquiv n) ∘ₗ LinearMap.baseChange A (exteriorPower.map n g)

The exterior-power scalar-extension comparison is natural in commuting maps of the original and extended modules.

theorem LinearMap.isLocalizedModule_exteriorPower {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) {S : Submonoid R} [IsLocalization S A] [IsLocalizedModule S f] (n : ℕ) [extR : Module R ↥(⋀[A]^n N)] [extTower : IsScalarTower R A ↥(⋀[A]^n N)] (g : ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[A]^n N)) (hg : ∀ (m : Fin n → M), g ((exteriorPower.ιMulti R n) m) = (exteriorPower.ιMulti A n) fun (i : Fin n) => f (m i)) : IsLocalizedModule S g

A map that sends wedges to the wedges of a localization map is itself a localization. The scalar structure on the exterior power is retained as a parameter so this also applies to restriction-of-scalars presentations of the target. Its tower uses the scalar action of that module explicitly: the actions inferred directly from the submodule carrier need not be the scalar projections of the caller's Module R instance.