RingFilterBasis.SubmodulesBasis.smul
theorem RingFilterBasis.SubmodulesBasis.smul :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{BR : RingFilterBasis R} {B : ι → Submodule R M},
BR.SubmodulesBasis B → ∀ (m : M) (i : ι), ∃ U ∈ BR, U ⊆ (fun x => x • m) ⁻¹' ↑(B i)
This theorem states that for any element `m` from type `M` and any set `B i` in the submodule basis on `M`, there exists a `U` in the ring filter basis on `R` such that `U * m` is contained in `B i`. Here, `R` is a commutative ring, `M` is an additive commutative group which is also a module over `R`, `BR` is a ring filter basis on `R`, and `B` is a function from index type `ι` to submodules of `R` and `M`. If `BR` forms a submodule basis for `B`, then for each `m` in `M` and `i` in `ι`, there exists a `U` in the ring filter basis `BR` such that all the scalar multiples (`x • m` for `x` in `U`) are elements of the submodule `B i`.
More concisely: For any `m` in an `R`-module `M` and submodule `B i` of `M`, there exists a ring filter `U` in `R` such that `U * m` is contained in `B i`. If `U` forms a submodule basis for `B`, then all scalar multiples of `m` by elements in `U` belong to `B i`.
|
SubmodulesRingBasis.mul
theorem SubmodulesRingBasis.mul :
∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
{B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
This theorem states that for every element in a basis of submodules on a given algebra over a commutative ring, there is another basis element such that the set-theoretic (Cartesian) product of this basis element with itself is contained within the initial basis element. This is valid for any commutative ring and any algebra over this ring.
More concisely: For every basis element in a submodule of a commutative ring algebra, there exists another basis element such that their product is contained in the first element.
|
SubmodulesRingBasis.toRing_subgroups_basis
theorem SubmodulesRingBasis.toRing_subgroups_basis :
∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
{B : ι → Submodule R A}, SubmodulesRingBasis B → RingSubgroupsBasis fun i => (B i).toAddSubgroup
This theorem states that for any index type `ι`, and any types `R` and `A` which have the structure of commutative rings, given an `R`-algebra structure on `A`, and a family `B` of submodules of `A` (indexed by `ι`) which forms a ring basis of submodules, the corresponding family of additive subgroups obtained by reinterpreting each submodule in the family `B` as an additive subgroup, forms a ring basis of additive subgroups. Essentially, the ring basis property is preserved when we switch from the context of submodules to additive subgroups.
More concisely: Given an index type `ι`, types `R` and `A` with commutative ring structures, an `R`-algebra structure on `A`, and a family `B` of `R`-submodules of `A` (indexed by `ι`) that forms a ring basis, the corresponding family of additive subgroups of `A` obtained from `B` is also a ring basis of additive subgroups.
|
RingSubgroupsBasis.leftMul
theorem RingSubgroupsBasis.leftMul :
∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
RingSubgroupsBasis B → ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(B i)
The theorem `RingSubgroupsBasis.leftMul` states that for any element `x` of a certain type `A` and any set `B` in the submodule basis on `A`, there exists another basis element `B'` such that the product of `B'` and `x` is in `B`. More concretely, given a ring `A`, a function `B` mapping indices of type `ι` to additive subgroups of `A`, and assuming that `B` forms a basis for the ring subgroups of `A`, for any element `x` of `A` and any index `i` of `ι`, there exists another index `j` such that every element of the subgroup `B j` when multiplied by `x` from the left falls within the subgroup `B i`.
More concisely: For any element `x` in a ring `A` and any subgroup basis `B` of `A`, there exists a basis element `B'` such that for all indices `i` and `j`, the product `x * B j` lies in `B i`.
|
RingSubgroupsBasis.rightMul
theorem RingSubgroupsBasis.rightMul :
∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
RingSubgroupsBasis B → ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
The theorem `RingSubgroupsBasis.rightMul` states that for any ring `A` and any set `B` that forms a basis of subgroups on `A`, for any element `x` of `A` and any basis element `B i`, there exists another basis element `B j` such that the multiplication of `x` and any element of `B j` is contained in `B i`. In other words, each element in the subgroup `B j` when right-multiplied by `x` results in an element that is in the subgroup `B i`.
More concisely: For any ring `A` and basis `B` of subgroups of `A`, for all `x in A` and basis elements `Bi, Bj in B`, there exists `Bj` such that `x * Bj` is contained in `Bi`.
|
RingSubgroupsBasis.mul
theorem RingSubgroupsBasis.mul :
∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
RingSubgroupsBasis B → ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
This theorem states that for any given set `B` from the submodule basis of a ring `A`, there exists another basis element `B'` such that the set-theoretic product of `B'` with itself is a subset of `B`. In other words, when you multiply every element in `B'` by every other element in `B'`, all the resulting elements belong to `B`. Here, `A` is a ring, `B` is a function mapping from type `ι` to AddSubgroup of `A`, and `RingSubgroupsBasis B` means that `B` is a Ring Subgroups Basis.
More concisely: For any ring `A` and any set `B` in `RingSubgroupsBasis A`, there exists a basis element `B'` such that `B'.map (λ x, ∀ y ∈ B, x * y ∈ B)`.
|
RingFilterBasis.SubmodulesBasis.inter
theorem RingFilterBasis.SubmodulesBasis.inter :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{BR : RingFilterBasis R} {B : ι → Submodule R M}, BR.SubmodulesBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
This theorem states the condition for `B` to serve as a filter basis on a module `M` over a commutative ring `R`. More precisely, for any commutative ring `R` and a module `M` over `R`, if `B` is a family of submodules of `M` indexed by `ι` and `BR` is a ring filter basis of `R`, such that `BR.SubmodulesBasis B` holds, then for any two indices `i` and `j` from `ι`, there exists an index `k` such that the `k`-th submodule of `B` is a subset of the intersection of the `i`-th and `j`-th submodules of `B`.
More concisely: Given a commutative ring R and a module M over R, if B is a family of submodules of M indexed by ι, and BR is a filter basis of R such that B is a subbasis of the lattice of submodules of M with respect to BR, then B is a filter basis of submodules of M.
|
SubmodulesRingBasis.inter
theorem SubmodulesRingBasis.inter :
∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
{B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
This theorem states a condition for `B` to be a filter basis on `A`. Specifically, for any types `ι`, `R`, and `A`, if `R` and `A` are both commutative rings and `A` is an `R`-algebra, and `B` is a function from `ι` to the submodules of `R` over `A`, then if `B` forms a ring basis of submodules, for any two elements `i` and `j` in `ι`, there exists a third element `k` in `ι` such that the submodule `B` at `k` is a subset of the intersection of the submodules `B` at `i` and `j`.
More concisely: If `B: ι → submodules R over A` is a ring basis in the category of submodules of a commutative `R`-algebra `A`, then for all `i, j ∈ ι`, there exists `k ∈ ι` such that `B i ∩ B j ⊆ B k`.
|
SubmodulesBasis.smul
theorem SubmodulesBasis.smul :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace R] {B : ι → Submodule R M},
SubmodulesBasis B → ∀ (m : M) (i : ι), ∀ᶠ (a : R) in nhds 0, a • m ∈ B i
This theorem states that for any module `M` over a commutative ring `R` with a topological space structure, given a basis `B` of submodules of `M`, for any element `m` from `M` and any set `B` in the basis, the scalar multiplication of `m` by any scalar `a` that is sufficiently close to zero belongs to `B`. Here, "sufficiently close" is defined with respect to the neighborhood filter `nhds` at `0` in the ring `R`. In other words, if we take a neighborhood of zero in `R` and multiply `m` by any element in that neighborhood, we stay within the submodule `B`.
More concisely: For any module `M` over a commutative ring `R` with a topological space structure, and for any basis `B` of submodules of `M` and any `m` in `M`, if `a` is a scalar in `R` sufficiently close to zero with respect to the neighborhood filter at `0`, then `am` belongs to `B`.
|
RingSubgroupsBasis.inter
theorem RingSubgroupsBasis.inter :
∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] {B : ι → AddSubgroup A},
RingSubgroupsBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
This theorem states that given a type `A` with a ring structure and a function `B` from a type `ι` to additive subgroups of `A`, if `B` is a ring subgroups basis, then for any two elements `i` and `j` of type `ι`, there exists another element `k` of type `ι` such that the additive subgroup `B k` is a subset of the intersection of the additive subgroups `B i` and `B j`. This is a condition for `B` to be a filter basis on `A`.
More concisely: Given a ring `A` and a family `B` of additive subgroups indexed by type `ι`, if `B` is a ring subgroup basis such that for all `i, j ∈ ι`, there exists `k ∈ ι` with `B k ⊆ B i ∩ Bi`, then `B` is a filter basis on `A`.
|
SubmodulesBasis.inter
theorem SubmodulesBasis.inter :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace R] {B : ι → Submodule R M}, SubmodulesBasis B → ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
This theorem states that for any two indices `i` and `j`, if `B` is a filter basis on a module `M` over a commutative ring `R` with an associated topology, there exists an index `k` such that the `k`-th submodule of `B` is a subset of the intersection of the `i`-th and `j`-th submodules of `B`. This is a condition for `B` to be a filter basis on `M`.
More concisely: For any filter basis `B` on a module `M` over a commutative ring `R`, there exists an index `k` such that the `k`-th submodule of `B` is contained in the intersection of the `i`-th and `j`-th submodules of `B`, for all indices `i` and `j`.
|
SubmodulesRingBasis.leftMul
theorem SubmodulesRingBasis.leftMul :
∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
{B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (a : A) (i : ι), ∃ j, a • B j ≤ B i
This is a theorem about the basis of a submodule in the context of algebra over commutative rings. It states that for any element `a` of type `A`, and for any set `B` within the basis of the submodule on `A`, there exists another basis element `B'` such that the product of `a` and `B'` (`a • B'`) is contained in `B`. This is true for all types `ι`, `R`, and `A`; where `R` and `A` are commutative rings and `A` is an `R`-algebra. The set `B` is a function from `ι` to the submodules of `R` in `A`. The theorem asserts that no matter which element and basis element you choose, you can always find another basis element that satisfies this condition.
More concisely: For any commutative ring `R`, `R`-algebra `A`, element `a` in `A`, and basis `B` of a submodule of `A` (as a function from some index type `ι` to submodules of `A`), there exists a basis element `B'` such that `a` times `B'` is in `B`.
|
RingSubgroupsBasis.hasBasis_nhds_zero
theorem RingSubgroupsBasis.hasBasis_nhds_zero :
∀ {A : Type u_1} {ι : Type u_2} [inst : Ring A] [inst_1 : Nonempty ι] {B : ι → AddSubgroup A}
(hB : RingSubgroupsBasis B), (nhds 0).HasBasis (fun x => True) fun i => ↑(B i)
The theorem `RingSubgroupsBasis.hasBasis_nhds_zero` states that for any type `A` with a ring structure and any index type `ι`, given a family `B` of additive subgroups of `A` indexed by `ι` and assuming `B` forms a ring subgroups basis, the neighborhood filter at zero in `A` has a basis consisting of the carrier sets of the members of `B`. Here, a basis of a filter in topology is a collection of sets such that every set in the filter can be written as a union of sets from this collection.
More concisely: For any ring `A` and indexed family `B` of additive subgroups of `A` forming a ring subgroup basis, the neighborhood filter at zero in `A` has a basis consisting of the carrier sets of members of `B`.
|