# mathlibdocumentation

algebra.direct_sum

# Direct sum

This file defines the direct sum of abelian groups, indexed by a discrete type.

## Notation

⨁ i, β i is the n-ary direct sum direct_sum. This notation is in the direct_sum locale, accessible after open_locale direct_sum.

## References

• https://en.wikipedia.org/wiki/Direct_sum
def direct_sum (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :
Type (max v w)

direct_sum β is the direct sum of a family of additive commutative monoids β i.

Note: open_locale direct_sum will enable the notation ⨁ i, β i for direct_sum β.

Equations
• β = Π₀ (i : ι), β i
@[instance]
def direct_sum.has_coe_to_fun (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

@[instance]
def direct_sum.add_comm_monoid (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

@[instance]
def direct_sum.inhabited (ι : Type v) (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] :

@[instance]
def direct_sum.add_comm_group {ι : Type v} (β : ι → Type w) [Π (i : ι), add_comm_group (β i)] :

Equations
@[simp]
theorem direct_sum.sub_apply {ι : Type v} {β : ι → Type w} [Π (i : ι), add_comm_group (β i)] (g₁ g₂ : ⨁ (i : ι), β i) (i : ι) :
(g₁ - g₂) i = g₁ i - g₂ i

@[simp]
theorem direct_sum.zero_apply {ι : Type v} (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (i : ι) :
0 i = 0

@[simp]
theorem direct_sum.add_apply {ι : Type v} {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (g₁ g₂ : ⨁ (i : ι), β i) (i : ι) :
(g₁ + g₂) i = g₁ i + g₂ i

def direct_sum.mk {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (s : finset ι) :
(Π (i : s), β i.val) →+ ⨁ (i : ι), β i

mk β s x is the element of ⨁ i, β i that is zero outside s and has coefficient x i for i in s.

Equations
def direct_sum.of {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (i : ι) :
β i →+ ⨁ (i : ι), β i

of i is the natural inclusion map from β i to ⨁ i, β i.

Equations
theorem direct_sum.mk_injective {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (s : finset ι) :

theorem direct_sum.of_injective {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] (i : ι) :

theorem direct_sum.induction_on {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {C : (⨁ (i : ι), β i) → Prop} (x : ⨁ (i : ι), β i) (H_zero : C 0) (H_basic : ∀ (i : ι) (x : β i), C ( i) x)) (H_plus : ∀ (x y : ⨁ (i : ι), β i), C xC yC (x + y)) :
C x

def direct_sum.to_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} (φ : Π (i : ι), β i →+ γ) :
(⨁ (i : ι), β i) →+ γ

to_add_monoid φ is the natural homomorphism from ⨁ i, β i to γ induced by a family φ of homomorphisms β i → γ.

Equations
@[simp]
theorem direct_sum.to_add_monoid_of {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} (φ : Π (i : ι), β i →+ γ) (i : ι) (x : β i) :
( i) x) = (φ i) x

theorem direct_sum.to_add_monoid.unique {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} (ψ : (⨁ (i : ι), β i) →+ γ) (f : ⨁ (i : ι), β i) :
ψ f = (direct_sum.to_add_monoid (λ (i : ι), ψ.comp i))) f

def direct_sum.from_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁}  :
(⨁ (i : ι), γ →+ β i) →+ γ →+ ⨁ (i : ι), β i

from_add_monoid φ is the natural homomorphism from γ to ⨁ i, β i induced by a family φ of homomorphisms γ → β i.

Note that this is not an isomorphism. Not every homomorphism γ →+ ⨁ i, β i arises in this way.

Equations
@[simp]
theorem direct_sum.from_add_monoid_of {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} (i : ι) (f : γ →+ β i) :
direct_sum.from_add_monoid ((direct_sum.of (λ (i : ι), γ →+ β i) i) f) = (direct_sum.of (λ (i : ι), β i) i).comp f

theorem direct_sum.from_add_monoid_of_apply {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} (i : ι) (f : γ →+ β i) (x : γ) :
(direct_sum.from_add_monoid ((direct_sum.of (λ (i : ι), γ →+ β i) i) f)) x = (direct_sum.of (λ (i : ι), β i) i) (f x)

def direct_sum.set_to_set {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_monoid (β i)] (S T : set ι) (H : S T) :
(⨁ (i : S), β i) →+ ⨁ (i : T), β i

set_to_set β S T h is the natural homomorphism ⨁ (i : S), β i → ⨁ (i : T), β i, where h : S ⊆ T.

Equations
def direct_sum.id (M : Type v) (ι : Type u_1 := punit) [unique ι] :
(⨁ (_x : ι), M) ≃+ M

The natural equivalence between ⨁ _ : ι, M and M when unique ι.

Equations