Direct sum from _ to _ #
This file includes the definition of direct_sum_from_to which is a linear map from M i to M j.
def
direct_sum_from_to
{R : Type u_1}
[semiring R]
{ι₁ : Type u_2}
[decidable_eq ι₁]
{M₁ : ι₁ → Type u_3}
[Π (i₁ : ι₁), add_comm_group (M₁ i₁)]
[Π (i₁ : ι₁), module R (M₁ i₁)]
(i j : ι₁) :
Equations
- direct_sum_from_to i j = (linear_map.proj j).comp (linear_map.single i)
theorem
direct_sum_from_to_apply_same
{R : Type u_1}
[semiring R]
{ι₁ : Type u_2}
[decidable_eq ι₁]
{M₁ : ι₁ → Type u_3}
[Π (i₁ : ι₁), add_comm_group (M₁ i₁)]
[Π (i₁ : ι₁), module R (M₁ i₁)]
(i : ι₁) :
direct_sum_from_to i i = 1
theorem
direct_sum_from_to_apply_ne_same
{R : Type u_1}
[semiring R]
{ι₁ : Type u_2}
[decidable_eq ι₁]
{M₁ : ι₁ → Type u_3}
[Π (i₁ : ι₁), add_comm_group (M₁ i₁)]
[Π (i₁ : ι₁), module R (M₁ i₁)]
{i j : ι₁}
(h : j ≠ i) :
direct_sum_from_to i j = 0