CompleteLattice.independent_of_dfinsupp_lsum_injective
theorem CompleteLattice.independent_of_dfinsupp_lsum_injective :
∀ {ι : Type u_1} {R : Type u_2} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : Semiring R]
[inst_2 : AddCommMonoid N] [inst_3 : Module R N] (p : ι → Submodule R N),
Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype) → CompleteLattice.Independent p
This theorem, named `CompleteLattice.independent_of_dfinsupp_lsum_injective`, states that for any type `ι`, and any types `R` and `N` (with `R` being a semiring, `N` being an additive commutative monoid and also a module over `R`), and a function `p` mapping each element of type `ι` to a submodule of `N`, if the function induced by the direct sum of the submodules (obtained by applying each `p i` to the subtype of the submodule and then applying the linear sum of the direct-finite-support function) is injective, then the set of submodules `{p i : i in ι}` is independent in the complete lattice sense.
In simpler terms, if we have a collection of submodules such that no linear combination of elements from different submodules sums to zero unless all coefficients are zero, then these submodules are said to be independent.
More concisely: If the function induced by the direct sum and linear sum of submodules mapping each index to a submodule is injective, then the collection of submodules is independent in the complete lattice sense.
|
CompleteLattice.Independent.linearIndependent
theorem CompleteLattice.Independent.linearIndependent :
∀ {ι : Type u_1} {R : Type u_2} {N : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N]
[inst_3 : NoZeroSMulDivisors R N] (p : ι → Submodule R N),
CompleteLattice.Independent p →
∀ {v : ι → N}, (∀ (i : ι), v i ∈ p i) → (∀ (i : ι), v i ≠ 0) → LinearIndependent R v
This theorem states that given a family of submodules (indexed by a type `ι`), denoted by `p`, over a ring `R` and an additive commutative group `N` (which also forms a module over `R`), if this family of submodules is independent (i.e., every element of the direct sum of these submodules comes from at most one of the submodules), then, for any map `v` from `ι` to `N`, if every `v i` belongs to the corresponding submodule `p i` and is non-zero, the family of vectors `v` is linearly independent over `R`. In other words, in an independent family of submodules, a non-zero element chosen from each submodule will form a linearly independent set.
More concisely: If a family of submodules over a ring is independent, then a non-zero vector from each submodule forms a linearly independent set.
|
CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective
theorem CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective :
∀ {ι : Type u_1} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : AddCommGroup N] (p : ι → AddSubgroup N),
CompleteLattice.Independent p ↔ Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
The theorem `CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective` states that for all types `ι` and `N`, where `N` is an additive commutative group and the equality on `ι` is decidable, if `p` is a function mapping from `ι` to additive subgroups of `N`, then `p` satisfies lattice independence if and only if the function `DFinsupp.sumAddHom` applied with the subtype of each subgroup is injective. In simpler terms, a family of additive subgroups over an additive group are independent if and only if summing over them using `DFinsupp.sumAddHom` with descriptors of the subgroup elements as arguments yields distinct results for distinct inputs.
More concisely: For any type ι and additive commutative group N with decidable equality, a family of additive subgroups of N defined on ι is independent if and only if the function summing with descriptors using DFinsupp.sumAddHom yields distinct results for distinct inputs.
|
Submodule.mem_iSup_iff_exists_dfinsupp'
theorem Submodule.mem_iSup_iff_exists_dfinsupp' :
∀ {ι : Type u_1} {R : Type u_2} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
[inst_3 : DecidableEq ι] (p : ι → Submodule R N) [inst_4 : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)] (x : N),
x ∈ iSup p ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
This Lean theorem, `Submodule.mem_iSup_iff_exists_dfinsupp'`, provides a different formulation of membership in the indexed supremum of a family of submodules (indexed by `ι`), in the context of a semiring `R`, an additively commutative monoid `N`, and `N` being a module over `R`.
Specifically, it states that for any function `p` mapping elements of `ι` to submodules of `N`, a given element `x` from `N` is in the indexed supremum of `p` if and only if there exists a function `f` such that the sum (over `i`) of the function's values (denoted by `xi`), when lifted (`↑xi`) to `N`, equals `x`. Here, decidability of inequality of nonzero elements of each submodule in the family and decidability of equality in the index set are assumed.
In other words, `x` is in the supremum of the submodules if it can be represented as a sum of elements from these submodules.
More concisely: For a semiring R, an additively commutative monoid N being an R-module, and a function p from an index set ι to submodules of N, an element x of N lies in the indexed supremum of p if and only if there exists a function f: ι → N such that ∑i∈ι (↑fi) = x, where ↑denotes the lifting of elements from R to N and ∑denotes the sum in N.
|
CompleteLattice.Independent.dfinsupp_sumAddHom_injective
theorem CompleteLattice.Independent.dfinsupp_sumAddHom_injective :
∀ {ι : Type u_1} {N : Type u_5} [inst : DecidableEq ι] [inst_1 : AddCommGroup N] {p : ι → AddSubgroup N},
CompleteLattice.Independent p → Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
This theorem states that for any type `ι`, and a type `N` which is an additive commutative group, given a function `p` that maps from `ι` to additive subgroups of `N`, if these additive subgroups are complete lattice independent, then the canonical map out of the direct sum of this family of additive subgroups is injective. Here, the canonical map is formed by applying the direct sum function `DFinsupp.sumAddHom` to the subtype function of each subgroup.
In other words, if we have a family of additive subgroups that are independent in the complete lattice sense, then no two different combinations of elements from these subgroups will map to the same element in the resulting direct sum.
More concisely: If `{G_i : i ∈ ι}` is a family of additive subgroups of an additive commutative group `N` that are complete lattice independent, then the canonical map from the direct sum of `{G_i}` to `N` is injective.
|
DFinsupp.lhom_ext
theorem DFinsupp.lhom_ext :
∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
[inst_4 : Module R N] [inst_5 : DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄,
(∀ (i : ι) (x : M i), φ (DFinsupp.single i x) = ψ (DFinsupp.single i x)) → φ = ψ
The theorem `DFinsupp.lhom_ext` asserts that for any two `R`-linear maps `φ` and `ψ` from the direct sum of an index set `ι` and a family `M i` of `R`-modules to a `R`-module `N`, if these two maps coincide on each element of the form `DFinsupp.single i x` (which sends `i` to `x` and all other points to `0`), then these two maps are identical everywhere. This means that the behavior of these `R`-linear maps is completely determined by their action on these specific elements. The context requires `R` to be a semiring, `M i` and `N` to be `R`-modules, and `ι` to have decidable equality.
More concisely: If `R` is a semiring and `φ` and `ψ` are `R-linear` maps from the direct sum of an index set `ι` and a family `M i` of `R-modules to an `R-module N`, with decidable equality on `ι`, then `φ = ψ` if and only if `φ(DFinsupp.single i x) = ψ(DFinsupp.single i x)` for all `i ∈ ι` and `x ∈ M i`.
|
DFinsupp.lsum_single
theorem DFinsupp.lsum_single :
∀ {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
[inst_4 : Module R N] [inst_5 : DecidableEq ι] [inst_6 : Semiring S] [inst_7 : Module S N]
[inst_8 : SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i),
((DFinsupp.lsum S) F) (DFinsupp.single i x) = (F i) x
This theorem, named `DFinsupp.lsum_single`, states that for any types `ι`, `R`, `S`, `M`, `N`, under conditions that `R` is a semiring, each `M i` is an additive commutative monoid and a module over `R`, `N` is an additive commutative monoid and a module over `R` and `S`, `S` is a semiring, `ι` has decidable equality, and the scalar multiplication of `R` and `S` on `N` commutes, given a family of linear maps `F : (i : ι) → M i →ₗ[R] N`, an index `i : ι`, and an element `x : M i`, applying `lsum` to `F` and then applying this to the direct sum with only `x` at the `i`-th position (`DFinsupp.single i x`) is the same as just applying the `i`-th map to `x`, i.e., `F i x`. This theorem allows us to simplify expressions involving `lsum` and `single` without expanding `lsum` into `sumAddHom`.
More concisely: For any semirings R and S, additive commutative monoids and R-modules M, N, decidable type ι, and commuting scalar multiplications of R and S on N, the application of `lsum` to a family of linear maps F and the application of the map F at index i to an element x in M, are equal: `lsum F (DFinsupp.single i x) = F i x`.
|
DFinsupp.lhom_ext'
theorem DFinsupp.lhom_ext' :
∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [inst : Semiring R]
[inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
[inst_4 : Module R N] [inst_5 : DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄,
(∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i) → φ = ψ
This theorem asserts that, for any types ι, R, and M, and any type N, given a semiring structure on R, an addition-commutative monoid structure on each M i, a module structure over R on each M i, an addition-commutative monoid structure on N, and a module structure over R on N, and given that equality on ι is decidable, if you have two R-linear maps φ and ψ from the direct sum of the M i's to N, then if φ and ψ agree on the result of applying the direct sum's `single` function to each element of ι, then φ equals ψ everywhere. In other words, to check if two such R-linear maps are equal, it is enough to check their values on the `single` function's outputs. Especially, if M equals R, it suffices to verify that φ and ψ agree on `single a 1` for each a in ι.
More concisely: Given types ι, R, M, and N, if φ and ψ are R-linear maps from the direct sum of the M\_i's to N with decidable equality on ι, then φ = ψ if and only if they agree on the image of the `single` function for each i in ι.
|