mathlib documentation

algebra.star.star_alg_hom

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 star_alg_hom and non_unital_star_alg_hom are direct extensions of their non-starred 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 non_unital_alg_hom in the non-unital case. In this file, we only assume has_star unless we want to talk about the zero map as a non_unital_star_alg_hom, in which case we need star_add_monoid. Note that the scalar ring R is not required to have a star operation, nor do we need star_ring or star_module structures on A and B.

As with non_unital_alg_hom, 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 star_alg_homs) and of C⋆-algebras (with non_unital_star_alg_homs).

TODO: add star_alg_equiv.

Main definitions #

Tags #

non-unital, algebra, morphism, star

Non-unital star algebra homomorphisms #

structure non_unital_star_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :
Type (max u_2 u_3)

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 non_unital_star_alg_hom

Reinterpret a non-unital star algebra homomorphism as a non-unital algebra homomorphism by forgetting the interaction with the star operation.

@[nolint, instance]
@[class]
structure non_unital_star_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [has_star A] [has_star B] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] :
Type (max u_1 u_3 u_4)

non_unital_star_alg_hom_class F R A B asserts F is a type of bundled non-unital ⋆-algebra homomorphisms from A to B.

Instances of this typeclass
Instances of other typeclasses for non_unital_star_alg_hom_class
  • non_unital_star_alg_hom_class.has_sizeof_inst
@[protected, instance]

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem non_unital_star_alg_hom.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] {f g : A →⋆ₙₐ[R] B} (h : ∀ (x : A), f x = g x) :
f = g
@[protected]
def non_unital_star_alg_hom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = f) :

Copy of a non_unital_star_alg_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem non_unital_star_alg_hom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A → B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = f x * f y) (h₅ : ∀ (a : A), f (has_star.star a) = has_star.star (f a)) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅} = f
@[simp]
theorem non_unital_star_alg_hom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), f (m x) = m f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = f x * f y) (h₅ : ∀ (a : A), f (has_star.star a) = has_star.star (f a)) :
{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅} = f
@[protected]

The identity as a non-unital ⋆-algebra homomorphism.

Equations

The composition of non-unital ⋆-algebra homomorphisms, as a non-unital ⋆-algebra homomorphism.

Equations
@[simp]
theorem non_unital_star_alg_hom.coe_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) :
(f.comp g) = f g
@[simp]
theorem non_unital_star_alg_hom.comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A) :
(f.comp g) a = f (g a)
@[simp]
theorem non_unital_star_alg_hom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] [non_unital_non_assoc_semiring D] [distrib_mul_action R D] [has_star D] (f : C →⋆ₙₐ[R] D) (g : B →⋆ₙₐ[R] C) (h : A →⋆ₙₐ[R] B) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem non_unital_star_alg_hom.coe_one {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] :
theorem non_unital_star_alg_hom.one_apply {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] (a : A) :
1 a = a

Unital star algebra homomorphisms #

def star_alg_hom.to_alg_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (self : A →⋆ₐ[R] B) :

Reinterpret a unital star algebra homomorphism as a unital algebra homomorphism by forgetting the interaction with the star operation.

structure star_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :
Type (max u_2 u_3)

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 star_alg_hom
@[nolint, instance]
def star_alg_hom_class.to_star_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [self : star_alg_hom_class F R A B] :
@[instance]
def star_alg_hom_class.to_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [self : star_alg_hom_class F R A B] :
@[class]
structure star_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :
Type (max u_1 u_3 u_4)

star_alg_hom_class F R A B states that F is a type of ⋆-algebra homomorphisms.

You should also extend this typeclass when you extend star_alg_hom.

Instances of this typeclass
Instances of other typeclasses for star_alg_hom_class
  • star_alg_hom_class.has_sizeof_inst
@[protected, instance]
def star_alg_hom_class.to_non_unital_star_alg_hom_class (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [star_alg_hom_class F R A B] :
Equations
@[protected, instance]
def star_alg_hom.star_alg_hom_class {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :
Equations
@[protected, instance]
def star_alg_hom.has_coe_to_fun {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :
has_coe_to_fun (A →⋆ₐ[R] B) (λ (_x : A →⋆ₐ[R] B), A → B)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem star_alg_hom.coe_to_alg_hom {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] {f : A →⋆ₐ[R] B} :
@[ext]
theorem star_alg_hom.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] {f g : A →⋆ₐ[R] B} (h : ∀ (x : A), f x = g x) :
f = g
@[protected]
def star_alg_hom.copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = f) :

Copy of a star_alg_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem star_alg_hom.coe_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A → B) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A) r) = (algebra_map R B) r) (h₆ : ∀ (x : A), f (has_star.star x) = has_star.star (f x)) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆} = f
@[simp]
theorem star_alg_hom.mk_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f ((algebra_map R A) r) = (algebra_map R B) r) (h₆ : ∀ (x : A), f (has_star.star x) = has_star.star (f x)) :
{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆} = f
@[protected]
def star_alg_hom.id (R : Type u_2) (A : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] :

The identity as a star_alg_hom.

Equations
@[simp]
theorem star_alg_hom.coe_id (R : Type u_2) (A : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] :
@[protected, instance]
def star_alg_hom.inhabited {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] :
Equations
def star_alg_hom.comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :

The composition of ⋆-algebra homomorphisms, as a ⋆-algebra homomorphism.

Equations
@[simp]
theorem star_alg_hom.coe_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :
(f.comp g) = f g
@[simp]
theorem star_alg_hom.comp_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) (a : A) :
(f.comp g) a = f (g a)
@[simp]
theorem star_alg_hom.comp_assoc {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] [semiring D] [algebra R D] [has_star D] (f : C →⋆ₐ[R] D) (g : B →⋆ₐ[R] C) (h : A →⋆ₐ[R] B) :
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem star_alg_hom.id_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) :
@[simp]
theorem star_alg_hom.comp_id {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) :
@[protected, instance]
def star_alg_hom.monoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] :
Equations
def star_alg_hom.to_non_unital_star_alg_hom {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) :

A unital morphism of ⋆-algebras is a non_unital_star_alg_hom.

Equations
@[simp]
theorem star_alg_hom.coe_to_non_unital_star_alg_hom {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) :

Operations on the product type #

Note that this is copied from algebra/hom/non_unital_alg.

The first projection of a product is a non-unital ⋆-algebra homomoprhism.

Equations
@[simp]
@[simp]

The second projection of a product is a non-unital ⋆-algebra homomorphism.

Equations

The pi.prod of two morphisms is a morphism.

Equations
@[simp]
@[simp]

Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

Equations

The left injection into a product is a non-unital algebra homomorphism.

Equations

The right injection into a product is a non-unital algebra homomorphism.

Equations
@[simp]
def star_alg_hom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

The first projection of a product is a ⋆-algebra homomoprhism.

Equations
@[simp]
theorem star_alg_hom.fst_to_fun (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (ᾰ : A × B) :
(star_alg_hom.fst R A B) = (alg_hom.fst R A B).to_fun
@[simp]
theorem star_alg_hom.snd_to_fun (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (ᾰ : A × B) :
(star_alg_hom.snd R A B) = (alg_hom.snd R A B).to_fun
def star_alg_hom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

The second projection of a product is a ⋆-algebra homomorphism.

Equations
@[simp]
theorem star_alg_hom.prod_to_fun {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) (ᾰ : A) :
def star_alg_hom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :

The pi.prod of two morphisms is a morphism.

Equations
theorem star_alg_hom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
@[simp]
theorem star_alg_hom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
(star_alg_hom.fst R B C).comp (f.prod g) = f
@[simp]
theorem star_alg_hom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :
(star_alg_hom.snd R B C).comp (f.prod g) = g
@[simp]
theorem star_alg_hom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :
@[simp]
theorem star_alg_hom.prod_equiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B × C) :
@[simp]
theorem star_alg_hom.prod_equiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)) :
def star_alg_hom.prod_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] :
(A →⋆ₐ[R] B) × (A →⋆ₐ[R] C) (A →⋆ₐ[R] B × C)

Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

Equations