# 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_group (β i)] :
Type (max v w)

direct_sum β is the direct sum of a family of additive commutative groups β 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_group (β i)] :

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

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

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

@[simp]
theorem direct_sum.add_apply {ι : Type v} {β : ι → Type w} [Π (i : ι), add_comm_group (β 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_group (β 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_group (β 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_group (β i)] (s : finset ι) :

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

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

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

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

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

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

def direct_sum.set_to_set {ι : Type v} [dec_ι : decidable_eq ι] (β : ι → Type w) [Π (i : ι), add_comm_group (β i)] (S T : set ι) :
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