# mathlib3documentation

algebra.direct_sum.basic

# Direct sum #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
Instances for direct_sum
@[protected, instance]
def direct_sum.add_comm_monoid (ι : Type v) (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] :
@[protected, instance]
def direct_sum.inhabited (ι : Type v) (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] :
@[protected, instance]
def direct_sum.has_coe_to_fun (ι : Type v) (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] :
has_coe_to_fun β) (λ (_x : β), Π (i : ι), β i)
Equations
@[protected, 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
@[simp]
theorem direct_sum.of_eq_same {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] (i : ι) (x : β i) :
((direct_sum.of (λ (i : ι), β i) i) x) i = x
theorem direct_sum.of_eq_of_ne {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] (i j : ι) (x : β i) (h : i j) :
((direct_sum.of (λ (i : ι), β i) i) x) j = 0
@[simp]
theorem direct_sum.support_zero {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] :
@[simp]
theorem direct_sum.support_of {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (i : ι) (x : β i) (h : x 0) :
dfinsupp.support ((direct_sum.of (λ (i : ι), β i) i) x) = {i}
theorem direct_sum.support_of_subset {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] {i : ι} {b : β i} :
dfinsupp.support ((direct_sum.of (λ {i : ι}, β i) i) b) {i}
theorem direct_sum.sum_support_of {ι : Type v} [dec_ι : decidable_eq ι] (β : ι Type w) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (x : (λ (i : ι), β i)) :
.sum (λ (i : ι), i) (x i)) = x
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 : ι) :
@[protected]
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 x C y C (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
@[protected, instance]
def direct_sum.unique {ι : Type v} {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] [ (i : ι), subsingleton (β i)] :
unique (λ (i : ι), β i))
Equations
@[protected, instance]
def direct_sum.unique_of_is_empty {ι : Type v} {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] [is_empty ι] :
unique (λ (i : ι), β i))

A direct sum over an empty type is trivial.

Equations
@[protected]
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.equiv_congr_left {ι : Type v} {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] {κ : Type u_1} (h : ι κ) :
(λ (i : ι), β i) ≃+ (λ (k : κ), β ((h.symm) k))

Reindexing terms of a direct sum.

Equations
@[simp]
theorem direct_sum.equiv_congr_left_apply {ι : Type v} {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] {κ : Type u_1} (h : ι κ) (f : (λ (i : ι), β i)) (k : κ) :
f) k = f ((h.symm) k)
@[simp]
theorem direct_sum.add_equiv_prod_direct_sum_apply {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] (ᾰ : Π₀ (i : option ι), (λ (i : option ι), α i) i) :
@[simp]
theorem direct_sum.add_equiv_prod_direct_sum_symm_apply {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] (ᾰ : (λ (i : option ι), α i) option.none × Π₀ (i : ι), (λ (i : option ι), α i) (option.some i)) :
noncomputable def direct_sum.add_equiv_prod_direct_sum {ι : Type v} [dec_ι : decidable_eq ι] {α : Type w} [Π (i : option ι), add_comm_monoid (α i)] :
direct_sum (option ι) (λ (i : option ι), α i) ≃+ × (λ (i : ι), α (option.some i))

Isomorphism obtained by separating the term of index none of a direct sum over option ι.

Equations
noncomputable def direct_sum.sigma_curry {ι : Type v} {α : ι Type u} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) →+ (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))

The natural map between ⨁ (i : Σ i, α i), δ i.1 i.2 and ⨁ i (j : α i), δ i j.

Equations
@[simp]
theorem direct_sum.sigma_curry_apply {ι : Type v} {α : ι Type u} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] (f : direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd)) (i : ι) (j : α i) :
i) j = f i, j⟩
def direct_sum.sigma_uncurry {ι : Type v} {α : ι Type u} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] :
(λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j)) →+ direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd)

The natural map between ⨁ i (j : α i), δ i j and Π₀ (i : Σ i, α i), δ i.1 i.2, inverse of curry.

Equations
@[simp]
theorem direct_sum.sigma_uncurry_apply {ι : Type v} {α : ι Type u} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] (f : (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))) (i : ι) (j : α i) :
i, j⟩ = (f i) j
noncomputable def direct_sum.sigma_curry_equiv {ι : Type v} {α : ι Type u} {δ : Π (i : ι), α i Type w} [Π (i : ι) (j : α i), add_comm_monoid (δ i j)] [Π (i : ι), decidable_eq (α i)] [Π (i : ι) (j : α i), decidable_eq (δ i j)] :
direct_sum (Σ (i : ι), α i) (λ (i : Σ (i : ι), α i), δ i.fst i.snd) ≃+ (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))

The natural map between ⨁ (i : Σ i, α i), δ i.1 i.2 and ⨁ i (j : α i), δ i j.

Equations
@[protected]
def direct_sum.coe_add_monoid_hom {ι : Type v} {M : Type u_1} {S : Type u_2} [decidable_eq ι] [ M] [ M] (A : ι S) :
(λ (i : ι), (A i)) →+ M

The canonical embedding from ⨁ i, A i to M where A is a collection of add_submonoid M indexed by ι.

When S = submodule _ M, this is available as a linear_map, direct_sum.coe_linear_map.

Equations
@[simp]
theorem direct_sum.coe_add_monoid_hom_of {ι : Type v} {M : Type u_1} {S : Type u_2} [decidable_eq ι] [ M] [ M] (A : ι S) (i : ι) (x : (A i)) :
((direct_sum.of (λ (i : ι), (A i)) i) x) = x
theorem direct_sum.coe_of_apply {ι : Type v} {M : Type u_1} {S : Type u_2} [decidable_eq ι] [ M] [ M] {A : ι S} (i j : ι) (x : (A i)) :
(((direct_sum.of (λ (i : ι), (A i)) i) x) j) = ite (i = j) x 0
def direct_sum.is_internal {ι : Type v} {M : Type u_1} {S : Type u_2} [decidable_eq ι] [ M] [ M] (A : ι S) :
Prop

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

For the alternate statement in terms of independence and spanning, see direct_sum.subgroup_is_internal_iff_independent_and_supr_eq_top and direct_sum.is_internal_submodule_iff_independent_and_supr_eq_top.

Equations