Exterior algebra of product module

In this file, we proved the equivelence between exterior algebra of product module and graded tensor product of the two exterior algebras.

noncomputable def ExteriorAlgebra.prodEquivTensorForward (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : ExteriorAlgebra R (M × N) →ₐ[R] GradedTensorProduct R (fun (i : ℕ) => ⋀[R]^i M) fun (i : ℕ) => ⋀[R]^i N

The forward function for the equivalence between ExteriorAlgebra R (M × N) and graded tensor product of the two exterior algebras, lift from (x, y) ↦ x ⊗ 1 + 1 ⊗ y.

Equations

• ExteriorAlgebra.prodEquivTensorForward R M N = (ExteriorAlgebra.lift R) ⟨ExteriorAlgebra.prodEquivTensorForwardAux✝ R M N, ⋯⟩

theorem ExteriorAlgebra.prodEquivTensorForward_ι_apply (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : M × N) : (prodEquivTensorForward R M N) ((ι R) m) = (ι R) m.1 ᵍ⊗ₜ[R] 1 + 1 ᵍ⊗ₜ[R] (ι R) m.2

theorem ExteriorAlgebra.map_inl_inr_anticomm (R : Type u) [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (i j : ℕ) (a : ↥(⋀[R]^i M)) (b : ↥(⋀[R]^j N)) : (map (LinearMap.inl R M N)) ↑a * (map (LinearMap.inr R M N)) ↑b = (-1) ^ (j * i) • ((map (LinearMap.inr R M N)) ↑b * (map (LinearMap.inl R M N)) ↑a)

noncomputable def ExteriorAlgebra.prodEquivTensorInverse (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : (GradedTensorProduct R (fun (i : ℕ) => ⋀[R]^i M) fun (i : ℕ) => ⋀[R]^i N) →ₐ[R] ExteriorAlgebra R (M × N)

The inverse function for the equivalence between ExteriorAlgebra R (M × N) and graded tensor product of the two exterior algebras, lift form universal property.

Equations

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

theorem ExteriorAlgebra.prodEquivTensorInverse_ι_tmul_one (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (m : M) : (prodEquivTensorInverse R M N) ((ι R) m ᵍ⊗ₜ[R] 1) = (ι R) (m, 0)

theorem ExteriorAlgebra.prodEquivTensorInverse_one_tmul_ι (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (n : N) : (prodEquivTensorInverse R M N) (1 ᵍ⊗ₜ[R] (ι R) n) = (ι R) (0, n)

theorem ExteriorAlgebra.prodEquivTensor_inverse_comp_forward (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : (prodEquivTensorInverse R M N).comp (prodEquivTensorForward R M N) = AlgHom.id R (ExteriorAlgebra R (M × N))

theorem ExteriorAlgebra.prodEquivTensor_forward_comp_inverse (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : (prodEquivTensorForward R M N).comp (prodEquivTensorInverse R M N) = AlgHom.id R (GradedTensorProduct R (fun (i : ℕ) => ⋀[R]^i M) fun (i : ℕ) => ⋀[R]^i N)

noncomputable def ExteriorAlgebra.prodEquivTensor (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] : ExteriorAlgebra R (M × N) ≃ₐ[R] GradedTensorProduct R (fun (i : ℕ) => ⋀[R]^i M) fun (i : ℕ) => ⋀[R]^i N

The equivalence ExteriorAlgebra R (M × N) ≃ₐ[R] ExteriorAlgebra R M ⊗ ExteriorAlgebra R N, with the right side given graded multiplication.

Equations

• ExteriorAlgebra.prodEquivTensor R M N = AlgEquiv.ofAlgHom (ExteriorAlgebra.prodEquivTensorForward R M N) (ExteriorAlgebra.prodEquivTensorInverse R M N) ⋯ ⋯

theorem ExteriorAlgebra.prodEquivTensor_symm_apply_tmul_ιMulti (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (i j : ℕ) (m : Fin i → M) (n : Fin j → N) : (prodEquivTensor R M N).symm ((ιMulti R i) m ᵍ⊗ₜ[R] (ιMulti R j) n) = (ιMulti R (i + j)) (Fin.append (⇑(LinearMap.inl R M N) ∘ m) (⇑(LinearMap.inr R M N) ∘ n))

theorem ExteriorAlgebra.prodEquivTensor_symm_tmul (R : Type u) [CommRing R] (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (a : ExteriorAlgebra R M) (b : ExteriorAlgebra R N) : (prodEquivTensor R M N).symm (a ᵍ⊗ₜ[R] b) = (map (LinearMap.inl R M N)) a * (map (LinearMap.inr R M N)) b