# 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 `DirectSum`. This notation is in the `DirectSum` locale, accessible after `open DirectSum`.

## References #

- https://en.wikipedia.org/wiki/Direct_sum

source
def DirectSum (ι : Type v) (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] :
Type (max w v)

`DirectSum ι β` is the direct sum of a family of additive commutative monoids `β i`.

Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum ι β`.

Equations

- DirectSum ι β = Π₀ (i : ι), β i

Instances For

source
instance instAddCommMonoidDirectSum (ι : Type u_1) (β : ι → Type u_2) [(i : ι) → AddCommMonoid (β i)] :
AddCommMonoid (DirectSum ι β)
Equations

- instAddCommMonoidDirectSum ι β = DFinsupp.addCommMonoid

source
instance instInhabitedDirectSum (ι : Type u_1) (β : ι → Type u_2) [(i : ι) → AddCommMonoid (β i)] :
Inhabited (DirectSum ι β)
Equations

- instInhabitedDirectSum ι β = DFinsupp.instInhabited

source
instance instDFunLikeDirectSum (ι : Type u_1) (β : ι → Type u_2) [(i : ι) → AddCommMonoid (β i)] :
DFunLike (DirectSum ι β) ι β
Equations

- instDFunLikeDirectSum ι β = DFinsupp.instDFunLike

source
instance instCoeFunDirectSumForall (ι : Type u_1) (β : ι → Type u_2) [(i : ι) → AddCommMonoid (β i)] :
CoeFun (DirectSum ι β) fun (x : Π₀ (i : ι), β i) => (a : ι) → β a
Equations

- instCoeFunDirectSumForall ι β = DFunLike.hasCoeToFun

source
def DirectSum.«term⨁_,_» :
Lean.ParserDescr

`⨁ i, f i` is notation for `DirectSum _ f` and equals the direct sum of `fun i ↦ f i`. Taking the direct sum over multiple arguments is possible, e.g. `⨁ (i) (j), f i j`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance instDecidableEqDirectSum (ι : Type v) (β : ι → Type w) [DecidableEq ι] [(i : ι) → AddCommMonoid (β i)] [(i : ι) → DecidableEq (β i)] :
DecidableEq (DirectSum ι β)
Equations

- instDecidableEqDirectSum ι β = inferInstanceAs (DecidableEq (Π₀ (i : ι), β i))

source
def DirectSum.coeFnAddMonoidHom {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] :
(DirectSum ι fun (i : ι) => β i) →+ (i : ι) → β i

Coercion from a `DirectSum` to a pi type is an `AddMonoidHom`.

Equations

- DirectSum.coeFnAddMonoidHom β = { toFun := fun (x : DirectSum ι fun (i : ι) => β i) => ⇑x, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DirectSum.coeFnAddMonoidHom_apply {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] (v : DirectSum ι fun (i : ι) => β i) :
(coeFnAddMonoidHom β) v = ⇑v
source
instance DirectSum.instAddCommGroup {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommGroup (β i)] :
AddCommGroup (DirectSum ι β)
Equations

- DirectSum.instAddCommGroup β = inferInstanceAs (AddCommGroup (Π₀ (i : ι), β i))

source
@[simp]
theorem DirectSum.sub_apply {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommGroup (β i)] (g₁ g₂ : DirectSum ι fun (i : ι) => β i) (i : ι) :
(g₁ - g₂) i = g₁ i - g₂ i
source
theorem DirectSum.ext {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] {x y : DirectSum ι β} (w : ∀ (i : ι), x i = y i) :
x = y
source
theorem DirectSum.ext_iff {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] {x y : DirectSum ι β} :
x = y ↔ ∀ (i : ι), x i = y i
source
@[simp]
theorem DirectSum.zero_apply {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] (i : ι) :
0 i = 0
source
@[simp]
theorem DirectSum.add_apply {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] (g₁ g₂ : DirectSum ι fun (i : ι) => β i) (i : ι) :
(g₁ + g₂) i = g₁ i + g₂ i
source
def DirectSum.mk {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (s : Finset ι) :
((i : ↑↑s) → β ↑i) →+ DirectSum ι fun (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

- DirectSum.mk β s = { toFun := DFinsupp.mk s, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
def DirectSum.of {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) :
β i →+ DirectSum ι fun (i : ι) => β i

`of i` is the natural inclusion map from `β i` to `⨁ i, β i`.

Equations

- DirectSum.of β i = DFinsupp.singleAddHom β i

Instances For

source
@[simp]
theorem DirectSum.of_eq_same {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) (x : β i) :
((of β i) x) i = x
source
theorem DirectSum.of_eq_of_ne {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i j : ι) (x : β i) (h : j ≠ i) :
((of β i) x) j = 0
source
theorem DirectSum.of_apply {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {i : ι} (j : ι) (x : β i) :
((of β i) x) j = if h : i = j then Eq.recOn h x else 0
source
theorem DirectSum.mk_apply_of_mem {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {s : Finset ι} {f : (i : ↑↑s) → β ↑i} {n : ι} (hn : n ∈ s) :
((mk β s) f) n = f ⟨n, hn⟩
source
theorem DirectSum.mk_apply_of_notMem {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {s : Finset ι} {f : (i : ↑↑s) → β ↑i} {n : ι} (hn : n ∉ s) :
((mk β s) f) n = 0
source
@[deprecated DirectSum.mk_apply_of_notMem (since := "2025-05-23")]
theorem DirectSum.mk_apply_of_not_mem {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {s : Finset ι} {f : (i : ↑↑s) → β ↑i} {n : ι} (hn : n ∉ s) :
((mk β s) f) n = 0

Alias of `DirectSum.mk_apply_of_notMem`.

source
@[simp]
theorem DirectSum.support_zero {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] :
DFinsupp.support 0 = ∅
source
@[simp]
theorem DirectSum.support_of {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) :
DFinsupp.support ((of β i) x) = {i}
source
theorem DirectSum.support_of_subset {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i} :
DFinsupp.support ((of β i) b) ⊆ {i}
source
theorem DirectSum.sum_support_of {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (x : DirectSum ι fun (i : ι) => β i) :
∑ i ∈ DFinsupp.support x, (of β i) (x i) = x
source
theorem DirectSum.sum_univ_of {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] [Fintype ι] (x : DirectSum ι fun (i : ι) => β i) :
∑ i : ι, (of β i) (x i) = x
source
theorem DirectSum.mk_injective {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (s : Finset ι) :
Function.Injective ⇑(mk β s)
source
theorem DirectSum.of_injective {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (i : ι) :
Function.Injective ⇑(of β i)
source
theorem DirectSum.induction_on {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {motive : (DirectSum ι fun (i : ι) => β i) → Prop} (x : DirectSum ι fun (i : ι) => β i) (zero : motive 0) (of : ∀ (i : ι) (x : β i), motive ((of β i) x)) (add : ∀ (x y : DirectSum ι fun (i : ι) => β i), motive x → motive y → motive (x + y)) :
motive x
source
theorem DirectSum.addHom_ext {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddZeroClass γ] ⦃f g : (DirectSum ι fun (i : ι) => β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), f ((of β i) y) = g ((of β i) y)) :
f = g

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

source
theorem DirectSum.addHom_ext' {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddZeroClass γ] ⦃f g : (DirectSum ι fun (i : ι) => β i) →+ γ⦄ (H : ∀ (i : ι), f.comp (of β i) = g.comp (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].

source
theorem DirectSum.addHom_ext'_iff {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u_1} [AddZeroClass γ] {f g : (DirectSum ι fun (i : ι) => β i) →+ γ} :
f = g ↔ ∀ (i : ι), f.comp (of β i) = g.comp (of β i)
source
def DirectSum.toAddMonoid {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) :
(DirectSum ι fun (i : ι) => β i) →+ γ

`toAddMonoid φ` is the natural homomorphism from `⨁ i, β i` to `γ` induced by a family `φ` of homomorphisms `β i → γ`.

Equations

- DirectSum.toAddMonoid φ = DFinsupp.liftAddHom φ

Instances For

source
@[simp]
theorem DirectSum.toAddMonoid_of {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i) :
(toAddMonoid φ) ((of β i) x) = (φ i) x
source
theorem DirectSum.toAddMonoid.unique {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (ψ : (DirectSum ι fun (i : ι) => β i) →+ γ) (f : DirectSum ι fun (i : ι) => β i) :
ψ f = (toAddMonoid fun (i : ι) => ψ.comp (of β i)) f
source
theorem DirectSum.toAddMonoid_injective {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] :
Function.Injective toAddMonoid
source
@[simp]
theorem DirectSum.toAddMonoid_inj {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] {f g : (i : ι) → β i →+ γ} :
toAddMonoid f = toAddMonoid g ↔ f = g
source
def DirectSum.fromAddMonoid {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] :
(DirectSum ι fun (i : ι) => γ →+ β i) →+ γ →+ DirectSum ι fun (i : ι) => β i

`fromAddMonoid φ` 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

- DirectSum.fromAddMonoid = DirectSum.toAddMonoid fun (i : ι) => AddMonoidHom.compHom (DirectSum.of β i)

Instances For

source
@[simp]
theorem DirectSum.fromAddMonoid_of {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (i : ι) (f : γ →+ β i) :
fromAddMonoid ((of (fun (i : ι) => γ →+ β i) i) f) = (of β i).comp f
source
theorem DirectSum.fromAddMonoid_of_apply {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] {γ : Type u₁} [AddCommMonoid γ] (i : ι) (f : γ →+ β i) (x : γ) :
(fromAddMonoid ((of (fun (i : ι) => γ →+ β i) i) f)) x = (of β i) (f x)
source
def DirectSum.setToSet {ι : Type v} (β : ι → Type w) [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (S T : Set ι) (H : S ⊆ T) :
(DirectSum ↑S fun (i : ↑S) => β ↑i) →+ DirectSum ↑T fun (i : ↑T) => β ↑i

`setToSet β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`, where `h : S ⊆ T`.

Equations

- DirectSum.setToSet β S T H = DirectSum.toAddMonoid fun (i : ↑S) => DirectSum.of (fun (i : Subtype T) => β ↑i) ⟨↑i, ⋯⟩

Instances For

source
instance DirectSum.unique {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [∀ (i : ι), Subsingleton (β i)] :
Unique (DirectSum ι fun (i : ι) => β i)
Equations

- DirectSum.unique = DFinsupp.unique

source
instance DirectSum.uniqueOfIsEmpty {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] [IsEmpty ι] :
Unique (DirectSum ι fun (i : ι) => β i)

A direct sum over an empty type is trivial.

Equations

- DirectSum.uniqueOfIsEmpty = DFinsupp.uniqueOfIsEmpty

source
def DirectSum.id (M : Type v) (ι : Type u_1 := PUnit.{u_1 + 1}) [AddCommMonoid M] [Unique ι] :
(DirectSum ι fun (x : ι) => M) ≃+ M

The natural equivalence between `⨁ _ : ι, M` and `M` when `Unique ι`.

Equations

- DirectSum.id M ι = { toFun := ⇑(DirectSum.toAddMonoid fun (x : ι) => AddMonoidHom.id M), invFun := ⇑(DirectSum.of (fun (x : ι) => M) default), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
def DirectSum.equivCongrLeft {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ) :
(DirectSum ι fun (i : ι) => β i) ≃+ DirectSum κ fun (k : κ) => β (h.symm k)

Reindexing terms of a direct sum.

Equations

- DirectSum.equivCongrLeft h = { toEquiv := DFinsupp.equivCongrLeft h, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DirectSum.equivCongrLeft_apply {ι : Type v} {β : ι → Type w} [(i : ι) → AddCommMonoid (β i)] {κ : Type u_1} (h : ι ≃ κ) (f : DirectSum ι fun (i : ι) => β i) (k : κ) :
((equivCongrLeft h) f) k = f (h.symm k)
source
noncomputable def DirectSum.addEquivProdDirectSum {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] :
(DirectSum (Option ι) fun (i : Option ι) => α i) ≃+ α none × DirectSum ι fun (i : ι) => α (some i)

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

Equations

- DirectSum.addEquivProdDirectSum = { toEquiv := DFinsupp.equivProdDFinsupp, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DirectSum.addEquivProdDirectSum_apply {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] (f : Π₀ (i : Option ι), (fun (i : Option ι) => α i) i) :
addEquivProdDirectSum f = (f none, DFinsupp.comapDomain some ⋯ f)
source
@[simp]
theorem DirectSum.addEquivProdDirectSum_symm_apply_support' {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] (f : (fun (i : Option ι) => α i) none × Π₀ (i : ι), (fun (i : Option ι) => α i) (some i)) :
(addEquivProdDirectSum.symm f).support' = Trunc.map (fun (s : { s : Multiset ι // ∀ (i : ι), i ∈ s ∨ f.2 i = 0 }) => ⟨none ::ₘ Multiset.map some ↑s, ⋯⟩) f.2.support'
source
@[simp]
theorem DirectSum.addEquivProdDirectSum_symm_apply_toFun {ι : Type v} {α : Option ι → Type w} [(i : Option ι) → AddCommMonoid (α i)] (f : (fun (i : Option ι) => α i) none × Π₀ (i : ι), (fun (i : Option ι) => α i) (some i)) (i : Option ι) :
(addEquivProdDirectSum.symm f) i = match i with | none => f.1 | some val => f.2 val
source
def DirectSum.sigmaCurry {ι : Type v} [DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
(DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) →+ DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

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

Equations

- DirectSum.sigmaCurry = { toFun := DFinsupp.sigmaCurry, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DirectSum.sigmaCurry_apply {ι : Type v} [DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) (i : ι) (j : α i) :
((sigmaCurry f) i) j = f ⟨i, j⟩
source
def DirectSum.sigmaUncurry {ι : Type v} [DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
(DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) →+ DirectSum ((_i : ι) × α _i) fun (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

- DirectSum.sigmaUncurry = { toFun := DFinsupp.sigmaUncurry, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem DirectSum.sigmaUncurry_apply {ι : Type v} [DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j) (i : ι) (j : α i) :
(sigmaUncurry f) ⟨i, j⟩ = (f i) j
source
def DirectSum.sigmaCurryEquiv {ι : Type v} [DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] :
(DirectSum ((_i : ι) × α _i) fun (i : (_i : ι) × α _i) => δ i.fst i.snd) ≃+ DirectSum ι fun (i : ι) => DirectSum (α i) fun (j : α i) => δ i j

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

Equations

- DirectSum.sigmaCurryEquiv = { toFun := (↑DirectSum.sigmaCurry).toFun, invFun := DFinsupp.sigmaCurryEquiv.invFun, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
def DirectSum.coeAddMonoidHom {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) :
(DirectSum ι fun (i : ι) => ↥(A i)) →+ M

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

When `S = Submodule _ M`, this is available as a `LinearMap`, `DirectSum.coe_linearMap`.

Equations

- DirectSum.coeAddMonoidHom A = DirectSum.toAddMonoid fun (i : ι) => AddSubmonoidClass.subtype (A i)

Instances For

source
theorem DirectSum.coeAddMonoidHom_eq_dfinsuppSum {ι : Type v} [DecidableEq ι] {M : Type u_1} {S : Type u_2} [DecidableEq M] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun (i : ι) => ↥(A i)) :
(DirectSum.coeAddMonoidHom A) x = DFinsupp.sum x fun (i : ι) (x : ↥(A i)) => ↑x
source
@[simp]
theorem DirectSum.coeAddMonoidHom_of {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) (i : ι) (x : ↥(A i)) :
(DirectSum.coeAddMonoidHom A) ((of (fun (i : ι) => ↥(A i)) i) x) = ↑x
source
theorem DirectSum.coe_of_apply {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : ↥(A i)) :
↑(((of (fun (i : ι) => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
source
def DirectSum.IsInternal {ι : Type v} {M : Type u_1} {S : Type u_2} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) :
Prop

The `DirectSum` 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 `DirectSum.subgroup_isInternal_iff_iSupIndep_and_supr_eq_top` and `DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top`.

Equations

- DirectSum.IsInternal A = Function.Bijective ⇑(DirectSum.coeAddMonoidHom A)

Instances For

source
theorem DirectSum.IsInternal.addSubmonoid_iSup_eq_top {ι : Type v} {M : Type u_1} [DecidableEq ι] [AddCommMonoid M] (A : ι → AddSubmonoid M) (h : IsInternal A) :
iSup A = ⊤
source
theorem DirectSum.support_subset {ι : Type v} {M : Type u_1} {S : Type u_2} [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] [DecidableEq ι] [DecidableEq M] (A : ι → S) (x : DirectSum ι fun (i : ι) => ↥(A i)) :
(Function.support fun (i : ι) => ↑(x i)) ⊆ ↑(DFinsupp.support x)
source
theorem DirectSum.finite_support {ι : Type v} {M : Type u_1} {S : Type u_2} [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) (x : DirectSum ι fun (i : ι) => ↥(A i)) :
(Function.support fun (i : ι) => ↑(x i)).Finite
source
def DirectSum.map {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) :
(DirectSum ι fun (i : ι) => α i) →+ DirectSum ι fun (i : ι) => β i

create a homomorphism from `⨁ i, α i` to `⨁ i, β i` by giving the component-wise map `f`.

Equations

- DirectSum.map f = DFinsupp.mapRange.addMonoidHom f

Instances For

source
@[simp]
theorem DirectSum.map_of {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) [DecidableEq ι] (i : ι) (x : α i) :
(map f) ((of α i) x) = (of β i) ((f i) x)
source
@[simp]
theorem DirectSum.map_apply {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) (i : ι) (x : DirectSum ι fun (i : ι) => α i) :
((map f) x) i = (f i) (x i)
source
@[simp]
theorem DirectSum.map_id {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → AddCommMonoid (α i)] :
(map fun (i : ι) => AddMonoidHom.id (α i)) = AddMonoidHom.id (DirectSum ι fun (i : ι) => α i)
source
@[simp]
theorem DirectSum.map_comp {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) {γ : ι → Type u_6} [(i : ι) → AddCommMonoid (γ i)] (g : (i : ι) → β i →+ γ i) :
(map fun (i : ι) => (g i).comp (f i)) = (map g).comp (map f)
source
theorem DirectSum.map_injective {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) :
Function.Injective ⇑(map f) ↔ ∀ (i : ι), Function.Injective ⇑(f i)
source
theorem DirectSum.map_surjective {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) :
Function.Surjective ⇑(map f) ↔ ∀ (i : ι), Function.Surjective ⇑(f i)
source
theorem DirectSum.map_eq_iff {ι : Type u_3} {α : ι → Type u_4} {β : ι → Type u_5} [(i : ι) → AddCommMonoid (α i)] [(i : ι) → AddCommMonoid (β i)] (f : (i : ι) → α i →+ β i) (x y : DirectSum ι fun (i : ι) => α i) :
(map f) x = (map f) y ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)
source
def DirectSum.addEquivProd {ι : Type u_1} [Fintype ι] (G : ι → Type u_2) [(i : ι) → AddCommMonoid (G i)] :
DirectSum ι G ≃+ ((i : ι) → G i)

The canonical isomorphism of a finite direct sum of additive commutative monoids and the corresponding finite product.

Equations

- DirectSum.addEquivProd G = { toEquiv := DFinsupp.equivFunOnFintype, map_add' := ⋯ }

Instances For