Submodule.iSup_eq_toSubmodule_range
theorem Submodule.iSup_eq_toSubmodule_range :
∀ {ι : Type u_1} {S : Type u_3} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι]
[inst_2 : CommSemiring S] [inst_3 : Semiring R] [inst_4 : Algebra S R] (A : ι → Submodule S R)
[inst_5 : SetLike.GradedMonoid A], ⨆ i, A i = Subalgebra.toSubmodule (DirectSum.coeAlgHom A).range
The theorem `Submodule.iSup_eq_toSubmodule_range` states that for given types `ι`, `S`, and `R`, under the conditions that `ι` has a decidable equality and is an additive monoid, `S` is a commutative semiring, `R` is a semiring, and `S` is an algebra over `R`, if we have a function `A` mapping `ι` to a submodule of `S` and `R` such that these submodules form a graded monoid, then the supremum of these submodules `A i` (denoted `⨆ i, A i`) is a subalgebra and is equal to the range of the canonical algebra isomorphism (constructed by `DirectSum.coeAlgHom`) from the direct sum of the submodules `A i` to `R`.
More concisely: Given an additive monoid `ι` with decidable equality, a commutative semiring `S` that is an algebra over semiring `R`, and a function `A : ι → Submodule S R` such that the submodules `A i` form a graded monoid, then `⨆ i, A i` is the range of the canonical algebra homomorphism from the direct sum of the `A i` to `R`.
|
DirectSum.coeRingHom_of
theorem DirectSum.coeRingHom_of :
∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
[inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A] (i : ι)
(x : ↥(A i)), (DirectSum.coeRingHom A) ((DirectSum.of (fun i => ↥(A i)) i) x) = ↑x
This theorem states that for any type `ι`, any type `σ`, and any semiring `R`, given decidable equality on `ι`, `σ` that behaves like a subset of `R`, `σ` that is a submonoid of `R`, a function `A` from `ι` to `σ`, `ι` that is an additive monoid, and that `A` is a graded monoid with respect to `SetLike`, for any `i` in `ι` and any `x` in the subset `A i` of `σ`, applying the canonical ring homomorphism from the direct sum over `ι` of the subsets `A i` of `σ` to `R` to the image of `x` under the natural inclusion map from `A i` to the direct sum over `ι` of the subsets `A i` of `σ` gives the same result as considering `x` as an element of `R`. In other words, it proves that the canonical ring homomorphism preserves the inclusion of elements from `A i` into the direct sum.
More concisely: For any semiring R, decidable equality on types ι and σ, submonoid σ of R, additive monoid ι, graded monoid A:ι→σ with respect to SetLike, and function A:ι→σ, the canonical ring homomorphism from the direct sum of subsets A i of σ to R preserves the inclusion of elements from A i.
|