Documentation

TauCeti.LinearAlgebra.ExteriorAlgebra.BaseChange

Scalar extension of exterior algebras #

The exterior algebra commutes with extension of scalars over arbitrary commutative rings, including in characteristic two. The inverse comparison sends a ⊗ ι(m) to ι(a ⊗ m). This supplies the ambient algebra comparison for scalar extension of exterior powers.

The construction follows Mathlib's CliffordAlgebra.equivBaseChange (Eric Wieser), but uses the alternating relations directly: unlike the Clifford-algebra comparison, it does not require that two be invertible. No flatness or freeness assumption is needed.

source
noncomputable def TauCeti.exteriorAlgebraEquivBaseChange {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] :
ExteriorAlgebra A (TensorProduct R A M) ≃ₐ[A] TensorProduct R A (ExteriorAlgebra R M)

Scalar extension commutes with exterior algebras, without restrictions on characteristic.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.exteriorAlgebraEquivBaseChange_ι {R : Type u_1} (A : Type u_2) {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] (x : TensorProduct R A M) :
    (exteriorAlgebraEquivBaseChange A) ((ExteriorAlgebra.ι A) x) = (LinearMap.baseChange A (ExteriorAlgebra.ι R)) x

    The comparison carries an exterior generator to the scalar extension of that generator.

    source
    @[simp]
    theorem TauCeti.exteriorAlgebraEquivBaseChange_symm_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] (a : A) (m : M) :
    (exteriorAlgebraEquivBaseChange A).symm (a ⊗ₜ[R] (ExteriorAlgebra.ι R) m) = (ExteriorAlgebra.ι A) (a ⊗ₜ[R] m)

    The inverse comparison on a scalar multiple of an exterior generator.

    source
    @[simp]
    theorem TauCeti.exteriorAlgebraEquivBaseChange_ι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) :
    (exteriorAlgebraEquivBaseChange A) ((ExteriorAlgebra.ιMulti A n) fun (i : Fin n) => a i ⊗ₜ[R] m i) = (∏ i : Fin n, a i) ⊗ₜ[R] (ExteriorAlgebra.ιMulti R n) m

    On wedges of pure tensors the scalar coefficients multiply.

    source
    @[simp]
    theorem TauCeti.exteriorAlgebraEquivBaseChange_map {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 : Type u_4} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (x : ExteriorAlgebra A (TensorProduct R A M)) :
    (exteriorAlgebraEquivBaseChange A) ((ExteriorAlgebra.map (LinearMap.baseChange A f)) x) = (Algebra.TensorProduct.map (AlgHom.id A A) (ExteriorAlgebra.map f)) ((exteriorAlgebraEquivBaseChange A) x)

    Scalar extension of exterior algebras is natural in the module.