NonUnitalAlgebra.subset_adjoin
theorem NonUnitalAlgebra.subset_adjoin :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A}, s ⊆ ↑(NonUnitalAlgebra.adjoin R s)
The theorem `NonUnitalAlgebra.subset_adjoin` states that for any commutative semiring `R` and any non-unital non-associative semiring `A`, where `A` is a module over `R` and `R` and `A` form a scalar tower, and `R` and `A` are commutative under scalar multiplication, any set `s` of elements from `A` is a subset of the set obtained by adjoining `s` to the non-unital algebra over `R`. In other words, all elements of `s` are included in the non-unital algebra generated by `s` over `R`.
More concisely: For any commutative semiring `R`, commutative non-unital non-associative semiring `A` that is a module over `R` and forms a scalar tower with `R`, if `s` is a subset of `A`, then `s` is included in the non-unital algebra generated by `s` over `R`.
|
NonUnitalAlgebra.adjoin_induction
theorem NonUnitalAlgebra.adjoin_induction :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A} {p : A → Prop} {a : A},
a ∈ NonUnitalAlgebra.adjoin R s →
(∀ x ∈ s, p x) →
(∀ (x y : A), p x → p y → p (x + y)) →
p 0 → (∀ (x y : A), p x → p y → p (x * y)) → (∀ (r : R) (x : A), p x → p (r • x)) → p a
This theorem is about a property preservation in the context of non-unital algebras. Specifically, it states that if a certain property, denoted by the predicate `p`, holds for all elements `x` in a set `s` of type `A`, and this property `p` is preserved under the operations of algebraic mapping (which is implied by the `IsScalarTower` typeclass), addition, multiplication, and scalar multiplication (`r • x` where `r` is of type `R`), then this property `p` will also hold for any element `a` that belongs to the minimal non-unital subalgebra that includes the set `s`, denoted by `NonUnitalAlgebra.adjoin R s`. In other words, the theorem asserts that the operations of the non-unital algebra do not introduce elements that would violate the property `p`.
More concisely: If `p` is a property preserved under algebraic mapping, addition, multiplication, and scalar multiplication, and `p` holds for all elements in set `s`, then `p` also holds for all elements in the minimal non-unital algebra generated by `s`.
|
NonUnitalAlgHom.mem_range
theorem NonUnitalAlgHom.mem_range :
∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R]
[inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B]
[inst_4 : Module R B] [inst_5 : FunLike F A B] [inst_6 : NonUnitalAlgHomClass F R A B] (φ : F) {y : B},
y ∈ NonUnitalAlgHom.range φ ↔ ∃ x, φ x = y
The theorem `NonUnitalAlgHom.mem_range` states that for any types `F`, `R`, `A`, `B`, given a commutative semiring `R`, a non-unital, non-associative semiring `A` that is also a `R`-module, another non-unital, non-associative semiring `B` that is also a `R`-module, a function-like `F` from `A` to `B`, and a non-unital algebra homomorphism class `F` from `R`, `A`, `B`, for any `φ` of type `F` and any element `y` of `B`, `y` is in the range of the non-unital algebra homomorphism `φ` if and only if there exists an `x` such that applying `φ` to `x` gives `y`. In other words, `y` is in the image of `φ` iff `y` is the image of some element under `φ`.
More concisely: For any non-unital commutative semirings `R`, `A`, `B`, `R`-module homomorphisms `F` from `A` to `B`, and a non-unital algebra homomorphism `φ` of type `F` from `R`, `A`, `B`, `y` is in the image of `φ` if and only if there exists an `x` in `A` such that `φ(x) = y`.
|
NonUnitalAlgebra.coe_sInf
theorem NonUnitalAlgebra.coe_sInf :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (S : Set (NonUnitalSubalgebra R A)),
↑(sInf S) = ⋂ s ∈ S, ↑s
This theorem, named `NonUnitalAlgebra.coe_sInf`, states that for any set `S` of non-unital subalgebras in a non-unital, non-associative semiring `A` over a commutative semiring `R`, the coercion of the infimum (`sInf`, also known as the greatest lower bound) of `S` is equal to the intersection of all elements `s` in `S`. Here, the semiring `A` is a module over `R`, there is a scalar multiplication operation for `R`, `A`, and `A` that forms a tower (i.e., scalar multiplication is compatible with the ring multiplication), and the scalar multiplication is commutative.
More concisely: For any commutative semiring `R`, non-unital, non-associative semiring `A` over `R`, and set `S` of non-unital subalgebras of `A`, the coercion of the infimum of `S` equals the intersection of all elements in `S`.
|
NonUnitalSubalgebra.ext
theorem NonUnitalSubalgebra.ext :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
{S T : NonUnitalSubalgebra R A}, (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any given types `R` and `A`, where `R` is a commutative semiring, `A` is a non-unital and non-associative semiring, and `A` is also an `R`-module, if `S` and `T` are non-unital subalgebras of `A` over `R`, then `S` equals `T` if and only if every element `x` of `A` is in `S` if and only if it is in `T`. Essentially, it says that two non-unital subalgebras are the same if they have exactly the same elements.
More concisely: Two non-unital subalgebras `S` and `T` of a non-unital, non-associative `R`-module `A` over a commutative semiring `R` are equal if and only if they have the same elements.
|
NonUnitalAlgebra.gc
theorem NonUnitalAlgebra.gc :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
GaloisConnection (NonUnitalAlgebra.adjoin R) SetLike.coe
The theorem `NonUnitalAlgebra.gc` states that for any Commutative Semiring `R` and any Non-Unital Non-Associative Semiring `A` that is also a `R`-module, if `A` is a scalar tower and follows the scalar multiplication commutative law, then there exists a Galois connection between the function `adjoin` of Non-Unital Algebra over `R` and the coercion function of a `SetLike` structure.
In mathematical terms, a Galois connection is established between the algebra generated by a subset and the subset itself when viewing it as a set in the algebra. This connection provides a link between the algebraic structure and the underlying set structure.
More concisely: Given a Commutative Semiring `R`, a Non-Unital Non-Associative `R`-module Semiring `A` that is a scalar tower and satisfies the scalar multiplication commutative law, there exists a Galois connection between the `adjoin` function of `A` and the coercion function of `A` as a `SetLike` structure.
|
NonUnitalSubalgebra.smul_mem'
theorem NonUnitalSubalgebra.smul_mem' :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
(self : NonUnitalSubalgebra R A) (c : R) {x : A}, x ∈ self.carrier → c • x ∈ self.carrier
This theorem states that for any types `R` and `A`, with `R` being a commutative semiring, `A` being a non-unital non-associative semiring, and `A` is also a module over `R`, in any non-unital subalgebra of `R` over `A`, the carrier set is closed under scalar multiplication. In other words, if `x` is an element of the carrier set of the subalgebra, then the result of scalar multiplication of `x` with any scalar `c` from `R` is also an element of the carrier set.
More concisely: In any non-unital subalgebra of a commutative semiring `R` over a non-unital, non-associative semiring `A`, the scalar multiplication of any `x` in the subalgebra by any `c` in `R` remains within the subalgebra.
|
NonUnitalAlgebra.mem_top
theorem NonUnitalAlgebra.mem_top :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {x : A}, x ∈ ⊤
This theorem states that for any type `R` which is a commutative semiring and any type `A` which is a non-unital non-associative semiring, if `A` is a module over `R`, and if there is a scalar tower of `R` over `A`, and if the scalar multiplication `R * A -> A` commutes, then any element of `A` is an element of the top (or greatest) submodule `⊤` of `A`. This can be seen as an abstract algebra version of the observation that every element of a set is an element of its power set.
More concisely: In Lean 4, given a commutative semiring `R`, a non-unital non-associative semiring `A` with an `R`-module structure and a scalar tower, if scalar multiplication commutes, then every element of `A` is contained in the top submodule `⊤` of `A`.
|
NonUnitalAlgebra.adjoin_induction'
theorem NonUnitalAlgebra.adjoin_induction' :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A}
{p : ↥(NonUnitalAlgebra.adjoin R s) → Prop} (a : ↥(NonUnitalAlgebra.adjoin R s)),
(∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩) →
(∀ (x y : ↥(NonUnitalAlgebra.adjoin R s)), p x → p y → p (x + y)) →
p 0 →
(∀ (x y : ↥(NonUnitalAlgebra.adjoin R s)), p x → p y → p (x * y)) →
(∀ (r : R) (x : ↥(NonUnitalAlgebra.adjoin R s)), p x → p (r • x)) → p a
This theorem, `NonUnitalAlgebra.adjoin_induction'`, states that for any commutative semiring `R`, any non-unital, non-associative semiring `A`, and any set `s` of elements of `A`, there is an induction principle for elements `a` in the non-unital subalgebra generated by `s`. More specifically, if a property `p` holds for all elements of `s`, for the sum and product of any two elements in the subalgebra for which `p` holds, for the zero element, and for scalar multiples of any element in the subalgebra for which `p` holds, then `p` holds for every element `a` in the subalgebra. This theorem is different from `NonUnitalAlgebra.adjoin_induction` in that it applies to the subtype of `A` that lies in the non-unital subalgebra generated by `s`, rather than `A` itself.
More concisely: If `R` is a commutative semiring, `A` is a non-unital, non-associative semiring, and `s` is a set of elements in `A`, then any property `p` that holds for all elements in the non-unital subalgebra generated by `s` and for the zero element, is closed under sum, product, and scalar multiplication, so `p` holds for every element in that subalgebra.
|