# 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 #

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
theorem direct_sum.add_hom_ext {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u_1} [add_monoid γ] ⦃f g : (⨁ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), f ((direct_sum.of (λ (i : ι), β i) i) y) = g ((direct_sum.of (λ (i : ι), β i) i) y)) :
f = g

If two additive homomorphisms from ⨁ i, β i are equal on each of β i y, then they are equal.

@[ext]
theorem direct_sum.add_hom_ext' {ι : Type v} [dec_ι : decidable_eq ι] {β : ι → Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u_1} [add_monoid γ] ⦃f g : (⨁ (i : ι), β i) →+ γ⦄ (H : ∀ (i : ι), f.comp (direct_sum.of (λ (i : ι), β i) i) = g.comp i)) :
f = g

If two additive homomorphisms from ⨁ i, β i are equal on each of β i y, then they are equal.

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
def direct_sum.add_submonoid_is_internal {ι : Type v} {M : Type u_1} [decidable_eq ι] (A : ι → ) :
Prop

The direct_sum formed by a collection of add_submonoids of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

See direct_sum.add_subgroup_is_internal for the same statement about add_subgroups.

Equations
theorem direct_sum.add_submonoid_is_internal.supr_eq_top {ι : Type v} {M : Type u_1} [decidable_eq ι] (A : ι → )  :
def direct_sum.add_subgroup_is_internal {ι : Type v} {M : Type u_1} [decidable_eq ι] (A : ι → ) :
Prop

The direct_sum formed by a collection of add_subgroups of M is said to be internal if the canonical map (⨁ i, A i) →+ M is bijective.

See direct_sum.submodule_is_internal for the same statement about submoduless.

Equations
theorem direct_sum.add_subgroup_is_internal.to_add_submonoid {ι : Type v} {M : Type u_1} [decidable_eq ι] (A : ι → ) :