StarSubalgebra.ext
theorem StarSubalgebra.ext :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S T : StarSubalgebra 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 semiring, both `R` and `A` have a star-ring structure, and `A` is an algebra over `R` with star-module structure, then for any two star subalgebras `S` and `T` of `R` in `A`, if for any element `x` in `A`, `x` is in `S` if and only if `x` is in `T`, then `S` and `T` are equal. That is, two star subalgebras are equal if they have the same elements.
More concisely: Given commutative semirings `R` and `A`, if `A` is an `R`-algebra with star-module structure and `S` and `T` are star subalgebras of `R` in `A` such that for all `x` in `A`, `x` is in `S` if and only if `x` is in `T`, then `S` equals `T`.
|
Subalgebra.mem_star_iff
theorem Subalgebra.mem_star_iff :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A) (x : A),
x ∈ star S ↔ star x ∈ S
This theorem states that for any commutative semiring `R`, star ring `R`, semiring `A`, algebra of `R` and `A`, star ring `A`, and a star module `R` and `A`, and given a subalgebra `S` of `R` and `A` and an element `x` in `A`, `x` is in the star of `S` if and only if the star of `x` is in `S`. Here, "star" refers to an operation in ring theory related to the conjugate of an element.
More concisely: For any commutative semirings R and star rings R\*, A, semirings A, and star modules R and A, if S is a subalgebra of R and A, then an element x in A is in the star of S if and only if the star of x is in S.
|
StarSubalgebra.coe_sInf
theorem StarSubalgebra.coe_sInf :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Set (StarSubalgebra R A)),
↑(sInf S) = ⋂ s ∈ S, ↑s
This theorem states that for any type `R` and `A`, where `R` is a commutative semiring and also a star ring, and `A` is a semiring which is an algebra over `R` and also a star ring, and `A` is a star module over `R`, and given a set `S` of star subalgebras of `R` and `A`, the coercion of the infimum of `S` is equal to the intersection over all elements `s` in `S` of the coercion of `s`.
In mathematical terms, this theorem asserts that for any set of star subalgebras in a star module, the infimum of the set (viewed as a subset of the module) is equal to the intersection of the sets corresponding to each subalgebra.
More concisely: Let `R` be a commutative semiring and star ring, `A` a semiring that is an algebra and star module over `R`, and `S` a set of star subalgebras of `R` and `A`. Then, the infimum of `S` as subsets of `A` equals the intersection of the sets of subalgebras in `S`.
|
Subalgebra.star_adjoin_comm
theorem Subalgebra.star_adjoin_comm :
∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (s : Set A),
star (Algebra.adjoin R s) = Algebra.adjoin R (star s)
This theorem states that for any type `R` with a commutative semiring structure, any type `A` with a semiring structure, an algebra structure over `R`, and a star ring structure, and any set `s` of elements of type `A`, the star operation (which is the operation defined in the context of star rings or star modules) commutes with the operation of adjoining elements to an algebra. In other words, taking the star of the algebra derived from adjoining `s` to `R` is the same as adjoining the star of `s` to `R`.
More concisely: For any commutative semiring `R`, type `A` with semiring and algebra structures over `R` and star ring structure, and set `s ⊆ A`, the star operation on `A` commutes with the algebra adjoining operation, i.e., adjoining the stars of elements in `s` to `R` is equivalent to adjoining the elements in `s` to the star ring derived from `R`.
|
StarSubalgebra.algebraMap_mem
theorem StarSubalgebra.algebraMap_mem :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A) (r : R),
(algebraMap R A) r ∈ S
The theorem `StarSubalgebra.algebraMap_mem` states that for any commutative semiring `R`, any star ring `R`, any semiring `A`, any star ring `A`, any algebra structure between `R` and `A`, any star module structure between `R` and `A`, any star subalgebra `S` of `A` over `R`, and any element `r` of `R`, the result of applying the algebra map (which is an embedding from `R` to `A` given by the algebra structure) to `r` is always an element of the star subalgebra `S`.
More concisely: For any commutative semirings R and A, star rings R and A, algebra structures between R and A, star module structures between R and A, star subalgebras S of A over R, and element r in R, the algebra map embedding R into A maps r to an element in S.
|
StarSubalgebra.toSubalgebra_injective
theorem StarSubalgebra.toSubalgebra_injective :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A],
Function.Injective StarSubalgebra.toSubalgebra
The theorem `StarSubalgebra.toSubalgebra_injective` asserts that for any types `R` and `A`, given that `R` is a commutative semiring, a star ring, and an algebra, and `A` is a semiring, a star ring, and a star module over `R`, the function `StarSubalgebra.toSubalgebra` is injective. In other words, if two star subalgebras are mapped to the same subalgebra under the function `StarSubalgebra.toSubalgebra`, then these two star subalgebras were indeed the same to begin with. This is an injectivity property specific to the structure of a star subalgebra within the context of *-ring theory.
More concisely: Given a commutative semiring `R` that is a star ring and an algebra, and a semiring `A` that is a star ring and a star module over `R`, the function `StarSubalgebras.toSubalgebra` mapping star subalgebras of `A` to subalgebras of `R` is injective.
|
StarSubalgebra.star_mem'
theorem StarSubalgebra.star_mem' :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
[inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (self : StarSubalgebra R A) {a : A},
a ∈ self.carrier → star a ∈ self.carrier
This theorem states that for any given `StarSubalgebra` (a star algebra which is also a subalgebra), denoted as `self`, of a commutative semiring `R` and a semiring `A` where `R` and `A` are Star Rings (rings equipped with an additional unary operation called star), and `A` is an `R`-algebra and a Star Module over `R`, if an element `a` from `A` belongs to the carrier set of `self`, then the star of `a` also belongs to the carrier set of `self`. In other words, the carrier set of a `StarSubalgebra` is closed under the `star` operation.
More concisely: If `self` is a `StarSubalgebra` of the commutative semiring `R`, an `R-`algebra and a Star Module over `R`, then the carrier set of `self` is closed under the star operation.
|