Direct sum from _ to _

This file includes the definition of direct_sum_from_to, a linear map from M i to M j.

def directSumFromTo {R : Type u_1} [Semiring R] {ι₁ : Type u_2} [DecidableEq ι₁] {M₁ : ι₁ → Type u_3} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₁ : ι₁) → Module R (M₁ i₁)] (i j : ι₁) : M₁ i →ₗ[R] M₁ j

Composition of the i-th injection and the j-th projection of a dependent direct sum, giving a linear map M₁ i →ₗ[R] M₁ j.

Equations

• directSumFromTo i j = LinearMap.proj j ∘ₗ LinearMap.single R M₁ i

theorem directSumFromTo_apply_same {R : Type u_1} [Semiring R] {ι₁ : Type u_2} [DecidableEq ι₁] {M₁ : ι₁ → Type u_3} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₁ : ι₁) → Module R (M₁ i₁)] (i : ι₁) : directSumFromTo i i = 1

theorem directSumFromTo_apply_ne_same {R : Type u_1} [Semiring R] {ι₁ : Type u_2} [DecidableEq ι₁] {M₁ : ι₁ → Type u_3} [(i₁ : ι₁) → AddCommGroup (M₁ i₁)] [(i₁ : ι₁) → Module R (M₁ i₁)] {i j : ι₁} (h : j ≠ i) : directSumFromTo i j = 0