Homotopy Type Theory
graded module > history (Rev #1)
Defintion
ℕ \mathbb{N} -graded modules
Given a commutative ring R R , an ℕ \mathbb{N} -graded R R -module or just graded R R -module is an R R -module A A with a binary function ⟨ − ⟩ ( − ) : A × ℕ → A \langle - \rangle_{(-)}: A \times \mathbb{N} \to A called the grade projection operator such that
∏ a : A a = ∑ n : ℕ ⟨ a ⟩ n \prod_{a:A} a = \sum_{n:\mathbb{N}} \langle a \rangle_n ∏ a : A ∏ b : A ∏ n : ℕ ⟨ a + b ⟩ n = ⟨ a ⟩ n + ⟨ b ⟩ n \prod_{a:A} \prod_{b:A} \prod_{n:\mathbb{N}} \langle a + b \rangle_n = \langle a \rangle_n + \langle b \rangle_n ∏ a : A ∏ c : A ∏ n : ℕ ( c = ⟨ c ⟩ 0 ) × ( ⟨ c a ⟩ n = c ⟨ a ⟩ n ) \prod_{a:A} \prod_{c:A} \prod_{n:\mathbb{N}} (c = \langle c \rangle_0) \times (\langle c a \rangle_n = c \langle a \rangle_n) ∏ a : A ∏ n : ℕ ⟨ ⟨ a ⟩ n ⟩ n = ⟨ a ⟩ n \prod_{a:A} \prod_{n:\mathbb{N}} \langle \langle a \rangle_n \rangle_n = \langle a \rangle_n ∏ a : A ∏ m : ℕ ∏ n : ℕ ( m ≠ n ) × ( ⟨ ⟨ a ⟩ m ⟩ n = 0 ) \prod_{a:A} \prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}} (m \neq n) \times (\langle \langle a \rangle_m \rangle_n = 0)
Terms of A A are called multivectors .
For a natural number n : ℕ n:\mathbb{N} , the image of ⟨ − ⟩ n \langle - \rangle_n under A A is called the n n -module and is denoted as ⟨ A ⟩ n \langle A \rangle_n .
⟨ A ⟩ n ≔ im ( ⟨ − ⟩ n ) \langle A \rangle_n \coloneqq \mathrm{im}(\langle - \rangle_n)
The terms of ⟨ A ⟩ n \langle A \rangle_n are called n n -vectors .
We define the filtration operator ℱ ( − ) : ℕ × A → A \mathcal{F}_{(-)}: \mathbb{N} \times A \to A
ℱ n ( v ) = ∑ m = 0 n ⟨ v ⟩ m \mathcal{F}_{n}(v) = \sum_{m = 0}^n \langle v \rangle_m
For a natural number n : ℕ n:\mathbb{N} , the image of ℱ n \mathcal{F}_{n} under A A is called the filtered n n -module and is denoted as ℱ n ( A ) \mathcal{F}_{n}(A) .
ℱ n ( A ) ≔ im ( ℱ n ) \mathcal{F}_{n}(A) \coloneqq \mathrm{im}(\mathcal{F}_{n})
The terms of ℱ n ( A ) \mathcal{F}_{n}(A) are called n n -multivectors .
Every filtered R R -algebra is an ℕ \mathbb{N} -graded R R -module.
supermodules
…
See also
Revision on May 10, 2022 at 17:23:11 by
Anonymous? .
See the history of this page for a list of all contributions to it.