Morphisms of star algebras #
This file defines morphisms between R
-algebras (unital or non-unital) A
and B
where both
A
and B
are equipped with a star
operation. These morphisms, namely StarAlgHom
and
NonUnitalStarAlgHom
are direct extensions of their non-star
red counterparts with a field
map_star
which guarantees they preserve the star operation. We keep the type classes as generic
as possible, in keeping with the definition of NonUnitalAlgHom
in the non-unital case. In this
file, we only assume Star
unless we want to talk about the zero map as a
NonUnitalStarAlgHom
, in which case we need StarAddMonoid
. Note that the scalar ring R
is not required to have a star operation, nor do we need StarRing
or StarModule
structures on
A
and B
.
As with NonUnitalAlgHom
, in the non-unital case the multiplications are not assumed to be
associative or unital, or even to be compatible with the scalar actions. In a typical application,
the operations will satisfy compatibility conditions making them into algebras (albeit possibly
non-associative and/or non-unital) but such conditions are not required here for the definitions.
The primary impetus for defining these types is that they constitute the morphisms in the categories
of unital C⋆-algebras (with StarAlgHom
s) and of C⋆-algebras (with NonUnitalStarAlgHom
s).
Main definitions #
Tags #
non-unital, algebra, morphism, star
Non-unital star algebra homomorphisms #
- toFun : A → B
- map_smul' : ∀ (m : R) (x : A), MulActionHom.toFun s.toMulActionHom (m • x) = m • MulActionHom.toFun s.toMulActionHom x
- map_zero' : MulActionHom.toFun s.toMulActionHom 0 = 0
- map_add' : ∀ (x y : A), MulActionHom.toFun s.toMulActionHom (x + y) = MulActionHom.toFun s.toMulActionHom x + MulActionHom.toFun s.toMulActionHom y
- map_mul' : ∀ (x y : A), MulActionHom.toFun s.toMulActionHom (x * y) = MulActionHom.toFun s.toMulActionHom x * MulActionHom.toFun s.toMulActionHom y
- map_star' : ∀ (a : A), MulActionHom.toFun s.toMulActionHom (star a) = star (MulActionHom.toFun s.toMulActionHom a)
By definition, a non-unital ⋆-algebra homomorphism preserves the
star
operation.
A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between
non-unital R
-algebras A
and B
equipped with a star
operation, and this homomorphism is
also star
-preserving.
Instances For
A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between
non-unital R
-algebras A
and B
equipped with a star
operation, and this homomorphism is
also star
-preserving.
Instances For
A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between
non-unital R
-algebras A
and B
equipped with a star
operation, and this homomorphism is
also star
-preserving.
Instances For
- coe : F → A → B
- coe_injective' : Function.Injective FunLike.coe
- map_zero : ∀ (f : F), ↑f 0 = 0
the maps preserve star
NonUnitalStarAlgHomClass F R A B
asserts F
is a type of bundled non-unital ⋆-algebra
homomorphisms from A
to B
.
Instances
Turn an element of a type F
satisfying NonUnitalStarAlgHomClass F R A B
into an actual
NonUnitalStarAlgHom
. This is declared as the default coercion from F
to A →⋆ₙₐ[R] B
.
Instances For
See Note [custom simps projection]
Instances For
Copy of a NonUnitalStarAlgHom
with a new toFun
equal to the old one. Useful
to fix definitional equalities.
Instances For
The identity as a non-unital ⋆-algebra homomorphism.
Instances For
The composition of non-unital ⋆-algebra homomorphisms, as a non-unital ⋆-algebra homomorphism.
Instances For
Unital star algebra homomorphisms #
- toFun : A → B
- map_one' : OneHom.toFun (↑↑↑s.toAlgHom) 1 = 1
- map_mul' : ∀ (x y : A), OneHom.toFun (↑↑↑s.toAlgHom) (x * y) = OneHom.toFun (↑↑↑s.toAlgHom) x * OneHom.toFun (↑↑↑s.toAlgHom) y
- map_zero' : OneHom.toFun (↑↑↑s.toAlgHom) 0 = 0
- map_add' : ∀ (x y : A), OneHom.toFun (↑↑↑s.toAlgHom) (x + y) = OneHom.toFun (↑↑↑s.toAlgHom) x + OneHom.toFun (↑↑↑s.toAlgHom) y
- commutes' : ∀ (r : R), OneHom.toFun (↑↑↑s.toAlgHom) (↑(algebraMap R A) r) = ↑(algebraMap R B) r
- map_star' : ∀ (x : A), OneHom.toFun (↑↑↑s.toAlgHom) (star x) = star (OneHom.toFun (↑↑↑s.toAlgHom) x)
By definition, a ⋆-algebra homomorphism preserves the
star
operation.
A ⋆-algebra homomorphism is an algebra homomorphism between R
-algebras A
and B
equipped with a star
operation, and this homomorphism is also star
-preserving.
Instances For
A ⋆-algebra homomorphism is an algebra homomorphism between R
-algebras A
and B
equipped with a star
operation, and this homomorphism is also star
-preserving.
Instances For
A ⋆-algebra homomorphism is an algebra homomorphism between R
-algebras A
and B
equipped with a star
operation, and this homomorphism is also star
-preserving.
Instances For
- coe : F → A → B
- coe_injective' : Function.Injective FunLike.coe
- map_one : ∀ (f : F), ↑f 1 = 1
- map_zero : ∀ (f : F), ↑f 0 = 0
- commutes : ∀ (f : F) (r : R), ↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
the maps preserve star
StarAlgHomClass F R A B
states that F
is a type of ⋆-algebra homomorphisms.
You should also extend this typeclass when you extend StarAlgHom
.
Instances
Turn an element of a type F
satisfying StarAlgHomClass F R A B
into an actual
StarAlgHom
. This is declared as the default coercion from F
to A →⋆ₐ[R] B
.
Instances For
Copy of a StarAlgHom
with a new toFun
equal to the old one. Useful
to fix definitional equalities.
Instances For
The identity as a StarAlgHom
.
Instances For
The composition of ⋆-algebra homomorphisms, as a ⋆-algebra homomorphism.
Instances For
Operations on the product type #
Note that this is copied from Algebra.Hom.NonUnitalAlg
.
The first projection of a product is a non-unital ⋆-algebra homomoprhism.
Instances For
The second projection of a product is a non-unital ⋆-algebra homomorphism.
Instances For
The Pi.prod
of two morphisms is a morphism.
Instances For
Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.
Instances For
The left injection into a product is a non-unital algebra homomorphism.
Instances For
The right injection into a product is a non-unital algebra homomorphism.
Instances For
Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.
Instances For
Star algebra equivalences #
- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- map_mul' : ∀ (x y : A), Equiv.toFun s.toEquiv (x * y) = Equiv.toFun s.toEquiv x * Equiv.toFun s.toEquiv y
- map_add' : ∀ (x y : A), Equiv.toFun s.toEquiv (x + y) = Equiv.toFun s.toEquiv x + Equiv.toFun s.toEquiv y
- map_star' : ∀ (a : A), Equiv.toFun s.toEquiv (star a) = star (Equiv.toFun s.toEquiv a)
By definition, a ⋆-algebra equivalence preserves the
star
operation. - map_smul' : ∀ (r : R) (a : A), Equiv.toFun s.toEquiv (r • a) = r • Equiv.toFun s.toEquiv a
By definition, a ⋆-algebra equivalence commutes with the action of scalars.
A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure. Currently, AlgEquiv
requires unital algebras, which is
why this structure does not extend it.
Instances For
A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure. Currently, AlgEquiv
requires unital algebras, which is
why this structure does not extend it.
Instances For
A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar
multiplication and the star operation, which allows for considering both unital and non-unital
equivalences with a single structure. Currently, AlgEquiv
requires unital algebras, which is
why this structure does not extend it.
Instances For
- coe : F → A → B
- inv : F → B → A
- left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
- right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
- coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
By definition, a ⋆-algebra equivalence preserves the
star
operation.By definition, a ⋆-algebra equivalence commutes with the action of scalars.
StarAlgEquivClass F R A B
asserts F
is a type of bundled ⋆-algebra equivalences between
A
and B
.
You should also extend this typeclass when you extend StarAlgEquiv
.
Instances
If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of star algebras.
Instances For
Promote a bijective star algebra homomorphism to a star algebra equivalence.