DirectSum.Decomposition.isInternal
theorem DirectSum.Decomposition.isInternal :
∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
[inst_2 : SetLike σ M] [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ],
DirectSum.IsInternal ℳ
The theorem `DirectSum.Decomposition.isInternal` asserts that for any type `ι`, any type `M` which forms an additive commutative monoid, and any type `σ` that is a set-like of `M` and forms an additive submonoid, given a function `ℳ` from `ι` to `σ` and provided that `ℳ` is a DirectSum.Decomposition, `ℳ` is also internal in the sense of forming a Direct Sum. The equality of elements in `ι` is required to be decidable.
More concisely: Given an additive commutative monoid `M`, a set-like submonoid `σ`, a decidably-equivalent relation on `ι`, and a Direct Sum Decomposition `ℳ` from `ι` to `σ` of `M`, `ℳ` is an internal Direct Sum decomposition.
|
DirectSum.decompose_lhom_ext
theorem DirectSum.decompose_lhom_ext :
∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R]
[inst_2 : AddCommMonoid M] [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst : DirectSum.Decomposition ℳ]
{N : Type u_5} [inst : AddCommMonoid N] [inst_4 : Module R N] ⦃f g : M →ₗ[R] N⦄,
(∀ (i : ι), f ∘ₗ (ℳ i).subtype = g ∘ₗ (ℳ i).subtype) → f = g
This theorem, `DirectSum.decompose_lhom_ext`, states that for any types `ι`, `R`, `M` and `N`, given `ι` has decidable equality, `R` is a semiring, `M` is an additive commutative monoid that is a module over `R`, `N` is also an additive commutative monoid that is a module over `R`, and there exists a decomposition `ℳ` for `M`, if two linear maps `f` and `g` from `M` to `N` agree for each piece in the decomposition of `M`, then `f` and `g` must be the same linear map. That is, if the linear maps `f` and `g` map each submodule in the decomposition of `M` identically, then `f` is identical to `g`.
More concisely: If `M` is a decomposable additive commutative `R`-module, `N` is an additive commutative `R`-module with decidable equality, and two linear maps `f` and `g` from `M` to `N` agree on each submodule in the decomposition of `M`, then `f` is equal to `g`.
|
DirectSum.decompose_symm_of
theorem DirectSum.decompose_symm_of :
∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
[inst_2 : SetLike σ M] [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {i : ι}
(x : ↥(ℳ i)), (DirectSum.decompose ℳ).symm ((DirectSum.of (fun i => ↥(ℳ i)) i) x) = ↑x
The theorem `DirectSum.decompose_symm_of` expresses the property that for any type `ι`, with `M` being an additive commutative monoid and `σ` behaving like a set of `M` with additive submonoid structure, and for any function `ℳ : ι → σ` that decomposes the direct sum, and for any index `ι` with `x` being an element of `ℳ(i)`, the inverse of the function `DirectSum.decompose ℳ` applied to the direct sum of `x` over the index `i` gives back the original element `x`. In other words, it states that the decomposition of the direct sum followed by its inverse transformation leads back to the original element, thus showing that these transformations are inverses of each other for the given structures and conditions.
More concisely: Given a commutative additive monoid `M` and a set `σ` with additive submonoid structure and a function `ℳ : ι → σ` decomposing the direct sum, the inverse of `DirectSum.decompose ℳ` applied to the direct sum of an element `x` in `ℳ(i)` yields back the original element `x`.
|