Documentation

TauCeti.LinearAlgebra.ExteriorPower.BaseChange

Scalar extension of exterior powers #

For every commutative R-algebra A, the comparison identifies ⋀[A]^n (A ⊗[R] M) with A ⊗[R] (⋀[R]^n M). It is natural in M and sends a wedge of pure tensors to the product of their coefficients tensored with the original wedge. No flatness or freeness assumption is needed: the grading splits the inclusion of each exterior power into the exterior algebra before scalar extension.

These comparisons allow exterior powers of algebraic-group representations to be evaluated on arbitrary value algebras, and identify scalar extensions of their exterior lines.

source
@[simp]
theorem TauCeti.exteriorAlgebraEquivBaseChange_map_exteriorPower {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) :
Submodule.map (exteriorAlgebraEquivBaseChange A).toLinearMap (⋀[A]^n (TensorProduct R A M)) = Submodule.baseChange A (⋀[R]^n M)

The exterior-algebra comparison preserves each homogeneous degree.

source
theorem TauCeti.exteriorPower.baseChange_subtype_injective {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) :
Function.Injective ⇑(LinearMap.baseChange A (⋀[R]^n M).subtype)

Scalar extension of the inclusion of a homogeneous exterior power into the exterior algebra remains injective, because the grading splits the inclusion.

source
noncomputable def TauCeti.exteriorPower.equivBaseChange {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) :
↥(⋀[A]^n (TensorProduct R A M)) ≃ₗ[A] TensorProduct R A ↥(⋀[R]^n M)

Exterior powers commute with extension of scalars over arbitrary commutative rings.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.exteriorPower.subtype_baseChange_equivBaseChange {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (n : ℕ) (x : ↥(⋀[A]^n (TensorProduct R A M))) :
    (LinearMap.baseChange A (⋀[R]^n M).subtype) ((equivBaseChange A n) x) = (exteriorAlgebraEquivBaseChange A) ↑x

    The exterior-power comparison is the restriction of the exterior-algebra comparison.

    source
    @[simp]
    theorem TauCeti.exteriorPower.equivBaseChange_ιMulti_tmul {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} (a : Fin n → A) (m : Fin n → M) :
    (equivBaseChange A n) ((exteriorPower.ιMulti A n) fun (i : Fin n) => a i ⊗ₜ[R] m i) = (∏ i : Fin n, a i) ⊗ₜ[R] (exteriorPower.ιMulti R n) m

    A wedge of pure tensors corresponds to the product of the scalars tensored with the wedge.

    source
    @[simp]
    theorem TauCeti.exteriorPower.equivBaseChange_symm_tmul_ιMulti {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] {n : ℕ} (a : A) (m : Fin n → M) :
    (equivBaseChange A n).symm (a ⊗ₜ[R] (exteriorPower.ιMulti R n) m) = a • (exteriorPower.ιMulti A n) fun (i : Fin n) => 1 ⊗ₜ[R] m i

    The inverse comparison on the spanning pure tensors.

    source
    @[simp]
    theorem TauCeti.exteriorPower.equivBaseChange_map {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] (n : ℕ) (f : M →ₗ[R] N) (x : ↥(⋀[A]^n (TensorProduct R A M))) :
    (equivBaseChange A n) ((exteriorPower.map n (LinearMap.baseChange A f)) x) = (LinearMap.baseChange A (exteriorPower.map n f)) ((equivBaseChange A n) x)

    The exterior-power comparison intertwines the maps induced by any linear map.