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 #
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
@[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₂ : ⨁ (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₂ : ⨁ (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 →+ ⨁ (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 : ⨁ (i : ι), β i) :
∑ (i : ι) in dfinsupp.support x, ⇑(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 : (⨁ (i : ι), β i) → Prop}
(x : ⨁ (i : ι), β i)
(H_zero : C 0)
(H_basic : ∀ (i : ι) (x : β i), C (⇑(direct_sum.of β 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 (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 →+ γ) :
(⨁ (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 γ]
(ψ : (⨁ (i : ι), β i) →+ γ)
(f : ⨁ (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 γ] :
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) :
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)]
[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)
[add_comm_monoid M]
[unique ι] :
(⨁ (_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) 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 : ι ≃ κ) :
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 : ⨁ (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) none × Π₀ (i : ι), (λ (i : option ι), α i) (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)] :
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)] :
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]
theorem
direct_sum.sigma_curry_apply
{ι : Type v}
{α : ι → Type u}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)]
(f : ⨁ (i : Σ (i : ι), α i), δ i.fst i.snd)
(i : ι)
(j : α i) :
noncomputable
def
direct_sum.sigma_uncurry
{ι : Type v}
{α : ι → Type u}
{δ : Π (i : ι), α i → Type w}
[Π (i : ι) (j : α i), add_comm_monoid (δ i j)] :
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 : ι) (i_1 : α i), add_zero_class.to_has_zero ((λ (j : α i), δ i j) i_1)), 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)]
(f : ⨁ (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)] :
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' := _}
def
direct_sum.add_submonoid_coe
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
(A : ι → add_submonoid M) :
The canonical embedding from ⨁ i, A i to M where A is a collection of add_submonoid M
indexed by ι
Equations
- direct_sum.add_submonoid_coe A = direct_sum.to_add_monoid (λ (i : ι), (A i).subtype)
@[simp]
theorem
direct_sum.add_submonoid_coe_of
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
(A : ι → add_submonoid M)
(i : ι)
(x : ↥(A i)) :
⇑(direct_sum.add_submonoid_coe A) (⇑(direct_sum.of (λ (i : ι), ↥(A i)) i) x) = ↑x
theorem
direct_sum.coe_of_add_submonoid_apply
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
{A : ι → add_submonoid M}
(i j : ι)
(x : ↥(A i)) :
def
direct_sum.add_submonoid_is_internal
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
(A : ι → add_submonoid M) :
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.
theorem
direct_sum.add_submonoid_is_internal.supr_eq_top
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_monoid M]
(A : ι → add_submonoid M)
(h : direct_sum.add_submonoid_is_internal A) :
def
direct_sum.add_subgroup_coe
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_group M]
(A : ι → add_subgroup M) :
The canonical embedding from ⨁ i, A i to M where A is a collection of add_subgroup M
indexed by ι
Equations
- direct_sum.add_subgroup_coe A = direct_sum.to_add_monoid (λ (i : ι), (A i).subtype)
@[simp]
theorem
direct_sum.add_subgroup_coe_of
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_group M]
(A : ι → add_subgroup M)
(i : ι)
(x : ↥(A i)) :
⇑(direct_sum.add_subgroup_coe A) (⇑(direct_sum.of (λ (i : ι), ↥(A i)) i) x) = ↑x
theorem
direct_sum.coe_of_add_subgroup_apply
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_group M]
{A : ι → add_subgroup M}
(i j : ι)
(x : ↥(A i)) :
def
direct_sum.add_subgroup_is_internal
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_group M]
(A : ι → add_subgroup M) :
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.
theorem
direct_sum.add_subgroup_is_internal.to_add_submonoid
{ι : Type v}
{M : Type u_1}
[decidable_eq ι]
[add_comm_group M]
(A : ι → add_subgroup M) :
direct_sum.add_subgroup_is_internal A ↔ direct_sum.add_submonoid_is_internal (λ (i : ι), (A i).to_add_submonoid)