NonUnitalStarSubalgebra.star_mem'
theorem NonUnitalStarSubalgebra.star_mem' :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : Star A] (self : NonUnitalStarSubalgebra R A) {a : A}, a ∈ self.carrier → star a ∈ self.carrier
The theorem `NonUnitalStarSubalgebra.star_mem'` states that for any types `R` and `A` where `R` is a commutative semiring, `A` is a non-unital non-associative semiring and also a module over `R`, and `A` has a `star` operation (which typically represents the complex conjugate), if an element `a` belongs to the carrier of a `NonUnitalStarSubalgebra`, then its `star` (or conjugate) also belongs to the same `NonUnitalStarSubalgebra`. This means the carrier set of a `NonUnitalStarSubalgebra` is closed under the `star` operation.
More concisely: In a commutative semiring `R`, if `A` is a non-unital non-associative `R`-module semiring with a `star` operation, then the carrier of any `NonUnitalStarSubalgebra` of `A` is closed under the `star` operation.
|
NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective
theorem NonUnitalStarSubalgebra.toNonUnitalSubalgebra_injective :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : Star A], Function.Injective NonUnitalStarSubalgebra.toNonUnitalSubalgebra
This theorem states that for any commutative semiring `R` and any non-unital, non-associative semiring `A` that is also a module over `R` and posseses a star operation, the function `NonUnitalStarSubalgebra.toNonUnitalSubalgebra` is injective. In other words, if `A` and `B` are two non-unital star subalgebras of `R` such that their corresponding non-unital subalgebras are equal (as determined by `toNonUnitalSubalgebra`), then `A` and `B` were already equal.
More concisely: Given commutative semirings `R`, a non-unital, non-associative semiring `A` over `R` with a star operation, if `toNonUnitalSubalgebra R A = toNonUnitalSubalgebra R B` for non-unital subalgebras `A` and `B`, then `A = B`.
|
NonUnitalStarAlgebra.coe_sInf
theorem NonUnitalStarAlgebra.coe_sInf :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
[inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
[inst_7 : StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)), ↑(sInf S) = ⋂ s ∈ S, ↑s
This theorem states that for any set `S` of elements of type `NonUnitalStarSubalgebra` over a commutative semiring `R` and a non-unital semiring `A` with some additional properties (like being a star ring, a module, obeying the scalar tower property, the scalar multiplication commutative property and being a star module), the underlying set of the infimum (`sInf`) of `S` is equal to the intersection of the underlying sets of all elements in `S`.
In other words, when we look at the set of all elements belonging to any non-unital star subalgebra in `S`, and take its smallest non-unital star subalgebra (if it exists), its elements are precisely the elements that belong to every non-unital star subalgebra in `S`.
More concisely: For any set `S` of non-unital star subalgebras over a commutative semiring `R` with additional properties, the underlying set of their infimum equals the intersection of the underlying sets of all elements in `S`.
|
NonUnitalSubalgebra.star_adjoin_comm
theorem NonUnitalSubalgebra.star_adjoin_comm :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
[inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
[inst_7 : StarModule R A] (s : Set A), star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s)
This theorem, `NonUnitalSubalgebra.star_adjoin_comm`, asserts that the star operation (an involution or conjugation operation commonly used in the study of *-algebras) commutes with the `NonUnitalAlgebra.adjoin` operation. More specifically, for any commutative semiring `R`, any star ring `R` and `A`, any non-unital semiring `A`, any module `A` over `R`, and any set `s` of type `A`, the star of the non-unital subalgebra generated by `s` is the same as the non-unital subalgebra generated by the star of `s`. Here `NonUnitalAlgebra.adjoin` is used to denote the smallest non-unital subalgebra containing a given set.
More concisely: For any commutative semiring `R`, star ring `R` over `R`, non-unital semiring `A` with module structure over `R`, and set `s` of elements in `A`, the non-unital subalgebra generated by the stars of elements in `s` equals the non-unital subalgebra generated by `s` in the star algebra of `A`.
|
NonUnitalStarSubalgebra.ext
theorem NonUnitalStarSubalgebra.ext :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
[inst_3 : Star A] {S T : NonUnitalStarSubalgebra R A}, (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any two sets, S and T, which are non-unital star subalgebras over a module A of a commutative semiring R (where A has a star operation), if every element of A is in S if and only if it is in T, then S and T are equal. Basically, if two non-unital star subalgebras of a module have the same elements, they are the same non-unital star subalgebra.
More concisely: If two non-unital star subalgebras S and T over a module A in a commutative semiring R with a star operation have the same elements, then S = T.
|
NonUnitalStarAlgebra.mem_top
theorem NonUnitalStarAlgebra.mem_top :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
[inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
[inst_7 : StarModule R A] {x : A}, x ∈ ⊤
This theorem states that for any `x` of type `A`, `x` is an element of top element `⊤`. Here, `R` is a type with the structure of a commutative semiring and a star ring, `A` is a type with the structure of a non-unital semiring, star ring, module over `R`, and star module over `R`. The scalar multiplications in `R` and `A` are assumed to be compatible, forming a scalar tower and satisfying the commutative property.
More concisely: For any element `x` of type `A` in a commutative semiring `R` with star ring structure, `x` belongs to the top element `⊤` of the non-unital semiring `A`, which is also a star module and a star ring over `R`, with compatible scalar multiplications.
|
NonUnitalStarAlgebra.gc
theorem NonUnitalStarAlgebra.gc :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
[inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
[inst_7 : StarModule R A], GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe
The theorem `NonUnitalStarAlgebra.gc` states that for any commutative semiring `R`, any non-unital semiring `A`, where `R` and `A` are both star rings and `A` is a module over `R` with the scalar multiplication satisfying the commutative law and tower law, and also `A` is a star module over `R`, there exists a Galois Connection between the operation of adjoining `R` to a non-unital star algebra and the operation of converting a `SetLike` object to its corresponding set. In other words, if `adjoin` is the left adjoint (`l` in the definition of Galois Connection) and `SetLike.coe` is the right adjoint (`u` in the definition), then for any `a` from the order `α` and `b` from the order `β`, `l a ≤ b` if and only if `a ≤ u b`, where `≤` denotes the order relation in the corresponding orders.
More concisely: Given a commutative semiring `R`, a non-unital semiring `A` that is a star ring, a module over `R`, and a star module over `R`, there exists a Galois Connection between the operation of adjoining `R` to `A` and the operation of taking the set of elements of a `SetLike` object over `A`, such that for all `a` in one order and `b` in the other, `a` is less than or equal to `b` in the former if and only if `a` is less than or equal to the image of `b` in the latter.
|