DirectSum.addHom_ext'
theorem DirectSum.addHom_ext' :
∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1}
[inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι), f.comp (DirectSum.of (fun i => β i) i) = g.comp (DirectSum.of (fun i => β i) i)) → f = g
This theorem states that if we have two additive homomorphisms `f` and `g` from the direct sum `⨁ i, β i` to another additive monoid `γ`, and for every index `i` in the direct sum, `f` and `g` are equal when composed with the natural inclusion map from `β i` to `⨁ i, β i` (i.e., `f.comp (DirectSum.of (fun i => β i) i) = g.comp (DirectSum.of (fun i => β i) i)`), then `f` and `g` are equal. This is an extensionality lemma for additive homomorphisms from the direct sum of additive commutative monoids.
More concisely: If two additive homomorphisms from the direct sum of additive commutative monoids to an additive monoid agree on the inclusion maps, then they are equal.
|
DirectSum.toAddMonoid_of
theorem DirectSum.toAddMonoid_of :
∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u₁}
[inst_1 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
(DirectSum.toAddMonoid φ) ((DirectSum.of β i) x) = (φ i) x
The theorem `DirectSum.toAddMonoid_of` states that for any type `ι` with decidable equality, a family of types `β` indexed by `ι` each equipped with an additive commutative monoid structure, another type `γ` with an additive commutative monoid structure, a family `φ` of homomorphisms from `β i` to `γ` for each `i` in `ι`, and any element `x` of type `β i` for some `i`, applying the natural homomorphism from the direct sum over `ι` of `β i` to `γ` (given by `DirectSum.toAddMonoid φ`) to the result of including `x` in the direct sum (given by `DirectSum.of β i x`) is the same as directly applying the homomorphism `φ i` to `x`.
In other words, when we include an element into a direct sum and then map it with the homomorphism built from the direct sum, it is the same as if we directly map the element with the corresponding homomorphism.
More concisely: For any type with decidable equality, a family of additive commutative monoids indexed by the type, another additive commutative monoid, a family of homomorphisms between each pair, and an element from one monoid, the homomorphism built from the direct sum applied to the element is equivalent to directly applying the homomorphism to the element.
|
DirectSum.addHom_ext
theorem DirectSum.addHom_ext :
∀ {ι : Type v} [dec_ι : DecidableEq ι] {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] {γ : Type u_1}
[inst_1 : AddMonoid γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
(∀ (i : ι) (y : β i), f ((DirectSum.of (fun i => β i) i) y) = g ((DirectSum.of (fun i => β i) i) y)) → f = g
The theorem `DirectSum.addHom_ext` states that for a type `ι` with decidable equality, a type family `β` indexed over `ι` where each `β i` is an additive commutative monoid, and another type `γ` which is an additive monoid, if we have two additive homomorphisms `f` and `g` from the direct sum of `β i` over `i` to `γ` such that for each `i` in `ι` and each `y` in `β i`, `f` and `g` are equal when applied to the natural inclusion of `y` from `β i` to the direct sum, then `f` and `g` are equal homomorphisms. In essence, this theorem asserts that two additive homomorphisms between such structures are equal if they agree on the images of the elements of each `β i` under the natural inclusion map into the direct sum.
More concisely: If `f` and `g` are additive homomorphisms from the direct sum of an additive commutative monoid type family `β i` over `ι` to an additive monoid `γ`, and they agree on the images of each element `y` in `β i` under the natural inclusion map, then `f` and `g` are equal.
|