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 #
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
- direct_sum ι β = Π₀ (i : ι), β i
Instances for direct_sum
- direct_sum.add_comm_monoid
- direct_sum.inhabited
- direct_sum.has_coe_to_fun
- direct_sum.add_comm_group
- direct_sum.unique
- direct_sum.unique_of_is_empty
- direct_sum.module
- direct_sum.smul_comm_class
- direct_sum.is_scalar_tower
- direct_sum.is_central_scalar
- module.free.direct_sum
- direct_sum.add_comm_group_set_like
@[protected, instance]
def
direct_sum.add_comm_monoid
(ι : Type v)
(β : ι → Type w)
[Π (i : ι), add_comm_monoid (β i)] :
add_comm_monoid (direct_sum ι β)
@[protected, instance]
def
direct_sum.inhabited
(ι : Type v)
(β : ι → Type w)
[Π (i : ι), add_comm_monoid (β i)] :
inhabited (direct_sum ι β)
@[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)] :
add_comm_group (direct_sum ι β)
Equations
@[simp]
theorem
direct_sum.sub_apply
{ι : Type v}
{β : ι → Type w}
[Π (i : ι), add_comm_group (β i)]
(g₁ g₂ : direct_sum ι (λ (i : ι), β i))
(i : ι) :
@[simp]
theorem
direct_sum.zero_apply
{ι : Type v}
(β : ι → Type w)
[Π (i : ι), add_comm_monoid (β i)]
(i : ι) :
@[simp]
theorem
direct_sum.add_apply
{ι : Type v}
{β : ι → Type w}
[Π (i : ι), add_comm_monoid (β i)]
(g₁ g₂ : direct_sum ι (λ (i : ι), β i))
(i : ι) :
def
direct_sum.mk
{ι : Type v}
[dec_ι : decidable_eq ι]
(β : ι → Type w)
[Π (i : ι), add_comm_monoid (β i)]
(s : finset ι) :
mk β s x is the element of ⨁ i, β i that is zero outside s
and has coefficient x i for i in s.
Equations
- direct_sum.mk β s = {to_fun := dfinsupp.mk s, map_zero' := _, map_add' := _}
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
- direct_sum.of β i = dfinsupp.single_add_hom β i
@[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.
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) :
⇑(direct_sum.to_add_monoid φ) (⇑(direct_sum.of β 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₁}
[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
- direct_sum.from_add_monoid = direct_sum.to_add_monoid (λ (i : ι), ⇑add_monoid_hom.comp_hom (direct_sum.of β i))
@[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
- direct_sum.set_to_set β S T H = direct_sum.to_add_monoid (λ (i : ↥S), direct_sum.of (λ (i : subtype T), β ↑i) ⟨↑i, _⟩)
@[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.
@[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
- direct_sum.id M ι = {to_fun := ⇑(direct_sum.to_add_monoid (λ (_x : ι), add_monoid_hom.id M)), inv_fun := ⇑(direct_sum.of (λ (_x : ι), M) inhabited.default), left_inv := _, right_inv := _, map_add' := _}
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
- direct_sum.equiv_congr_left h = {to_fun := (dfinsupp.equiv_congr_left h).to_fun, inv_fun := (dfinsupp.equiv_congr_left h).inv_fun, left_inv := _, right_inv := _, map_add' := _}
@[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
- direct_sum.sigma_curry = {to_fun := dfinsupp.sigma_curry (λ (i : ι) (j : α i), add_zero_class.to_has_zero (δ i j)), map_zero' := _, map_add' := _}
@[simp]
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
- direct_sum.sigma_uncurry = {to_fun := dfinsupp.sigma_uncurry (λ (i : ι) (j : α i) (x : (λ (j : α i), δ i j) j), ne.decidable x 0), map_zero' := _, map_add' := _}
@[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
- direct_sum.sigma_curry_equiv = {to_fun := direct_sum.sigma_curry.to_fun, inv_fun := dfinsupp.sigma_curry_equiv.inv_fun, left_inv := _, right_inv := _, map_add' := _}
@[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
- direct_sum.coe_add_monoid_hom A = direct_sum.to_add_monoid (λ (i : ι), add_submonoid_class.subtype (A i))
@[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)) :
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
theorem
direct_sum.is_internal.add_submonoid_supr_eq_top
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
(A : ι → add_submonoid M)
(h : direct_sum.is_internal A) :