mathlib3 documentation

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 #

@[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 (direct_sum ι β) (λ (_x : direct_sum ι β), Π (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₂ : direct_sum ι (λ (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₂ : direct_sum ι (λ (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) →+ direct_sum ι (λ (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 →+ direct_sum ι (λ (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 : direct_sum ι (λ (i : ι), β i)) :
(dfinsupp.support x).sum (λ (i : ι), (direct_sum.of β 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 : direct_sum ι (λ (i : ι), β i) Prop} (x : direct_sum ι (λ (i : ι), β i)) (H_zero : C 0) (H_basic : (i : ι) (x : β i), C ((direct_sum.of β i) x)) (H_plus : (x y : direct_sum ι (λ (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 : direct_sum ι (λ (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 : direct_sum ι (λ (i : ι), β i) →+ γ⦄ (H : (i : ι), f.comp (direct_sum.of (λ (i : ι), β i) i) = g.comp (direct_sum.of β i)) :
f = g

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

See note [partially-applied ext lemmas].

def direct_sum.to_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) :
direct_sum ι (λ (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₁} [add_comm_monoid γ] (φ : Π (i : ι), β i →+ γ) (i : ι) (x : β i) :
theorem direct_sum.to_add_monoid.unique {ι : Type v} [dec_ι : decidable_eq ι] {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] (ψ : direct_sum ι (λ (i : ι), β i) →+ γ) (f : direct_sum ι (λ (i : ι), β i)) :
ψ f = (direct_sum.to_add_monoid (λ (i : ι), ψ.comp (direct_sum.of β i))) f
def direct_sum.from_add_monoid {ι : Type v} [dec_ι : decidable_eq ι] {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] {γ : Type u₁} [add_comm_monoid γ] :
direct_sum ι (λ (i : ι), γ →+ β i) →+ γ →+ direct_sum ι (λ (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₁} [add_comm_monoid γ] (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₁} [add_comm_monoid γ] (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) :
direct_sum S (λ (i : S), β i) →+ direct_sum T (λ (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 (direct_sum ι (λ (i : ι), β i))
Equations
@[protected, instance]
def direct_sum.unique_of_is_empty {ι : Type v} {β : ι Type w} [Π (i : ι), add_comm_monoid (β i)] [is_empty ι] :
unique (direct_sum ι (λ (i : ι), β i))

A direct sum over an empty type is trivial.

Equations
@[protected]
def direct_sum.id (M : Type v) (ι : Type u_1 := punit) [add_comm_monoid M] [unique ι] :
direct_sum ι (λ (_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 : ι κ) :
direct_sum ι (λ (i : ι), β i) ≃+ direct_sum κ (λ (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 : direct_sum ι (λ (i : ι), β i)) (k : κ) :
@[simp]
theorem direct_sum.add_equiv_prod_direct_sum_apply {ι : Type v} [dec_ι : decidable_eq ι] {α : option ι 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 ι] {α : option ι 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 ι] {α : option ι Type w} [Π (i : option ι), add_comm_monoid (α i)] :
direct_sum (option ι) (λ (i : option ι), α i) ≃+ α option.none × direct_sum ι (λ (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) →+ direct_sum ι (λ (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) :
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)] :
direct_sum ι (λ (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 : direct_sum ι (λ (i : ι), direct_sum (α i) (λ (j : α i), δ i j))) (i : ι) (j : α i) :
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) ≃+ direct_sum ι (λ (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 ι] [add_comm_monoid M] [set_like S M] [add_submonoid_class S M] (A : ι S) :
direct_sum ι (λ (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 ι] [add_comm_monoid M] [set_like S M] [add_submonoid_class S M] (A : ι S) (i : ι) (x : (A i)) :
(direct_sum.coe_add_monoid_hom A) ((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 ι] [add_comm_monoid M] [set_like S M] [add_submonoid_class S 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 ι] [add_comm_monoid M] [set_like S M] [add_submonoid_class S 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