mathlib3 documentation

linear_algebra.exterior_algebra.grading

Results about the grading structure of the exterior algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Many of these results are copied with minimal modification from the tensor algebra.

The main result is exterior_algebra.graded_algebra, which says that the exterior algebra is a ℕ-graded algebra.

source
def exterior_algebra.graded_algebra.ι (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] :
M →ₗ[R] direct_sum ℕ (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i))

A version of exterior_algebra.ι that maps directly into the graded structure. This is primarily an auxiliary construction used to provide exterior_algebra.graded_algebra.

Equations
source
theorem exterior_algebra.graded_algebra.ι_apply (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] (m : M) :
⇑(exterior_algebra.graded_algebra.ι R M) m = ⇑(direct_sum.of (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i)) 1) ⟨⇑(exterior_algebra.ι R) m, _⟩
source
theorem exterior_algebra.graded_algebra.ι_sq_zero (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] (m : M) :
⇑(exterior_algebra.graded_algebra.ι R M) m * ⇑(exterior_algebra.graded_algebra.ι R M) m = 0
source
def exterior_algebra.graded_algebra.lift_ι (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] :
exterior_algebra R M →ₐ[R] direct_sum ℕ (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i))

exterior_algebra.graded_algebra.ι lifted to exterior algebra. This is primarily an auxiliary construction used to provide exterior_algebra.graded_algebra.

Equations
source
theorem exterior_algebra.graded_algebra.lift_ι_eq (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] (i : ℕ) (x : ↥(linear_map.range (exterior_algebra.ι R) ^ i)) :
⇑(exterior_algebra.graded_algebra.lift_ι R M) ↑x = ⇑(direct_sum.of (λ (i : ℕ), ↥(linear_map.range (exterior_algebra.ι R) ^ i)) i) x
source
@[protected, instance]
def exterior_algebra.graded_algebra (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] :
graded_algebra (has_pow.pow (linear_map.range (exterior_algebra.ι R)))

The exterior algebra is graded by the powers of the submodule (exterior_algebra.ι R).range.

Equations