Algebra.adjoin_le_iff
theorem Algebra.adjoin_le_iff :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
{S : Subalgebra R A}, Algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
The theorem `Algebra.adjoin_le_iff` states that for any commutative semiring `R`, semiring `A`, algebra structure on `R` and `A`, a set `s` of elements from `A`, and a subalgebra `S` of `R` and `A`, the minimal subalgebra that includes `s` is a subalgebra of `S` if and only if the set `s` is contained in the set of elements of `S`. In other words, the theorem provides a characterization of the containment relationship between the subalgebra generated by a set and another subalgebra in terms of set inclusion.
More concisely: The subalgebra generated by a set in a commutative semiring with respect to an algebra structure is contained in another subalgebra if and only if the set is included in the other subalgebra.
|
Algebra.span_le_adjoin
theorem Algebra.span_le_adjoin :
∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
Submodule.span R s ≤ Subalgebra.toSubmodule (Algebra.adjoin R s)
The theorem `Algebra.span_le_adjoin` states that for any commutative semiring `R` and any semiring `A` with a given algebra structure over `R`, for any set `s` of elements from `A`, the span of `s` as a submodule of `A` over `R` is a subset of (or equal to) the submodule associated with the smallest subalgebra that includes `s`. Here, the span of a set `s` is the smallest submodule of `A` that contains `s`, and the smallest subalgebra that includes `s` is obtained by adjoining `s` to the algebra of `R`. The theorem formalizes the intuition that the process of adjoining elements to an algebra 'enlarges' the algebra more (or at least not less) than merely forming the span of those elements as a submodule.
More concisely: For any commutative semiring `R`, semiring `A` with an algebra structure over `R`, and set `s` of elements from `A`, the span of `s` in `A` is contained in the submodule generated by `s` in the algebra of `R`.
|
Algebra.adjoin_eq_span
theorem Algebra.adjoin_eq_span :
∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R ↑(Submonoid.closure s)
This theorem states that for any commutative semiring `R` and any semiring `A` over `R`, for any set `s` of elements from `A`, the submodule corresponding to the subalgebra generated by adjoining `R` to `s` (obtained via the `Subalgebra.toSubmodule` map) is equal to the submodule spanned by the closure of `s` as a submonoid (obtained via `Submonoid.closure` followed by `Submodule.span`). In other words, the process of adjoined algebra generation followed by submodule mapping yields the same result as the process of submonoid closure followed by submodule span generation.
More concisely: For any commutative semiring `R`, set `s` of elements from a semiring `A` over `R`, the submodule of `A` generated by adjoining `R` to `s` is equal to the submodule spanned by the closure of `s` as a submonoid.
|
Algebra.subset_adjoin
theorem Algebra.subset_adjoin :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
s ⊆ ↑(Algebra.adjoin R s)
The theorem `Algebra.subset_adjoin` states that for any commutative semiring `R` and any semiring `A` with an algebra structure over `R`, and any set `s` of elements from `A`, the set `s` is a subset of the subalgebra `adjoin R s`. In other words, this theorem states that the subalgebra generated by adjoining the elements of `s` to `R` includes all elements of `s`.
More concisely: For any commutative semiring R and an algebra structure over R on semiring A, the set of elements from A that can be expressed as polynomials in s (a subset of A) over R is equal to the subalgebra of A generated by s.
|
Algebra.adjoin_empty
theorem Algebra.adjoin_empty :
∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
Algebra.adjoin R ∅ = ⊥
The theorem `Algebra.adjoin_empty` states that for any commutative semiring `R`, any semiring `A`, and any algebra structure on `A` over `R`, the minimal subalgebra of `A` that includes the empty set is the bottom element (or the trivial subalgebra). In other words, if we don't add any elements from `A` to the algebra structure, we get the smallest possible subalgebra, which consists only of the elements of `R` under the algebra map.
More concisely: The empty set is the smallest subalgebra of an algebra over a commutative semiring.
|
Submonoid.adjoin_eq_span_of_eq_span
theorem Submonoid.adjoin_eq_span_of_eq_span :
∀ (F : Type u_1) (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
[inst_3 : Algebra E K] [inst_4 : Semiring F] [inst_5 : Module F K] [inst_6 : IsScalarTower F E K]
(L : Submonoid K) {S : Set K},
↑L = ↑(Submodule.span F S) → Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
This theorem states that, given a ring extension tower `K / E / F` and a `F`-module `L` that is a submonoid of `K / F` generated by a set `S`, if `L` is equal to the span of `S` as an `F`-module, then the subalgebra generated by `E` and `L` (`E[L]`) is equal to the span of `S` as an `E`-module. In other words, the generation of a subalgebra by a submonoid is equivalent to the generation of a submodule by a set under the condition that the submonoid is the span of the set in the base of the extension tower.
More concisely: Given a ring extension tower `K / E / F`, if an `F`-module `L` in `K/F` generated by a set `S` equals its span as an `F`-module, then the subalgebra `E[L]` equals the span of `S` as an `E`-module.
|
Algebra.adjoin_induction'
theorem Algebra.adjoin_induction' :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
{p : ↥(Algebra.adjoin R s) → Prop},
(∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) →
(∀ (r : R), p ((algebraMap R ↥(Algebra.adjoin R s)) r)) →
(∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x + y)) →
(∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x * y)) → ∀ (x : ↥(Algebra.adjoin R s)), p x
The theorem `Algebra.adjoin_induction'` states that for all commutative semirings `R` and semirings `A`, with an algebra structure on `A` with `R` as the scalars, and a set `s` of elements from `A`, if a property `p` holds for all elements of `s` and for all elements of `R` under the algebra map to the adjoined algebra, and if this property is preserved under addition and multiplication in the adjoined algebra, then `p` holds for all elements of the adjoined algebra. Specifically, if `p` is true for each element in the set `s`, for each `r` in `R` under the algebra map, and for the sum and product of any two elements in the adjoined algebra for which `p` is true, then `p` is true for every element in the adjoined algebra.
More concisely: If a property holds for all elements in a set and their images under the algebra map in the adjoined algebra of a commutative semiring, and is closed under addition and multiplication in the adjoined algebra, then the property holds for all elements in the adjoined algebra.
|
Algebra.adjoin_induction₂
theorem Algebra.adjoin_induction₂ :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
{p : A → A → Prop} {a b : A},
a ∈ Algebra.adjoin R s →
b ∈ Algebra.adjoin R s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)) →
(∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x) →
(∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)) →
(∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y) →
(∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)) →
(∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y) →
(∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)) → p a b
This theorem is a principle of induction for the algebra generated by a set `s`. It states that if for any `x` and `y` in `s`, a property `p` holds for `x` and `y`, and this property also holds for elements mapped from the commutative semiring `R` to the semiring `A` by the algebra structure, and this property also respects addition and multiplication (in both the first and second arguments of `p`), then this property `p` holds for any `a` and `b` in the algebra adjoined from `R` and `s`. The addition and multiplication respect conditions are specifically, if `p` holds for `x₁` and `y`, `x₂` and `y`, then `p` holds for `x₁ + x₂` and `y`, and `x₁ * x₂` and `y`, and similarly for the second arguments of `p`.
More concisely: If `p(x, y)` holds for all `x, y` in a set `s` and elements of the commutative semiring `R`, and respects algebraic operations in both arguments, then `p` holds for all elements in the algebra generated by `R` and `s`.
|
Algebra.adjoin_image
theorem Algebra.adjoin_image :
∀ (R : Type uR) {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (s : Set A),
Algebra.adjoin R (⇑f '' s) = Subalgebra.map f (Algebra.adjoin R s)
The theorem `Algebra.adjoin_image` states that for any commutative semiring `R`, semirings `A` and `B`, and an algebra homomorphism `f` from `A` to `B`, if we have a set `s` of elements in `A`, then the subalgebra generated by the image of `s` under the homomorphism `f` (i.e., `Algebra.adjoin R (⇑f '' s)`) is equal to the subalgebra obtained by mapping the subalgebra generated by `s` (i.e., `Algebra.adjoin R s`) under the homomorphism `f` (i.e., `Subalgebra.map f (Algebra.adjoin R s)`). This theorem captures the idea that the process of adjoining elements to an algebra and then mapping to another algebra can be interchanged with the process of first mapping the elements to the other algebra, and then adjoining there.
More concisely: For any commutative semirings R, semirings A and B, and algebra homomorphism f from A to B, the subalgebras generated by the image of a set s under f and the set s itself, both in A and then mapped to B, are equal.
|
Algebra.self_mem_adjoin_singleton
theorem Algebra.self_mem_adjoin_singleton :
∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
x ∈ Algebra.adjoin R {x}
The theorem `Algebra.self_mem_adjoin_singleton` states that for any commutative semiring `R`, any semiring `A`, any algebra structure between `R` and `A`, and any element `x` from `A`, `x` is an element of the subalgebra of `A` adjoined by `R` that includes only `x`. In other words, if we create a subalgebra by adjoining the set containing only `x` to `R`, `x` itself is guaranteed to be in that subalgebra.
More concisely: For any commutative semiring `R`, algebra `A` over `R` with an algebra structure map `r : R → A`, and element `x ∈ A`, `x` is contained in the subalgebra of `A` generated over `R` by `{x}`.
|
Algebra.adjoin_int
theorem Algebra.adjoin_int :
∀ {R : Type u_1} [inst : Ring R] (s : Set R), Algebra.adjoin ℤ s = subalgebraOfSubring (Subring.closure s) := by
sorry
This theorem states that for any ring `R` and a set `s` of elements from `R`, the minimal subalgebra that includes `s` when the ring of scalars is the integers (`ℤ`) is equivalent to a `ℤ`-subalgebra generated by the subring closure of `s`. In essence, this theorem is expressing a relationship between the operations of adjoining to an algebra and the closure of a subring within the context of integer scalars.
More concisely: The minimal subalgebra of a ring generated by a set of elements is equal to the subring generated by the closure of that set under addition and multiplication, when the ring of scalars is the integers.
|
Algebra.adjoin_induction
theorem Algebra.adjoin_induction :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
{p : A → Prop} {x : A},
x ∈ Algebra.adjoin R s →
(∀ x ∈ s, p x) →
(∀ (r : R), p ((algebraMap R A) r)) →
(∀ (x y : A), p x → p y → p (x + y)) → (∀ (x y : A), p x → p y → p (x * y)) → p x
The theorem `Algebra.adjoin_induction` states the following:
For all types `R` and `A`, where `R` is a commutative semiring, `A` is a semiring, and there exists an algebra structure between `R` and `A`, and given a set `s` of `A`, a predicate `p` on `A`, and an element `x` of `A`, if `x` belongs to the minimal subalgebra that includes `s` (`Algebra.adjoin R s`), and if the predicate `p` holds for all elements of `s`, and for all elements of `R` mapped into `A`, and is preserved under addition and multiplication in `A`, then `p` holds for `x`.
In simpler words, this theorem is a principle of mathematical induction for elements in the subalgebra generated by a particular set in the context of semirings and algebras.
More concisely: If `s` is a set in a semiring `A` over a commutative semiring `R` with an algebra structure, and `x` is an element of the minimal subalgebra generated by `s` such that `p(y)` holds for all `y` in `s` and maps of `R` into `A`, then `p(x)` holds.
|
Algebra.restrictScalars_adjoin_of_algEquiv
theorem Algebra.restrictScalars_adjoin_of_algEquiv :
∀ {F : Type u_4} {E : Type u_5} {L : Type u_6} {L' : Type u_7} [inst : CommSemiring F] [inst_1 : CommSemiring L]
[inst_2 : CommSemiring L'] [inst_3 : Semiring E] [inst_4 : Algebra F L] [inst_5 : Algebra L E]
[inst_6 : Algebra F L'] [inst_7 : Algebra L' E] [inst_8 : Algebra F E] [inst_9 : IsScalarTower F L E]
[inst_10 : IsScalarTower F L' E] (i : L ≃ₐ[F] L'),
⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i →
∀ (S : Set E),
Subalgebra.restrictScalars F (Algebra.adjoin L S) = Subalgebra.restrictScalars F (Algebra.adjoin L' S)
This theorem states that given two ring extension towers `E / L / F` and `E / L' / F`, if there is an algebra isomorphism `L ≃ₐ[F] L'` that is compatible with the extensions `E / L` and `E / L'`, then for any subset `S` of `E`, the minimal subalgebras that include `S` in `L` and `L'` are equal as subalgebras of `E / F`. This is under the condition that the algebra map from `L` to `E` is the same as the composition of the algebra map from `L'` to `E` and the isomorphism `i`, when viewing `i` as a function.
More concisely: Given ring extension towers `E / L / F` and `E / L' / F` with a compatible isomorphism `L ≃ₐ[F] L'` between their middle layers, any subset `S` of `E` has equal minimal subalgebras containing it in `L` and `L'` as subalgebras of `E/F`.
|
AlgHom.map_adjoin
theorem AlgHom.map_adjoin :
∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (s : Set A),
Subalgebra.map φ (Algebra.adjoin R s) = Algebra.adjoin R (⇑φ '' s)
The theorem `AlgHom.map_adjoin` states that for any commutative semiring `R` and semirings `A` and `B` equipped with algebra structures over `R`, and for any algebra homomorphism `φ` from `A` to `B` and any set `s` of elements from `A`, the image of the subalgebra generated by `s` under the map `φ` is equal to the subalgebra generated by the image of `s` under `φ`. In other words, applying an algebra homomorphism to the subalgebra generated by a set is the same as generating a subalgebra from the image of the set under the homomorphism.
More concisely: For any commutative semirings `R`, semialgebras `A` and `B` over `R`, algebra homomorphism `φ: A → B`, and set `s ∈ A`, the subalgebra of `B` generated by `φ(s)` is equal to the image of the subalgebra of `A` generated by `s` under `φ`.
|
Algebra.adjoin_mono
theorem Algebra.adjoin_mono :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s t : Set A},
s ⊆ t → Algebra.adjoin R s ≤ Algebra.adjoin R t
This theorem, `Algebra.adjoin_mono`, states that for any commutative semiring `R`, semiring `A`, and algebra structure from `R` to `A`, and for any sets `s` and `t` of elements from `A`, if `s` is a subset of `t`, then the smallest subalgebra of `A` that includes `s` is a subalgebra of the smallest subalgebra of `A` that includes `t`. In other words, if `s` is contained within `t`, then the subalgebra generated by `s` is also contained within the subalgebra generated by `t`.
More concisely: For any commutative semirings R and A, and an algebra structure from R to A, if s is a subset of t in A, then the subalgebra generated by s is contained in the subalgebra generated by t.
|
Subalgebra.adjoin_eq_span_basis
theorem Subalgebra.adjoin_eq_span_basis :
∀ {F : Type u_1} (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
[inst_3 : Algebra E K] [inst_4 : CommSemiring F] [inst_5 : Algebra F K] [inst_6 : IsScalarTower F E K]
(L : Subalgebra F K) {ι : Type u_4} (bL : Basis ι F ↥L),
Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E (Set.range fun i => ↑(bL i))
This theorem states that given a ring extension tower `K / E / F`, and a subalgebra `L` of `K / F`, the minimal subalgebra `E[L]` that includes `L` is generated by any basis of `L / F` as an `E`-module. This means that the forgetful map from the subalgebra to submodule of `E[L]` is equal to the submodule spanned by the set of all basis elements of `L / F` in `E`. In other words, it is sufficient to take the set of basis elements to generate the subalgebra `E[L]` as an `E`-module.
More concisely: Given a ring extension tower `K / E / F` and a subalgebra `L` of `K/F`, the minimal `E`-submodule of `E[L]` containing `L` is generated by any basis of `L/F` as an `E`-module.
|
Subalgebra.adjoin_eq_span_of_eq_span
theorem Subalgebra.adjoin_eq_span_of_eq_span :
∀ {F : Type u_1} (E : Type u_2) {K : Type u_3} [inst : CommSemiring E] [inst_1 : Semiring K] [inst_2 : SMul F E]
[inst_3 : Algebra E K] [inst_4 : CommSemiring F] [inst_5 : Algebra F K] [inst_6 : IsScalarTower F E K]
(L : Subalgebra F K) {S : Set K},
Subalgebra.toSubmodule L = Submodule.span F S →
Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
This theorem states that in a tower of ring extensions `K / E / F`, if `L` is a subalgebra of `K / F` which is generated by a set `S` as an `F`-module, then the subalgebra generated by `E` and `L`, denoted by `E[L]`, is also generated by `S` as an `E`-module. In other words, if `L` is the smallest `F`-submodule containing `S`, then `E[L]` is the smallest `E`-submodule containing `S`. This highlights a preservation property in the context of ring extensions and the generation of subalgebras and submodules.
More concisely: In a tower of ring extensions K / E / F, if L is an F-submodule of K generated by a set S, then the subalgebra E[L] is also generated by S as an E-module.
|
Algebra.adjoin_le
theorem Algebra.adjoin_le :
∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
{S : Subalgebra R A}, s ⊆ ↑S → Algebra.adjoin R s ≤ S
This theorem states that for any commutative semiring `R`, semiring `A`, and an algebra `R A`, given a set `s` of elements from `A` and a subalgebra `S` of `R A`, if `s` is a subset of `S` (denoted as `s ⊆ ↑S`), then the minimal subalgebra that includes `s` (created using the `Algebra.adjoin` function) is a subalgebra of `S` (denoted as `Algebra.adjoin R s ≤ S`). In other words, the smallest algebra that contains a particular set of elements is always a subset of any other algebra that contains the same set of elements.
More concisely: For any commutative semirings R and A, and an algebra R A, if s is a subset of a subalgebra S of R A, then the subalgebra generated by s (using Algebra.adjoin) is included in S.
|