Mathlib.Algebra.DirectSum.Basic

DirectSum definition

[∀ i, AddCommMonoid (β i)] : Type _

Full source

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

Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum ι β`. -/
def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
  Π₀ i, β i

Direct sum of additive commutative monoids

Informal description

Given an index type $\iota$ and a family of additive commutative monoids $\beta_i$ for each $i \in \iota$, the direct sum $\bigoplus_{i} \beta_i$ is the coproduct in the category of additive commutative monoids. It consists of dependent functions with finite support from $\iota$ to the $\beta_i$.

instInhabitedDirectSum instance

[∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β)

Full source

instance [∀ i, AddCommMonoid (β i)] : Inhabited (DirectSum ι β) :=
  inferInstanceAs (Inhabited (Π₀ i, β i))

Direct Sum is Inhabited

Informal description

For any index type $\iota$ and family of additive commutative monoids $\beta_i$ indexed by $\iota$, the direct sum $\bigoplus_i \beta_i$ is inhabited (i.e., has at least one element).

instAddCommMonoidDirectSum instance

[∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β)

Full source

instance [∀ i, AddCommMonoid (β i)] : AddCommMonoid (DirectSum ι β) :=
  inferInstanceAs (AddCommMonoid (Π₀ i, β i))

Additive Commutative Monoid Structure on Direct Sum

Informal description

For any index type $\iota$ and family of additive commutative monoids $\beta_i$ indexed by $\iota$, the direct sum $\bigoplus_{i} \beta_i$ is an additive commutative monoid with pointwise addition and zero element.

instDFunLikeDirectSum instance

[∀ i, AddCommMonoid (β i)] : DFunLike (DirectSum ι β) _ fun i : ι => β i

Full source

instance [∀ i, AddCommMonoid (β i)] : DFunLike (DirectSum ι β) _ fun i : ι => β i :=
  inferInstanceAs (DFunLike (Π₀ i, β i) _ _)

Dependent Function-Like Structure on Direct Sums

Informal description

For any family of additive commutative monoids $\beta_i$ indexed by $i \in \iota$, the direct sum $\bigoplus_{i} \beta_i$ can be treated as a dependent function type where each element is a function from $\iota$ to $\beta_i$ with finite support.

instCoeFunDirectSumForall instance

[∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i

Full source

instance [∀ i, AddCommMonoid (β i)] : CoeFun (DirectSum ι β) fun _ => ∀ i : ι, β i :=
  inferInstanceAs (CoeFun (Π₀ i, β i) fun _ => ∀ i : ι, β i)

Canonical Function Coercion for Direct Sums

Informal description

For any index type $\iota$ and family of additive commutative monoids $\beta_i$ indexed by $i \in \iota$, the direct sum $\bigoplus_{i} \beta_i$ can be treated as a function from $\iota$ to $\beta_i$ via the canonical coercion.

DirectSum.term⨁_,_ definition

: Lean.ParserDescr✝

Full source

/-- `⨁ 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`. -/
scoped[DirectSum] notation3 "⨁ "(...)", "r:(scoped f => DirectSum _ f) => r

Direct sum notation

Informal description

The notation `⨁ i, f i` represents the direct sum of a family of abelian groups `(f i)`, indexed by a discrete type. This can be extended to multiple indices, such as `⨁ (i) (j), f i j`, which denotes the direct sum over both indices `i` and `j`.

DirectSum.term⨁_,_.delab_app.DirectSum definition

: Delab✝

Full source

/-- `⨁ 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`. -/
scoped[DirectSum] notation3 "⨁ "(...)", "r:(scoped f => DirectSum _ f) => r

Direct sum notation

Informal description

The notation `⨁ i, β i` represents the direct sum of abelian groups (or more generally, additive commutative monoids) indexed by a discrete type `ι`, where each `β i` is the component at index `i`. This can be extended to multiple indices as `⨁ (i) (j), β i j` for direct sums over multiple arguments.

instDecidableEqDirectSum instance

[DecidableEq ι] [∀ i, AddCommMonoid (β i)] [∀ i, DecidableEq (β i)] : DecidableEq (DirectSum ι β)

Full source

instance [DecidableEq ι] [∀ i, AddCommMonoid (β i)] [∀ i, DecidableEq (β i)] :
    DecidableEq (DirectSum ι β) :=
  inferInstanceAs <| DecidableEq (Π₀ i, β i)

Decidable Equality for Direct Sums of Additive Commutative Monoids

Informal description

For any index type $\iota$ with decidable equality and a family of additive commutative monoids $\beta_i$ (each with decidable equality), the direct sum $\bigoplus_{i} \beta_i$ has decidable equality.

DirectSum.coeFnAddMonoidHom definition

[∀ i, AddCommMonoid (β i)] : (⨁ i, β i) →+ (Π i, β i)

Full source

/-- Coercion from a `DirectSum` to a pi type is an `AddMonoidHom`. -/
def coeFnAddMonoidHom [∀ i, AddCommMonoid (β i)] : (⨁ i, β i) →+ (Π i, β i) where
  toFun x := x
  __ := DFinsupp.coeFnAddMonoidHom

Canonical inclusion of direct sum into product

Informal description

The canonical additive monoid homomorphism from the direct sum $\bigoplus_{i} \beta_i$ to the product $\prod_{i} \beta_i$, where each $\beta_i$ is an additive commutative monoid. This homomorphism maps each element of the direct sum to its underlying function in the product space.

DirectSum.coeFnAddMonoidHom_apply theorem

[∀ i, AddCommMonoid (β i)] (v : ⨁ i, β i) : coeFnAddMonoidHom β v = v

Full source

@[simp]
lemma coeFnAddMonoidHom_apply [∀ i, AddCommMonoid (β i)] (v : ⨁ i, β i) :
    coeFnAddMonoidHom β v = v :=
  rfl

Identity Property of Direct Sum Inclusion: $\text{coeFnAddMonoidHom}_\beta(v) = v$

Informal description

For any family of additive commutative monoids $\beta_i$ indexed by $i \in \iota$ and any element $v$ in the direct sum $\bigoplus_i \beta_i$, the canonical additive monoid homomorphism $\text{coeFnAddMonoidHom}_\beta$ evaluated at $v$ equals $v$ itself. In other words, the inclusion map from the direct sum to the product space is the identity on its domain.

DirectSum.instAddCommGroup instance

: AddCommGroup (DirectSum ι β)

Full source

instance : AddCommGroup (DirectSum ι β) :=
  inferInstanceAs (AddCommGroup (Π₀ i, β i))

Direct Sum as an Additive Commutative Group

Informal description

For any index type $\iota$ and family of additive commutative monoids $\beta_i$ indexed by $\iota$, the direct sum $\bigoplus_i \beta_i$ forms an additive commutative group. The group operations are defined pointwise, where addition and subtraction are performed componentwise, and the zero element is the function that is zero on all components.

DirectSum.sub_apply theorem

(g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i

Full source

@[simp]
theorem sub_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i :=
  rfl

Componentwise Subtraction in Direct Sum: $(g_1 - g_2)_i = g_1(i) - g_2(i)$

Informal description

For any two elements $g_1$ and $g_2$ in the direct sum $\bigoplus_{i} \beta_i$ and any index $i \in \iota$, the $i$-th component of their difference $(g_1 - g_2)_i$ is equal to the difference of their components $g_1(i) - g_2(i)$.

DirectSum.ext theorem

{x y : DirectSum ι β} (w : ∀ i, x i = y i) : x = y

Full source

@[ext] theorem ext {x y : DirectSum ι β} (w : ∀ i, x i = y i) : x = y :=
  DFunLike.ext _ _ w

Extensionality for Direct Sum: Componentwise Equality Implies Equality

Informal description

For any two elements $x$ and $y$ in the direct sum $\bigoplus_{i} \beta_i$, if $x(i) = y(i)$ for all indices $i \in \iota$, then $x = y$.

DirectSum.zero_apply theorem

(i : ι) : (0 : ⨁ i, β i) i = 0

Full source

@[simp]
theorem zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 :=
  rfl

Zero Component in Direct Sum Equals Zero in Each Factor

Informal description

For any index $i$ in the index type $\iota$, the $i$-th component of the zero element in the direct sum $\bigoplus_{i} \beta_i$ is equal to the zero element of $\beta_i$, i.e., $0_i = 0$.

DirectSum.add_apply theorem

(g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i

Full source

@[simp]
theorem add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i :=
  rfl

Component-wise Addition in Direct Sum: $(g_1 + g_2)_i = g_{1i} + g_{2i}$

Informal description

For any two elements $g_1, g_2$ in the direct sum $\bigoplus_{i} \beta_i$ and any index $i \in \iota$, the $i$-th component of their sum $(g_1 + g_2)_i$ equals the sum of their individual components $g_{1i} + g_{2i}$.

DirectSum.mk definition

(s : Finset ι) : (∀ i : (↑s : Set ι), β i.1) →+ ⨁ i, β i

Full source

/-- `mk β s x` is the element of `⨁ i, β i` that is zero outside `s`
and has coefficient `x i` for `i` in `s`. -/
def mk (s : Finset ι) : (∀ i : (↑s : Set ι), β i.1) →+ ⨁ i, β i where
  toFun := DFinsupp.mk s
  map_add' _ _ := DFinsupp.mk_add
  map_zero' := DFinsupp.mk_zero

Construction of direct sum element with finite support

Informal description

Given a finite subset $s$ of the index type $\iota$ and a family of elements $x_i \in \beta_i$ for each $i \in s$, the function `mk` constructs an element of the direct sum $\bigoplus_{i} \beta_i$ that equals $x_i$ for $i \in s$ and is zero elsewhere. This function is an additive monoid homomorphism.

DirectSum.of definition

(i : ι) : β i →+ ⨁ i, β i

Full source

/-- `of i` is the natural inclusion map from `β i` to `⨁ i, β i`. -/
def of (i : ι) : β i →+ ⨁ i, β i :=
  DFinsupp.singleAddHom β i

Inclusion map into direct sum

Informal description

For each index $i$ in the index type $\iota$, the function $\text{of}_i$ is the natural inclusion map from the additive commutative monoid $\beta_i$ to the direct sum $\bigoplus_{i} \beta_i$. This map preserves the additive structure, sending an element $x \in \beta_i$ to the element in the direct sum that is $x$ at index $i$ and zero elsewhere.

DirectSum.of_eq_same theorem

(i : ι) (x : β i) : (of _ i x) i = x

Full source

@[simp]
theorem of_eq_same (i : ι) (x : β i) : (of _ i x) i = x :=
  DFinsupp.single_eq_same

Component Equality in Direct Sum Inclusion

Informal description

For any index $i$ in the index type $\iota$ and any element $x \in \beta_i$, the $i$-th component of the inclusion map $\text{of}_i(x)$ in the direct sum $\bigoplus_{i} \beta_i$ is equal to $x$.

DirectSum.of_eq_of_ne theorem

(i j : ι) (x : β i) (h : i ≠ j) : (of _ i x) j = 0

Full source

theorem of_eq_of_ne (i j : ι) (x : β i) (h : i ≠ j) : (of _ i x) j = 0 :=
  DFinsupp.single_eq_of_ne h

Vanishing of Off-Diagonal Components in Direct Sum Inclusion

Informal description

For any distinct indices $i$ and $j$ in the index type $\iota$, and any element $x \in \beta_i$, the $j$-th component of the inclusion map $\text{of}_i(x)$ in the direct sum $\bigoplus_{i} \beta_i$ is zero. That is, $(\text{of}_i(x))_j = 0$ whenever $i \neq j$.

DirectSum.of_apply theorem

{i : ι} (j : ι) (x : β i) : of β i x j = if h : i = j then Eq.recOn h x else 0

Full source

lemma of_apply {i : ι} (j : ι) (x : β i) : of β i x j = if h : i = j then Eq.recOn h x else 0 :=
  DFinsupp.single_apply

Component-wise Evaluation of Direct Sum Inclusion Map

Informal description

For any index $i$ in the index type $\iota$, any index $j \in \iota$, and any element $x \in \beta_i$, the $j$-th component of the inclusion map $\text{of}_i(x)$ in the direct sum $\bigoplus_{i} \beta_i$ is given by: \[ (\text{of}_i(x))_j = \begin{cases} x & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases} \]

DirectSum.mk_apply_of_mem theorem

{s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) : mk β s f n = f ⟨n, hn⟩

Full source

theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
    mk β s f n = f ⟨n, hn⟩ := by
  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
  rw [dif_pos hn]

Component-wise Evaluation of Direct Sum Construction on Support

Informal description

For any finite subset $s$ of the index set $\iota$, any family of elements $f_i \in \beta_i$ for $i \in s$, and any index $n \in s$, the $n$-th component of the direct sum element constructed by `mk` equals $f_n$, i.e., $(\bigoplus_{i \in s} f_i)_n = f_n$.

DirectSum.mk_apply_of_not_mem theorem

{s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) : mk β s f n = 0

Full source

theorem mk_apply_of_not_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∉ s) :
    mk β s f n = 0 := by
  dsimp only [Finset.coe_sort_coe, mk, AddMonoidHom.coe_mk, ZeroHom.coe_mk, DFinsupp.mk_apply]
  rw [dif_neg hn]

Vanishing of Direct Sum Components Outside Support

Informal description

For any finite subset $s$ of the index set $\iota$, any family of elements $f_i \in \beta_i$ for $i \in s$, and any index $n \notin s$, the $n$-th component of the direct sum element constructed by `mk` is zero, i.e., $(\bigoplus_{i \in s} f_i)_n = 0$.

DirectSum.support_zero theorem

[∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅

Full source

@[simp]
theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i, β i).support = ∅ :=
  DFinsupp.support_zero

Support of Zero in Direct Sum is Empty

Informal description

For a direct sum $\bigoplus_{i} \beta_i$ of additive commutative monoids, the support of the zero element is the empty set, i.e., $\text{supp}(0) = \emptyset$.

DirectSum.support_of theorem

[∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) : (of _ i x).support = { i }

Full source

@[simp]
theorem support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) :
    (of _ i x).support = {i} :=
  DFinsupp.support_single_ne_zero h

Support of Nonzero Inclusion in Direct Sum is Singleton

Informal description

For any index $i$ in the index type $\iota$ and any nonzero element $x \in \beta_i$, the support of the inclusion map $\text{of}_i(x)$ in the direct sum $\bigoplus_{i} \beta_i$ is the singleton set $\{i\}$.

DirectSum.support_of_subset theorem

[∀ (i : ι) (x : β i), Decidable (x ≠ 0)] {i : ι} {b : β i} : (of _ i b).support ⊆ { i }

Full source

theorem support_of_subset [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] {i : ι} {b : β i} :
    (of _ i b).support ⊆ {i} :=
  DFinsupp.support_single_subset

Support of Inclusion in Direct Sum is Contained in Singleton

Informal description

For any index $i$ in the index type $\iota$ and any element $b \in \beta_i$, the support of the inclusion map $\text{of}_i(b)$ in the direct sum $\bigoplus_{i} \beta_i$ is a subset of the singleton set $\{i\}$.

DirectSum.sum_support_of theorem

[∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (x : ⨁ i, β i) : (∑ i ∈ x.support, of β i (x i)) = x

Full source

theorem sum_support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (x : ⨁ i, β i) :
    (∑ i ∈ x.support, of β i (x i)) = x :=
  DFinsupp.sum_single

Decomposition of Direct Sum Element over Its Support

Informal description

For any element $x$ in the direct sum $\bigoplus_{i} \beta_i$ of additive commutative monoids, the sum of the inclusion maps $\text{of}_i(x_i)$ over the finite support of $x$ equals $x$ itself, i.e., \[ \sum_{i \in \text{support}(x)} \text{of}_i(x_i) = x. \]

DirectSum.sum_univ_of theorem

[Fintype ι] (x : ⨁ i, β i) : ∑ i ∈ Finset.univ, of β i (x i) = x

Full source

theorem sum_univ_of [Fintype ι] (x : ⨁ i, β i) :
    ∑ i ∈ Finset.univ, of β i (x i) = x := by
  apply DFinsupp.ext (fun i ↦ ?_)
  rw [DFinsupp.finset_sum_apply]
  simp [of_apply]

Decomposition of Direct Sum Element over Finite Index Set

Informal description

For any finite index type $\iota$ and any element $x$ in the direct sum $\bigoplus_{i} \beta_i$ of additive commutative monoids, the sum of the inclusion maps $\text{of}_i(x_i)$ over all indices $i \in \iota$ equals $x$ itself, i.e., \[ \sum_{i \in \iota} \text{of}_i(x_i) = x. \]

DirectSum.mk_injective theorem

(s : Finset ι) : Function.Injective (mk β s)

Full source

theorem mk_injective (s : Finset ι) : Function.Injective (mk β s) :=
  DFinsupp.mk_injective s

Injectivity of Finite Support Construction Map for Direct Sum

Informal description

For any finite subset $s$ of the index set $\iota$, the construction map $\text{mk}_s : \prod_{i \in s} \beta_i \to \bigoplus_{i} \beta_i$ is injective. That is, if two families $(x_i)_{i \in s}$ and $(y_i)_{i \in s}$ satisfy $\text{mk}_s(x) = \text{mk}_s(y)$, then $x_i = y_i$ for all $i \in s$.

DirectSum.of_injective theorem

(i : ι) : Function.Injective (of β i)

Full source

theorem of_injective (i : ι) : Function.Injective (of β i) :=
  DFinsupp.single_injective

Injectivity of the Inclusion Map into Direct Sum

Informal description

For any index $i$ in the index type $\iota$, the inclusion map $\text{of}_i : \beta_i \to \bigoplus_{i} \beta_i$ is injective. That is, for any $x, y \in \beta_i$, if $\text{of}_i(x) = \text{of}_i(y)$, then $x = y$.

DirectSum.induction_on theorem

 {motive : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (zero : motive 0) (of : ∀ (i : ι) (x : β i), motive (of β i x))
  (add : ∀ x y, motive x → motive y → motive (x + y)) : motive x

Full source

@[elab_as_elim]
protected theorem induction_on {motive : (⨁ i, β i) → Prop} (x : ⨁ i, β i) (zero : motive 0)
    (of : ∀ (i : ι) (x : β i), motive (of β i x))
    (add : ∀ x y, motive x → motive y → motive (x + y)) : motive x := by
  apply DFinsupp.induction x zero
  intro i b f h1 h2 ih
  solve_by_elim

Induction Principle for Direct Sum of Additive Commutative Monoids

Informal description

Let $\bigoplus_{i} \beta_i$ be the direct sum of a family of additive commutative monoids $\{\beta_i\}_{i \in \iota}$. Given a predicate $\text{motive}$ on $\bigoplus_{i} \beta_i$, an element $x \in \bigoplus_{i} \beta_i$, and the following hypotheses: 1. $\text{motive}(0)$ holds (base case), 2. For every $i \in \iota$ and $x \in \beta_i$, $\text{motive}(\text{of}_i(x))$ holds (inclusion case), 3. For any $x, y \in \bigoplus_{i} \beta_i$, if $\text{motive}(x)$ and $\text{motive}(y)$ hold, then $\text{motive}(x + y)$ holds (additive closure), then $\text{motive}(x)$ holds for all $x \in \bigoplus_{i} \beta_i$.

DirectSum.addHom_ext theorem

 {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄ (H : ∀ (i : ι) (y : β i), f (of _ i y) = g (of _ i y)) : f = g

Full source

/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal. -/
theorem addHom_ext {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄
    (H : ∀ (i : ι) (y : β i), f (of _ i y) = g (of _ i y)) : f = g :=
  DFinsupp.addHom_ext H

Uniqueness of Additive Homomorphisms from Direct Sum via Generators

Informal description

Let $\gamma$ be an additive monoid with zero, and let $f, g \colon \bigoplus_{i} \beta_i \to \gamma$ be additive homomorphisms from the direct sum of a family of additive commutative monoids $\{\beta_i\}_{i \in \iota}$. If $f$ and $g$ agree on all elements of the form $\text{of}_i(y)$ for every $i \in \iota$ and $y \in \beta_i$, then $f = g$.

DirectSum.addHom_ext' theorem

 {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄ (H : ∀ i : ι, f.comp (of _ i) = g.comp (of _ i)) : f = g

Full source

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

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem addHom_ext' {γ : Type*} [AddZeroClass γ] ⦃f g : (⨁ i, β i) →+ γ⦄
    (H : ∀ i : ι, f.comp (of _ i) = g.comp (of _ i)) : f = g :=
  addHom_ext fun i => DFunLike.congr_fun <| H i

Uniqueness of Additive Homomorphisms from Direct Sum via Composition with Inclusions

Informal description

Let $\gamma$ be an additive monoid with zero, and let $f, g \colon \bigoplus_{i} \beta_i \to \gamma$ be additive homomorphisms from the direct sum of a family of additive commutative monoids $\{\beta_i\}_{i \in \iota}$. If for every $i \in \iota$, the compositions $f \circ \text{of}_i$ and $g \circ \text{of}_i$ are equal, then $f = g$.

DirectSum.toAddMonoid definition

: (⨁ i, β i) →+ γ

Full source

/-- `toAddMonoid φ` is the natural homomorphism from `⨁ i, β i` to `γ`
induced by a family `φ` of homomorphisms `β i → γ`. -/
def toAddMonoid : (⨁ i, β i) →+ γ :=
  DFinsupp.liftAddHom (β := β) φ

Universal homomorphism from direct sum to monoid

Informal description

Given an index type $\iota$ and a family of additive commutative monoids $\beta_i$ for each $i \in \iota$, the function `toAddMonoid φ` is the natural homomorphism from the direct sum $\bigoplus_{i} \beta_i$ to an additive commutative monoid $\gamma$, induced by a family $\varphi$ of homomorphisms $\beta_i \to \gamma$ for each $i \in \iota$. This homomorphism is constructed by lifting the family $\varphi$ to the direct sum via the universal property of coproducts in the category of additive commutative monoids.

DirectSum.toAddMonoid_of theorem

(i) (x : β i) : toAddMonoid φ (of β i x) = φ i x

Full source

@[simp]
theorem toAddMonoid_of (i) (x : β i) : toAddMonoid φ (of β i x) = φ i x :=
  DFinsupp.liftAddHom_apply_single φ i x

Universal Property of Direct Sum: Evaluation on Generators

Informal description

For any index $i$ and element $x \in \beta_i$, the image of the inclusion $\text{of}_i(x)$ under the universal homomorphism $\text{toAddMonoid}\,\varphi$ equals $\varphi_i(x)$, i.e., $\text{toAddMonoid}\,\varphi (\text{of}_i(x)) = \varphi_i(x)$.

DirectSum.toAddMonoid.unique theorem

(f : ⨁ i, β i) : ψ f = toAddMonoid (fun i => ψ.comp (of β i)) f

Full source

theorem toAddMonoid.unique (f : ⨁ i, β i) : ψ f = toAddMonoid (fun i => ψ.comp (of β i)) f := by
  congr
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` applies addHom_ext' here, which isn't what we want.
  apply DFinsupp.addHom_ext'
  simp [toAddMonoid, of]

Uniqueness of Homomorphism from Direct Sum via Universal Property

Informal description

For any homomorphism $\psi$ from the direct sum $\bigoplus_i \beta_i$ to an additive commutative monoid $\gamma$, and for any element $f$ in the direct sum, $\psi(f)$ is equal to the evaluation of the universal homomorphism $\text{toAddMonoid}$ applied to the family of homomorphisms $\psi \circ \text{of}_i$ at $f$. That is, $\psi(f) = \text{toAddMonoid}\,(\lambda i, \psi \circ \text{of}_i)\,(f)$.

DirectSum.toAddMonoid_injective theorem

: Injective (toAddMonoid : (∀ i, β i →+ γ) → (⨁ i, β i) →+ γ)

Full source

lemma toAddMonoid_injective : Injective (toAddMonoid : (∀ i, β i →+ γ) → (⨁ i, β i) →+ γ) :=
  DFinsupp.liftAddHom.injective

Injectivity of the Universal Homomorphism from Direct Sum

Informal description

The homomorphism `toAddMonoid` from the family of additive group homomorphisms $(\beta_i \to+ \gamma)_{i \in \iota}$ to the homomorphism $\bigoplus_i \beta_i \to+ \gamma$ is injective. In other words, if two families of homomorphisms induce the same homomorphism on the direct sum, then they must be equal.

DirectSum.toAddMonoid_inj theorem

{f g : ∀ i, β i →+ γ} : toAddMonoid f = toAddMonoid g ↔ f = g

Full source

@[simp] lemma toAddMonoid_inj {f g : ∀ i, β i →+ γ} : toAddMonoidtoAddMonoid f = toAddMonoid g ↔ f = g :=
  toAddMonoid_injective.eq_iff

Injectivity Criterion for the Universal Homomorphism from Direct Sum: $\text{toAddMonoid}\,f = \text{toAddMonoid}\,g \leftrightarrow f = g$

Informal description

For any two families of additive group homomorphisms $f, g \colon (\beta_i \to+ \gamma)_{i \in \iota}$, the induced homomorphisms $\text{toAddMonoid}\,f$ and $\text{toAddMonoid}\,g$ from the direct sum $\bigoplus_i \beta_i$ to $\gamma$ are equal if and only if the families $f$ and $g$ are equal.

DirectSum.fromAddMonoid definition

: (⨁ i, γ →+ β i) →+ γ →+ ⨁ i, β i

Full source

/-- `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. -/
def fromAddMonoid : (⨁ i, γ →+ β i) →+ γ →+ ⨁ i, β i :=
  toAddMonoid fun i => AddMonoidHom.compHom (of β i)

Homomorphism from direct sum of homomorphisms to homomorphism into direct sum

Informal description

The function `fromAddMonoid φ` is the natural homomorphism from the direct sum $\bigoplus_{i} (\gamma \to+ \beta_i)$ to the homomorphism space $\gamma \to+ \bigoplus_{i} \beta_i$, induced by a family $\varphi$ of homomorphisms $\gamma \to \beta_i$ for each $i$. Note that this is not an isomorphism, as not every homomorphism $\gamma \to+ \bigoplus_{i} \beta_i$ arises in this way.

DirectSum.fromAddMonoid_of theorem

(i : ι) (f : γ →+ β i) : fromAddMonoid (of _ i f) = (of _ i).comp f

Full source

@[simp]
theorem fromAddMonoid_of (i : ι) (f : γ →+ β i) : fromAddMonoid (of _ i f) = (of _ i).comp f := by
  rw [fromAddMonoid, toAddMonoid_of]
  rfl

Compatibility of $\text{fromAddMonoid}$ with inclusions and compositions

Informal description

For any index $i \in \iota$ and any additive monoid homomorphism $f \colon \gamma \to \beta_i$, the homomorphism $\text{fromAddMonoid}$ applied to the inclusion $\text{of}_i(f)$ equals the composition of the inclusion $\text{of}_i$ with $f$. In symbols: $\text{fromAddMonoid}(\text{of}_i(f)) = \text{of}_i \circ f$.

DirectSum.fromAddMonoid_of_apply theorem

(i : ι) (f : γ →+ β i) (x : γ) : fromAddMonoid (of _ i f) x = of _ i (f x)

Full source

theorem fromAddMonoid_of_apply (i : ι) (f : γ →+ β i) (x : γ) :
    fromAddMonoid (of _ i f) x = of _ i (f x) := by
      rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]

Evaluation of $\text{fromAddMonoid}$ on Inclusions and Elements

Informal description

For any index $i \in \iota$, any additive monoid homomorphism $f \colon \gamma \to \beta_i$, and any element $x \in \gamma$, the evaluation of the homomorphism $\text{fromAddMonoid}(\text{of}_i(f))$ at $x$ equals the inclusion $\text{of}_i(f(x))$ in the direct sum $\bigoplus_i \beta_i$. In symbols: $\text{fromAddMonoid}(\text{of}_i(f))(x) = \text{of}_i(f(x))$.

DirectSum.setToSet definition

(S T : Set ι) (H : S ⊆ T) : (⨁ i : S, β i) →+ ⨁ i : T, β i

Full source

/-- `setToSet β S T h` is the natural homomorphism `⨁ (i : S), β i → ⨁ (i : T), β i`,
where `h : S ⊆ T`. -/
def setToSet (S T : Set ι) (H : S ⊆ T) : (⨁ i : S, β i) →+ ⨁ i : T, β i :=
  toAddMonoid fun i => of (fun i : Subtype T => β i) ⟨↑i, H i.2⟩

Inclusion homomorphism between direct sums over nested index sets

Informal description

Given two sets $S$ and $T$ of indices with $S \subseteq T$, the function $\text{setToSet}$ is the natural additive monoid homomorphism from the direct sum $\bigoplus_{i \in S} \beta_i$ to the direct sum $\bigoplus_{i \in T} \beta_i$. This homomorphism is induced by the inclusion maps of each $\beta_i$ for $i \in S$ into the larger direct sum over $T$.

DirectSum.unique instance

[∀ i, Subsingleton (β i)] : Unique (⨁ i, β i)

Full source

instance unique [∀ i, Subsingleton (β i)] : Unique (⨁ i, β i) :=
  DFinsupp.unique

Uniqueness of Direct Sum of Subsingleton Monoids

Informal description

For any family of additive commutative monoids $\beta_i$ where each $\beta_i$ has at most one element (i.e., is a subsingleton), the direct sum $\bigoplus_i \beta_i$ has exactly one element (i.e., is a unique type).

DirectSum.uniqueOfIsEmpty instance

[IsEmpty ι] : Unique (⨁ i, β i)

Full source

/-- A direct sum over an empty type is trivial. -/
instance uniqueOfIsEmpty [IsEmpty ι] : Unique (⨁ i, β i) :=
  DFinsupp.uniqueOfIsEmpty

Uniqueness of Direct Sum over Empty Index Type

Informal description

For any empty index type $\iota$ and family of additive commutative monoids $\beta_i$ indexed by $\iota$, the direct sum $\bigoplus_{i} \beta_i$ is uniquely determined (i.e., it is a singleton type).

DirectSum.equivCongrLeft definition

(h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k)

Full source

/-- Reindexing terms of a direct sum. -/
def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) :=
  { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv}

Additive equivalence of direct sums under index bijection

Informal description

Given an equivalence $h : \iota \simeq \kappa$ between index types $\iota$ and $\kappa$, there is an additive equivalence between the direct sum $\bigoplus_{i \in \iota} \beta_i$ and the direct sum $\bigoplus_{k \in \kappa} \beta_{h^{-1}(k)}$. This equivalence reindexes the components of the direct sum according to the bijection $h$.

DirectSum.equivCongrLeft_apply theorem

(h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : equivCongrLeft h f k = f (h.symm k)

Full source

@[simp]
theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) :
    equivCongrLeft h f k = f (h.symm k) := by
  exact DFinsupp.comapDomain'_apply _ h.right_inv _ _

Component Formula for Reindexed Direct Sum via Bijection

Informal description

Given a bijection $h : \iota \simeq \kappa$ between index types $\iota$ and $\kappa$, for any element $f$ of the direct sum $\bigoplus_{i \in \iota} \beta_i$ and any index $k \in \kappa$, the $k$-th component of the reindexed direct sum $\bigoplus_{k \in \kappa} \beta_{h^{-1}(k)}$ under the equivalence `equivCongrLeft h` is equal to the $h^{-1}(k)$-th component of $f$.

DirectSum.addEquivProdDirectSum definition

: (⨁ i, α i) ≃+ α none × ⨁ i, α (some i)

Full source

/-- Isomorphism obtained by separating the term of index `none` of a direct sum over `Option ι`. -/
@[simps!]
noncomputable def addEquivProdDirectSum : (⨁ i, α i) ≃+ α none × ⨁ i, α (some i) :=
  { DFinsupp.equivProdDFinsupp with map_add' := DFinsupp.equivProdDFinsupp_add }

Direct sum decomposition over `Option ι`

Informal description

The additive equivalence between the direct sum $\bigoplus_{i \in \text{Option} \iota} \alpha_i$ and the product $\alpha_{\text{none}} \times \bigoplus_{i \in \iota} \alpha_{\text{some } i}$. This isomorphism separates the term of index `none` from the rest of the direct sum over `Option ι`.

DirectSum.sigmaCurry definition

: (⨁ i : Σ _i, _, δ i.1 i.2) →+ ⨁ (i) (j), δ i j

Full source

/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`. -/
def sigmaCurry : (⨁ i : Σ _i, _, δ i.1 i.2) →+ ⨁ (i) (j), δ i j where
  toFun := DFinsupp.sigmaCurry (δ := δ)
  map_zero' := DFinsupp.sigmaCurry_zero
  map_add' f g := DFinsupp.sigmaCurry_add f g

Curry homomorphism for direct sums

Informal description

The natural additive homomorphism from the direct sum $\bigoplus_{(i : \Sigma_i \alpha_i)} \delta_{i.1 i.2}$ to the iterated direct sum $\bigoplus_i \bigoplus_j \delta_{i j}$, which maps an element of the sigma-type direct sum to its curried form.

DirectSum.sigmaCurry_apply theorem

(f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) : sigmaCurry f i j = f ⟨i, j⟩

Full source

@[simp]
theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) :
    sigmaCurry f i j = f ⟨i, j⟩ :=
  DFinsupp.sigmaCurry_apply (δ := δ) _ i j

Component Formula for Curried Direct Sum

Informal description

For any element $f$ in the direct sum $\bigoplus_{(i,j) \in \Sigma_i \alpha_i} \delta_{i j}$ and any indices $i \in \iota$ and $j \in \alpha_i$, the $(i,j)$-th component of the curried direct sum $\operatorname{sigmaCurry}(f)$ equals the value of $f$ at the pair $\langle i, j \rangle$, i.e., \[ \operatorname{sigmaCurry}(f)_{i j} = f_{\langle i, j \rangle}. \]

DirectSum.sigmaUncurry definition

: (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2

Full source

/-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
`curry`. -/
def sigmaUncurry : (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2 where
  toFun := DFinsupp.sigmaUncurry
  map_zero' := DFinsupp.sigmaUncurry_zero
  map_add' := DFinsupp.sigmaUncurry_add

Uncurry homomorphism for direct sums

Informal description

The natural additive homomorphism from the direct sum $\bigoplus_{(i,j)} \delta_{i j}$ to the direct sum $\bigoplus_{(i : \Sigma_i \alpha_i)} \delta_{i.1 i.2}$, which is the inverse of the `curry` operation. This map takes an element of the iterated direct sum and flattens it into a direct sum over the sigma type.

DirectSum.sigmaUncurry_apply theorem

(f : ⨁ (i) (j), δ i j) (i : ι) (j : α i) : sigmaUncurry f ⟨i, j⟩ = f i j

Full source

@[simp]
theorem sigmaUncurry_apply (f : ⨁ (i) (j), δ i j) (i : ι) (j : α i) :
    sigmaUncurry f ⟨i, j⟩ = f i j :=
  DFinsupp.sigmaUncurry_apply f i j

Component Formula for Uncurried Direct Sum

Informal description

For any element $f$ in the direct sum $\bigoplus_{i,j} \delta_{i j}$ and any indices $i \in \iota$, $j \in \alpha_i$, the value of the uncurried direct sum $\operatorname{sigmaUncurry}(f)$ at the pair $\langle i, j \rangle$ equals the $(i,j)$-th component of $f$, i.e., \[ \operatorname{sigmaUncurry}(f)_{\langle i, j \rangle} = f_{i j}. \]

DirectSum.sigmaCurryEquiv definition

: (⨁ i : Σ _i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j

Full source

/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`. -/
def sigmaCurryEquiv : (⨁ i : Σ _i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j :=
  { sigmaCurry, DFinsupp.sigmaCurryEquiv with }

Curry equivalence for direct sums

Informal description

The natural additive equivalence between the direct sum $\bigoplus_{(i : \Sigma_i \alpha_i)} \delta_{i.1 i.2}$ and the iterated direct sum $\bigoplus_i \bigoplus_j \delta_{i j}$. This equivalence consists of the currying homomorphism and its inverse, establishing an isomorphism between the two direct sum representations.

DirectSum.coeAddMonoidHom definition

 {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) : (⨁ i, A i) →+ M

Full source

/-- 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`. -/
protected def coeAddMonoidHom {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
    [AddSubmonoidClass S M] (A : ι → S) : (⨁ i, A i) →+ M :=
  toAddMonoid fun i => AddSubmonoidClass.subtype (A i)

Canonical inclusion homomorphism from direct sum to monoid

Informal description

Given an index type $\iota$, an additive commutative monoid $M$, and a family of additive submonoids $A_i \subseteq M$ indexed by $\iota$, the function `coeAddMonoidHom` is the canonical additive monoid homomorphism from the direct sum $\bigoplus_i A_i$ to $M$. This homomorphism is constructed by summing the inclusions of each component $A_i$ into $M$. More precisely, for any element $x$ in the direct sum $\bigoplus_i A_i$, the homomorphism evaluates to the sum of the underlying elements in $M$ corresponding to the components of $x$.

DirectSum.coeAddMonoidHom_eq_dfinsuppSum theorem

 [DecidableEq ι] {M S : Type*} [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 => (fun x : A i => ↑x)

Full source

theorem coeAddMonoidHom_eq_dfinsuppSum [DecidableEq ι]
    {M S : Type*} [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 => (fun x : A i => ↑x) := by
  simp only [DirectSum.coeAddMonoidHom, toAddMonoid, DFinsupp.liftAddHom, AddEquiv.coe_mk,
    Equiv.coe_fn_mk]
  exact DFinsupp.sumAddHom_apply _ x

Canonical Inclusion Homomorphism Equals Component-wise Sum in Direct Sum

Informal description

Let $\iota$ be a decidable index type, $M$ an additive commutative monoid with decidable equality, and $S$ a set-like structure on $M$ with an additive submonoid class. Given a family of submonoids $A : \iota \to S$, for any element $x$ in the direct sum $\bigoplus_i A_i$, the image of $x$ under the canonical inclusion homomorphism $\text{coeAddMonoidHom}_A$ is equal to the sum of the underlying elements in $M$ corresponding to the components of $x$. That is, $$\text{coeAddMonoidHom}_A(x) = \sum_{i} x_i,$$ where $x_i \in A_i$ is the $i$-th component of $x$ and the sum is taken over the support of $x$.

DirectSum.coeAddMonoidHom_of theorem

 {M S : Type*} [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

Full source

@[simp]
theorem coeAddMonoidHom_of {M S : Type*} [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 :=
  toAddMonoid_of _ _ _

Canonical Inclusion Homomorphism Evaluates to Identity on Generators

Informal description

Let $\iota$ be a decidable index type, $M$ an additive commutative monoid, and $S$ a set-like structure on $M$ with an additive submonoid class. Given a family of submonoids $A : \iota \to S$, for any index $i \in \iota$ and any element $x \in A_i$, the canonical inclusion homomorphism $\text{coeAddMonoidHom}\,A$ applied to the direct sum inclusion $\text{of}_i(x)$ equals $x$. That is, $$\text{coeAddMonoidHom}\,A (\text{of}_i(x)) = x.$$

DirectSum.coe_of_apply theorem

 {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : A i) :
  (of (fun i ↦ { x // x ∈ A i }) i x j : M) = if i = j then x else 0

Full source

theorem coe_of_apply {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
    [AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : A i) :
    (of (fun i ↦ {x // x ∈ A i}) i x j : M) = if i = j then x else 0 := by
  obtain rfl | h := Decidable.eq_or_ne i j
  · rw [DirectSum.of_eq_same, if_pos rfl]
  · rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]

Component-wise Evaluation of Direct Sum Inclusion Map

Informal description

Let $\iota$ be a decidable index type, $M$ an additive commutative monoid, and $S$ a set-like structure on $M$ with an additive submonoid class. Given a family of submonoids $A : \iota \to S$, for any indices $i, j \in \iota$ and any element $x \in A_i$, the $j$-th component of the inclusion map $\text{of}_i(x)$ in the direct sum $\bigoplus_{i} A_i$ is equal to $x$ when $i = j$ and $0$ otherwise. That is, $$(\text{of}_i(x))_j = \begin{cases} x & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases}$$

DirectSum.IsInternal definition

{M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] (A : ι → S) : Prop

Full source

/-- 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`. -/
def IsInternal {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M]
    [AddSubmonoidClass S M] (A : ι → S) : Prop :=
  Function.Bijective (DirectSum.coeAddMonoidHom A)

Internal direct sum of submonoids

Informal description

Given an index type $\iota$, an additive commutative monoid $M$, and a family of additive submonoids $A_i \subseteq M$ indexed by $\iota$, we say the direct sum $\bigoplus_i A_i$ is *internal* when the canonical additive monoid homomorphism from $\bigoplus_i A_i$ to $M$ (which sums the components) is bijective.

DirectSum.IsInternal.addSubmonoid_iSup_eq_top theorem

{M : Type*} [DecidableEq ι] [AddCommMonoid M] (A : ι → AddSubmonoid M) (h : IsInternal A) : iSup A = ⊤

Full source

theorem IsInternal.addSubmonoid_iSup_eq_top {M : Type*} [DecidableEq ι] [AddCommMonoid M]
    (A : ι → AddSubmonoid M) (h : IsInternal A) : iSup A = ⊤ := by
  rw [AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, AddMonoidHom.mrange_eq_top]
  exact Function.Bijective.surjective h

Supremum of Submonoids in Internal Direct Sum Equals Top Submonoid

Informal description

Let $\iota$ be a decidable index type and $M$ an additive commutative monoid. Given a family of additive submonoids $A_i \subseteq M$ indexed by $\iota$, if the direct sum $\bigoplus_i A_i$ is internal (i.e., the canonical homomorphism from $\bigoplus_i A_i$ to $M$ is bijective), then the supremum of the submonoids $A_i$ equals the top submonoid of $M$. In other words, $\bigsqcup_i A_i = \top$.

DirectSum.support_subset theorem

 [DecidableEq ι] [DecidableEq M] (A : ι → S) (x : DirectSum ι fun i => A i) :
  (Function.support fun i => (x i : M)) ⊆ ↑(DFinsupp.support x)

Full source

theorem support_subset [DecidableEq ι] [DecidableEq M] (A : ι → S) (x : DirectSum ι fun i => A i) :
    (Function.support fun i => (x i : M)) ⊆ ↑(DFinsupp.support x) := by
  intro m
  simp only [Function.mem_support, Finset.mem_coe, DFinsupp.mem_support_toFun, not_imp_not,
    ZeroMemClass.coe_eq_zero, imp_self]

Support Inclusion for Direct Sum Elements

Informal description

Let $\iota$ be a type with decidable equality, $M$ a type with decidable equality, and $S$ a set-like structure on $M$ with additive submonoid properties. Given a family $A : \iota \to S$ and an element $x$ of the direct sum $\bigoplus_{i} A_i$, the support of the function $i \mapsto (x_i : M)$ is contained in the support of $x$ viewed as a dependent function with finite support.

DirectSum.finite_support theorem

(A : ι → S) (x : DirectSum ι fun i => A i) : (Function.support fun i => (x i : M)).Finite

Full source

theorem finite_support (A : ι → S) (x : DirectSum ι fun i => A i) :
    (Function.support fun i => (x i : M)).Finite := by
  classical
  exact (DFinsupp.support x).finite_toSet.subset (DirectSum.support_subset _ x)

Finite Support Property of Direct Sum Elements

Informal description

For any family of additive submonoids $A_i$ indexed by $i \in \iota$ and any element $x$ of the direct sum $\bigoplus_{i} A_i$, the support of the function $i \mapsto x_i$ (where $x_i$ is the $i$-th component of $x$) is finite.

DirectSum.map definition

: (⨁ i, α i) →+ ⨁ i, β i

Full source

/-- create a homomorphism from `⨁ i, α i` to `⨁ i, β i` by giving the component-wise map `f`. -/
def map : (⨁ i, α i) →+ ⨁ i, β i := DFinsupp.mapRange.addMonoidHom f

Component-wise homomorphism of direct sums

Informal description

Given a family of additive commutative monoids $\alpha_i$ and $\beta_i$ indexed by $\iota$, and a family of additive monoid homomorphisms $f_i : \alpha_i \to \beta_i$, the function $\text{map} f$ constructs a homomorphism from the direct sum $\bigoplus_i \alpha_i$ to $\bigoplus_i \beta_i$ by applying $f_i$ component-wise.

DirectSum.map_of theorem

[DecidableEq ι] (i : ι) (x : α i) : map f (of α i x) = of β i (f i x)

Full source

@[simp] lemma map_of [DecidableEq ι] (i : ι) (x : α i) : map f (of α i x) = of β i (f i x) :=
  DFinsupp.mapRange_single (hf := fun _ => map_zero _)

Component-wise Homomorphism Preserves Inclusion in Direct Sum

Informal description

For any index $i$ in a decidable index type $\iota$, and any element $x$ in the additive commutative monoid $\alpha_i$, the component-wise homomorphism $\text{map} f$ applied to the inclusion $\text{of}_i(x)$ in the direct sum $\bigoplus_i \alpha_i$ equals the inclusion $\text{of}_i(f_i(x))$ in the direct sum $\bigoplus_i \beta_i$. In other words, $\text{map} f (\text{of}_i(x)) = \text{of}_i(f_i(x))$.

DirectSum.map_apply theorem

(i : ι) (x : ⨁ i, α i) : map f x i = f i (x i)

Full source

@[simp] lemma map_apply (i : ι) (x : ⨁ i, α i) : map f x i = f i (x i) :=
  DFinsupp.mapRange_apply (hf := fun _ => map_zero _) _ _ _

Component-wise Evaluation of Direct Sum Homomorphism

Informal description

For any index $i$ in the index type $\iota$ and any element $x$ in the direct sum $\bigoplus_i \alpha_i$, the $i$-th component of the homomorphism $\text{map}\, f$ applied to $x$ equals the homomorphism $f_i$ applied to the $i$-th component of $x$. That is, $(\text{map}\, f\, x)_i = f_i(x_i)$.

DirectSum.map_id theorem

: (map (fun i ↦ AddMonoidHom.id (α i))) = AddMonoidHom.id (⨁ i, α i)

Full source

@[simp] lemma map_id :
    (map (fun i ↦ AddMonoidHom.id (α i))) = AddMonoidHom.id (⨁ i, α i) :=
  DFinsupp.mapRange.addMonoidHom_id

Identity Homomorphism on Direct Sum via Component-wise Identity

Informal description

The component-wise homomorphism induced by the identity homomorphism on each $\alpha_i$ is equal to the identity homomorphism on the direct sum $\bigoplus_i \alpha_i$. That is, $\text{map} (\lambda i, \text{id}_{\alpha_i}) = \text{id}_{\bigoplus_i \alpha_i}$.

DirectSum.map_comp theorem

 {γ : ι → Type*} [∀ i, AddCommMonoid (γ i)] (g : ∀ (i : ι), β i →+ γ i) :
  (map (fun i ↦ (g i).comp (f i))) = (map g).comp (map f)

Full source

@[simp] lemma map_comp {γ : ι → Type*} [∀ i, AddCommMonoid (γ i)]
    (g : ∀ (i : ι), β i →+ γ i) :
    (map (fun i ↦ (g i).comp (f i))) = (map g).comp (map f) :=
  DFinsupp.mapRange.addMonoidHom_comp _ _

Composition of Component-wise Homomorphisms on Direct Sums

Informal description

Let $\iota$ be an index type, and let $\alpha_i$, $\beta_i$, and $\gamma_i$ be families of additive commutative monoids indexed by $\iota$. Given a family of additive monoid homomorphisms $f_i \colon \alpha_i \to \beta_i$ and $g_i \colon \beta_i \to \gamma_i$ for each $i \in \iota$, the composition of the induced maps on direct sums satisfies: \[ \text{map} \left( \lambda i, g_i \circ f_i \right) = \text{map}\, g \circ \text{map}\, f. \]

DirectSum.map_injective theorem

: Function.Injective (map f) ↔ ∀ i, Function.Injective (f i)

Full source

lemma map_injective : Function.InjectiveFunction.Injective (map f) ↔ ∀ i, Function.Injective (f i) := by
  classical exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Injectivity of Direct Sum Map via Component-wise Injectivity

Informal description

The homomorphism $\text{map}\, f \colon \bigoplus_i \alpha_i \to \bigoplus_i \beta_i$ is injective if and only if for every index $i$, the component homomorphism $f_i \colon \alpha_i \to \beta_i$ is injective.

DirectSum.map_surjective theorem

: Function.Surjective (map f) ↔ (∀ i, Function.Surjective (f i))

Full source

lemma map_surjective : Function.SurjectiveFunction.Surjective (map f) ↔ (∀ i, Function.Surjective (f i)) := by
  classical exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Surjectivity of Direct Sum Map via Component-wise Surjectivity

Informal description

The map $\text{map}\, f$ from the direct sum $\bigoplus_i \alpha_i$ to the direct sum $\bigoplus_i \beta_i$ is surjective if and only if for every index $i$, the component map $f_i \colon \alpha_i \to \beta_i$ is surjective.

DirectSum.map_eq_iff theorem

(x y : ⨁ i, α i) : map f x = map f y ↔ ∀ i, f i (x i) = f i (y i)

Full source

lemma map_eq_iff (x y : ⨁ i, α i) :
    mapmap f x = map f y ↔ ∀ i, f i (x i) = f i (y i) := by
  simp_rw [DirectSum.ext_iff, map_apply]

Component-wise Equality Criterion for Direct Sum Map: $\text{map}\, f\, x = \text{map}\, f\, y \leftrightarrow \forall i, f_i(x_i) = f_i(y_i)$

Informal description

For any two elements $x$ and $y$ in the direct sum $\bigoplus_i \alpha_i$, the equality $\text{map}\, f\, x = \text{map}\, f\, y$ holds if and only if for every index $i$, the component-wise evaluation satisfies $f_i(x_i) = f_i(y_i)$.

DirectSum.addEquivProd definition

 {ι : Type*} [Fintype ι] (G : ι → Type*) [(i : ι) → AddCommMonoid (G i)] : DirectSum ι G ≃+ ((i : ι) → G i)

Full source

/-- The canonical isomorphism of a finite direct sum of additive commutative monoids
and the corresponding finite product. -/
def DirectSum.addEquivProd {ι : Type*} [Fintype ι] (G : ι → Type*) [(i : ι) → AddCommMonoid (G i)] :
    DirectSumDirectSum ι G ≃+ ((i : ι) → G i) :=
  ⟨DFinsupp.equivFunOnFintype, fun g h ↦ funext fun _ ↦ by
    simp only [DFinsupp.equivFunOnFintype, Equiv.toFun_as_coe, Equiv.coe_fn_mk, add_apply,
      Pi.add_apply]⟩

Canonical isomorphism between direct sum and product of additive commutative monoids

Informal description

For a finite index type $\iota$ and a family of additive commutative monoids $G_i$ indexed by $\iota$, there is a canonical isomorphism of additive commutative monoids between the direct sum $\bigoplus_{i} G_i$ and the product $\prod_{i} G_i$. This isomorphism maps an element of the direct sum to its corresponding tuple in the product.

Mathlib.Algebra.DirectSum.Basic

Notation

References