Base change of exterior algebra

In this file, we proved that Exterior algebra behaves well with respect to base change.

Main Results

• ExteriorAlgebra.baseChangeEquiv: for R-algebra S, the base change isomorphism S ⊗[R] (⋀[R]^i M) ≃ₗ[S] ⋀[S]^i (S ⊗[R] M)

def ExteriorAlgebra.baseChangeEquiv (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (S : Type u_3) [CommRing S] [Algebra R S] : TensorProduct R S (ExteriorAlgebra R M) ≃ₐ[S] ExteriorAlgebra S (TensorProduct R S M)

Exterior algebra behaves well with respect to base change.

Equations

• One or more equations did not get rendered due to their size.

theorem ExteriorAlgebra.baseChangeEquiv_apply (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (S : Type u_3) [CommRing S] [Algebra R S] (s : S) (m : M) : (baseChangeEquiv R M S) (s ⊗ₜ[R] (ι R) m) = (ι S) (s ⊗ₜ[R] m)

theorem ExteriorAlgebra.baseChangeEquiv_symm_apply (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] (S : Type u_3) [CommRing S] [Algebra R S] (s : S) (m : M) : (baseChangeEquiv R M S).symm ((ι S) (s ⊗ₜ[R] m)) = s ⊗ₜ[R] (ι R) m