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
Equations
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' := _}
of i
is the natural inclusion map from β i
to ⨁ i, β i
.
Equations
- direct_sum.of β i = dfinsupp.single_add_hom β i
If two additive homomorphisms from ⨁ i, β i
are equal on each of β i y
,
then they are equal.
If two additive homomorphisms from ⨁ i, β i
are equal on each of β i y
,
then they are equal.
to_add_monoid φ
is the natural homomorphism from ⨁ i, β i
to γ
induced by a family φ
of homomorphisms β i → γ
.
Equations
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))
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, _⟩)
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' := _}
The direct_sum
formed by a collection of add_submonoid
s 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_subgroup
s.
Equations
- direct_sum.add_submonoid_is_internal A = function.bijective ⇑(direct_sum.to_add_monoid (λ (i : ι), (A i).subtype))
The direct_sum
formed by a collection of add_subgroup
s 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 submodules
s.
Equations
- direct_sum.add_subgroup_is_internal A = function.bijective ⇑(direct_sum.to_add_monoid (λ (i : ι), (A i).subtype))