IsScalarTower.algebraMap_eq
theorem IsScalarTower.algebraMap_eq :
∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
algebraMap R A = (algebraMap S A).comp (algebraMap R S)
The theorem `IsScalarTower.algebraMap_eq` states that, for any three types `R`, `S`, and `A` where `R` and `S` are commutative semirings, `A` is a semiring, `R` and `S` are algebras over `A`, and `R`,`S` and `A` form a scalar tower, the algebra map from `R` to `A` is equal to the composition of the algebra map from `S` to `A` and the algebra map from `R` to `S`. In other words, if we have a scalar tower, then mapping a scalar from the base of the tower to the top of the tower directly or going through an intermediate level yields the same result.
More concisely: For any commutative semirings R, S, and semiring A with R, S algebra extensions, if R, S, and A form a scalar tower, then the algebra map from R to A equals the composition of the algebra maps from S to A and R to S.
|
IsScalarTower.algebraMap_smul
theorem IsScalarTower.algebraMap_smul :
∀ {R : Type u} (A : Type w) {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : MulAction A M] [inst_4 : SMul R M] [inst_5 : IsScalarTower R A M] (r : R) (x : M),
(algebraMap R A) r • x = r • x
The theorem `IsScalarTower.algebraMap_smul` states that for any commutative semiring `R`, semiring `A`, and type `M`, given that `A` is an algebra over `R`, `M` is a module over `A`, `R` acts by scalar multiplication on `M`, and `R`, `A`, and `M` form a scalar tower, then scalar multiplication by an element `r` of `R` on an element `x` of `M`, when `r` is first mapped to `A` via the algebra structure, is the same as direct scalar multiplication by `r` on `x`. In mathematical terms, this can be written as $(\phi(r)) \cdot x = r \cdot x$ where $\phi : R \to A$ is the algebra structure map.
More concisely: For any commutative semiring R, algebra A over R, A-module M, scalar action of R on M, and scalar tower (R, A, M), the algebra map of R to A commutes with scalar multiplication on M: $\phi(r) \cdot x = r \cdot x$.
|
IsScalarTower.of_algebraMap_eq
theorem IsScalarTower.of_algebraMap_eq :
∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A],
(∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)) → IsScalarTower R S A
This theorem is named `IsScalarTower.of_algebraMap_eq`. It states that for any types `R`, `S`, and `A`, where `R`, `S`, and `A` have the structure of commutative semirings, `R` and `S` have an algebra structure over `A`, and `R` has an algebra structure over `S`, then if for every element `x` in `R`, the map from `R` to `A` applied to `x` equals the map from `S` to `A` applied to the map from `R` to `S` applied to `x`, then `R`, `S`, and `A` form a scalar tower. A scalar tower is a mathematical structure in which the multiplication in `R`, `S`, and `A` is compatible in a certain way.
More concisely: If for all `x` in `R`, the map from `R` to `A` applied to `x` equals the map from `S` to `A` applied to the algebra map from `R` to `S` applied to `x`, then `R`, `S`, and `A` form a scalar tower over `A`.
|
IsScalarTower.algebraMap_apply
theorem IsScalarTower.algebraMap_apply :
∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A] (x : R),
(algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)
This theorem, `IsScalarTower.algebraMap_apply`, asserts that for any types `R`, `S`, and `A` which form a scalar tower and have the type `R` as a commutative semiring, type `S` as a commutative semiring, and type `A` as a semiring with `R`, `S`, and `A` being algebraic structures, the mapping of any element `x` from `R` to `A` using the algebra map is equivalent to the composition of the mapping of `x` from `R` to `S` and then to `A`. In other words, if we have a scalar tower, the map from the bottom of the tower to the top is the same as going up one level and then to the top: $(R \rightarrow A) = (S \rightarrow A) \circ (R \rightarrow S)$.
More concisely: For any commutative semirings R, S, and semiring A forming a scalar tower, the algebra map from R to A is equal to the composition of the maps from R to S and then from S to A.
|
Submodule.span_smul_of_span_eq_top
theorem Submodule.span_smul_of_span_eq_top :
∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
[inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {s : Set S},
Submodule.span R s = ⊤ →
∀ (t : Set A), Submodule.span R (s • t) = Submodule.restrictScalars R (Submodule.span S t)
The theorem `Submodule.span_smul_of_span_eq_top` states that for any types `R`, `S`, `A` with `R` and `S` being semirings, `A` an additive commutative monoid, `S` a module over `R`, `A` a module over both `R` and `S`, and `A` a scalar tower over `R` and `S`, if the span of a set `s` of type `S` over `R` equals the top submodule, then for any set `t` of type `A`, the span of the scaled set `s • t` over `R` equals the restriction of the scalars of the span of `t` over `S` to `R`. Here, `s • t` denotes the set of all elements obtained by scaling elements of `t` by elements of `s`. The `Submodule.span R s = ⊤` condition means that every element of the module `S` can be expressed as a linear combination of elements from the set `s` with coefficients in `R`.
More concisely: If the span of a set in an `R`-module `S` over `R` equals the whole module, then the span of the scalar multiples of another set in `S` over `R` is equal to the restriction of scalars of the span of that set over `S` to `R`.
|
Submodule.restrictScalars_span
theorem Submodule.restrictScalars_span :
∀ (R : Type u) (A : Type w) {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M],
Function.Surjective ⇑(algebraMap R A) →
∀ (X : Set M), Submodule.restrictScalars R (Submodule.span A X) = Submodule.span R X
The theorem `Submodule.restrictScalars_span` states that for any commutative semiring `R`, any semiring `A`, and any type `M` forming a module over `R` and `A`, and assuming `R` is a scalar tower over `A` and `M`, if the morphism induced by the `R`-algebra structure on `A` is surjective (meaning every element in `A` is mapped from an element in `R`), then the `R`-module generated by any set `X` is the same as the `A`-module generated by the same set `X`. In mathematical terms, if every element of `A` can be expressed as a result of some `R`-algebra operation, then the span of a set `X` under `R` and `A` are the same.
More concisely: If `R` is a commutative semiring that is a scalar tower over semiring `A`, `M` is a module over both `R` and `A`, and the `R`-algebra structure morphism from `A` to the `R`-algebra of `M` is surjective, then the `R`-module generated by a set `X` equals the `A`-module generated by `X`.
|
AlgHom.comp_algebraMap_of_tower
theorem AlgHom.comp_algebraMap_of_tower :
∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
[inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
[inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
(f : A →ₐ[S] B), (↑f).comp (algebraMap R A) = algebraMap R B
This theorem states that for any commutative semi-rings R and S and semi-rings A and B, if we have algebra structures between R and S, S and A, S and B, R and A, R and B, and if A and B form a scalar tower over R and S, then the composition of any algebra homomorphism from A to B over S with the embedding from R to A defined by the algebra structure is equal to the embedding from R to B defined by its algebra structure. Essentially, this theorem is a statement about the compatibility of the algebra structure and the concept of a scalar tower in the context of ring homomorphisms, specifically how the algebra map behaves with respect to the composition of algebra homomorphisms.
More concisely: Given commutative semi-rings R, S, and algebra structures between R and S, S and A, S and B, R and A, and R and B, if A and B form a scalar tower over R and S, then the composition of the algebra homomorphism from A to B over S with the embedding from R to A is equal to the embedding from R to B.
|
IsScalarTower.of_algebraMap_eq'
theorem IsScalarTower.of_algebraMap_eq' :
∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
[inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A],
algebraMap R A = (algebraMap S A).comp (algebraMap R S) → IsScalarTower R S A
This theorem, named `IsScalarTower.of_algebraMap_eq'`, states that for any three given types `R`, `S`, and `A` with the associated structures of commutative semirings for `R` and `S`, semiring for `A`, and algebra structures between `R` and `S`, `S` and `A`, and `R` and `A`, if the algebra map from `R` to `A` is equivalent to the composition of the algebra map from `S` to `A` and the algebra map from `R` to `S`, then `R`, `S`, and `A` form a scalar tower. In mathematical terms, if $\phi: R\rightarrow A$ is the same as the composition of $\psi: S\rightarrow A$ and $\chi: R\rightarrow S$ (i.e., $\phi = \psi \circ \chi$), then `R`, `S`, and `A` obey the compatibility condition of scalar multiplication in a scalar tower.
More concisely: If the algebra maps from `R` to `A` and from `S` to `A` via `χ` and `ψ`, respectively, satisfy `ψ ∘ χ = α` for some algebra map `α` from `R` to `S`, then `R`, `S`, and `A` form a scalar tower.
|
Submodule.span_algebraMap_image
theorem Submodule.span_algebraMap_image :
∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (a : Set R),
Submodule.span R (⇑(algebraMap R S) '' a) = Submodule.map (Algebra.linearMap R S) (Submodule.span R a)
This theorem, `Submodule.span_algebraMap_image`, states that for any commutative semiring `R`, semiring `S`, and algebra `S` over `R`, given a set `a` of elements from `R`, the span of the image of `a` under the canonical ring homomorphism (often referred to as `algebraMap` in Lean 4) from `R` to `S` is equal to the image of the span of `a` under the canonical linear map from `R` to `S`. In mathematical terms, if you take a set of elements from `R`, map them into `S` using the algebra structure, and then find the smallest submodule of `S` containing these mapped elements (i.e., you "span" the image of `a`), you get the same result as if you first span the original set in `R` and then map the resulting submodule into `S` using the linear map associated with the algebra structure.
More concisely: For any commutative semirings R and S, semiring homomorphism f : R -> S from R to S, and finite set a in R, the image of the submodule spanned by a under f is equal to the submodule spanned by the images of a under f in S.
|