StarAlgEquiv.map_star'
theorem StarAlgEquiv.map_star' :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
[inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (self : A ≃⋆ₐ[R] B) (a : A),
self.toFun (star a) = star (self.toFun a)
This theorem states that for any given ⋆-algebra equivalence between two types (A and B), the 'star' operation is preserved. More concretely, for any instance of A, the 'star' of the image of this instance under the equivalence is the same as the image of the 'star' of this instance under the equivalence. This holds across all possible types A and B, and potential additional operations defined on them, as long as they support addition, multiplication, scalar multiplication, and have a defined 'star' operation.
More concisely: For any equivalence between two ⋆-algebras A and B, the star operation is preserved, that is, for all a in A, (f(a))\* = f(a\*) under the given equivalence f, where \* denotes the star operation.
|
StarAlgEquivClass.map_star
theorem StarAlgEquivClass.map_star :
∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} [inst : Add A]
[inst_1 : Mul A] [inst_2 : SMul R A] [inst_3 : Star A] [inst_4 : Add B] [inst_5 : Mul B] [inst_6 : SMul R B]
[inst_7 : Star B] [inst_8 : EquivLike F A B] [inst_9 : NonUnitalAlgEquivClass F R A B]
[self : StarAlgEquivClass F R A B] (f : F) (a : A), f (star a) = star (f a)
The theorem `StarAlgEquivClass.map_star` states that for any ⋆-algebra equivalence `F`, given structures `A` and `B` with algebraic operations of addition, multiplication, scalar multiplication and the `star` operation, and given an element `a` from the structure `A`, the application of `F` on the `star` of `a` is equivalent to the `star` of the application of `F` on `a`. In other words, the ⋆-algebra equivalence `F` preserves the `star` operation.
More concisely: For any star-algebra equivalence F, F(a*) = (F(a))* for all elements a in the star-algebras.
|
NonUnitalStarAlgHom.ext
theorem NonUnitalStarAlgHom.ext :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
[inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
[inst_5 : DistribMulAction R B] [inst_6 : Star B] {f g : A →⋆ₙₐ[R] B}, (∀ (x : A), f x = g x) → f = g
The theorem `NonUnitalStarAlgHom.ext` states that for all types `R`, `A`, and `B`, where `R` is a Monoid, `A` and `B` are NonUnitalNonAssocSemirings with a DistribMulAction from `R` and a `Star` operation, if we have two `Star` algebra homomorphisms (non-unital) `f` and `g` from `A` to `B` over `R`, then if for every element `x` of `A`, `f(x)` equals `g(x)`, it follows that `f` and `g` are the same function. In other words, two `Star` algebra homomorphisms are equal if they map every element of `A` to the same element in `B`.
More concisely: If `f` and `g` are two non-unital star algebra homomorphisms from a NonUnitalNonAssocSemiring `A` to another with a DistribMulAction from a Monoid `R` and a `Star` operation, such that `f(x) = g(x)` for all `x` in `A`, then `f = g`.
|
StarAlgHom.map_star'
theorem StarAlgHom.map_star' :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (self : A →⋆ₐ[R] B) (x : A),
self.toFun (star x) = star (self.toFun x)
This theorem states that, given a ⋆-algebra homomorphism (denoted as `self`), for every element `x` of the original ⋆-algebra, the homomorphism applied to the star of `x` (`self.toFun (star x)`) is equal to the star of the homomorphism applied to `x` (`star (self.toFun x)`). In simpler terms, the ⋆-algebra homomorphism preserves the `star` operation. This is true for all types `R`, `A`, and `B` where `R` is a commutative semiring, `A` and `B` are semirings that are also `R`-algebras, and both `A` and `B` have a `star` operation.
More concisely: For any commutative semiring `R`, and `⋆-algebra homomorphisms `self : A → B` between `R-algebras` `A` and `B`, the star operation is preserved: `self.toFun (star x) = star (self.toFun x)` for all `x ∈ A`.
|
StarAlgEquiv.map_smul'
theorem StarAlgEquiv.map_smul' :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
[inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (self : A ≃⋆ₐ[R] B) (r : R) (a : A),
self.toFun (r • a) = r • self.toFun a
This theorem states that for any types `R`, `A`, and `B`, where `A` and `B` are both star algebras over `R` (i.e., they have addition, multiplication, scalar multiplication, and a star operation defined on them), and `self` is a star-algebra equivalence between `A` and `B`, the action of scalar multiplication commutes with the equivalence. In other words, if you first scale an element `a` in `A` by a scalar `r` and then apply the equivalence, it's the same as if you first apply the equivalence to `a` and then scale the result by `r`. This is expressed by the equation `self.toFun (r • a) = r • self.toFun a`.
More concisely: For any star-algebra equivalence `self` between types `A` and `B`, both being star algebras over a common type `R`, the scalar multiplication of `R` commutes with the equivalence, i.e., `self.toFun (r * a) = r * self.toFun a` for all `r ∈ R` and `a ∈ A`.
|
StarAlgHom.ext
theorem StarAlgHom.ext :
∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] {f g : A →⋆ₐ[R] B},
(∀ (x : A), f x = g x) → f = g
This theorem states that for all types `R`, `A`, `B` where `R` is a commutative semiring, `A` is a semiring, `B` is a semiring, `A` is an `R`-algebra, `B` is an `R`-algebra, `A` has a star operation, and `B` has a star operation, if `f` and `g` are star-algebra homomorphisms from `A` to `B`, then if for all elements `x` in `A`, `f(x)` equals `g(x)`, it follows that `f` and `g` are equal.
More concisely: If `f` and `g` are star-algebra homomorphisms from a commutative semiring `A`, which is an `R`-algebra with a star operation, to another commutative semiring `B`, also an `R`-algebra with a star operation, such that `f(x) = g(x)` for all `x` in `A`, then `f` equals `g`.
|
NonUnitalStarAlgHom.map_star'
theorem NonUnitalStarAlgHom.map_star' :
∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
[inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
[inst_5 : DistribMulAction R B] [inst_6 : Star B] (self : A →⋆ₙₐ[R] B) (a : A),
self.toFun (star a) = star (self.toFun a)
The theorem `NonUnitalStarAlgHom.map_star'` states that for all elements `a` of a type `A`, which is a non-unital, non-associated semiring with a `star` operation and a monoid action by `R`, and for all non-unital ⋆-algebra homomorphisms from `A` to a type `B` (which also a non-unital, non-associated semiring with a `star` operation and a monoid action by `R`), the application of the homomorphism to the `star` of `a` is equal to the `star` of the application of the homomorphism to `a`. In other words, a non-unital ⋆-algebra homomorphism preserves the `star` operation.
More concisely: For any non-unital semiring `A` with a `star` operation and a monoid action by `R`, and any non-unital `⋆`-algebra homomorphism from `A` to a non-unital semiring `B` with `star` operation and monoid action by `R`, the `star` of the image of an element `a` in `A` under the homomorphism is equal to the image of the `star` of `a`.
|