mathlib3 documentation

algebra.star.star_alg_hom

Morphisms of star algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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.

@[class]

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
@[protected, simp]
@[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]

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_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) :
(f.copy f' h) = f'
theorem non_unital_star_alg_hom.copy_eq {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) :
f.copy f' h = f
@[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

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.star_alg_hom.has_coe_t (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] [hF : 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
@[protected, simp]
theorem star_alg_hom.coe_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 : Type u_1} [star_alg_hom_class F R A B] (f : F) :
@[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_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) :
(f.copy f' h) = f'
theorem star_alg_hom.copy_eq {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) :
f.copy f' h = f
@[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]

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

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

Equations

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
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_apply (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_apply (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_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) (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

Star algebra equivalences #

structure star_alg_equiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :
Type (max u_2 u_3)

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, alg_equiv requires unital algebras, which is why this structure does not extend it.

Instances for star_alg_equiv
def star_alg_equiv.to_ring_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (self : A ≃⋆ₐ[R] B) :
A ≃+* B

Reinterpret a star algebra equivalence as a ring_equiv by forgetting the interaction with the star operation and scalar multiplication.

@[class]
structure star_alg_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :
Type (max u_1 u_3 u_4)

star_alg_equiv_class 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 star_alg_equiv.

Instances of this typeclass
Instances of other typeclasses for star_alg_equiv_class
  • star_alg_equiv_class.has_sizeof_inst
@[nolint, instance]
def star_alg_equiv_class.to_ring_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [self : star_alg_equiv_class F R A B] :
@[protected, nolint, instance]
def star_alg_equiv_class.star_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [hF : star_alg_equiv_class F R A B] :
Equations
@[protected, nolint, instance]
def star_alg_equiv_class.smul_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_star A] [has_smul R A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [hF : star_alg_equiv_class F R A B] :
Equations
@[protected, instance]
def star_alg_equiv_class.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] [hF : star_alg_equiv_class F R A B] :
Equations
@[protected, instance]
def star_alg_equiv.star_alg_equiv_class {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :
Equations
@[protected, instance]
def star_alg_equiv.has_coe_to_fun {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul 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
@[ext]
theorem star_alg_equiv.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {f g : A ≃⋆ₐ[R] B} (h : (a : A), f a = g a) :
f = g
theorem star_alg_equiv.ext_iff {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {f g : A ≃⋆ₐ[R] B} :
f = g (a : A), f a = g a
@[refl]
def star_alg_equiv.refl {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :

Star algebra equivalences are reflexive.

Equations
@[protected, instance]
def star_alg_equiv.inhabited {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :
Equations
@[simp]
theorem star_alg_equiv.coe_refl {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :
@[symm]
def star_alg_equiv.symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :

Star algebra equivalences are symmetric.

Equations
def star_alg_equiv.simps.symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :
B A

See Note [custom simps projection]

Equations
@[simp]
theorem star_alg_equiv.inv_fun_eq_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {e : A ≃⋆ₐ[R] B} :
@[simp]
theorem star_alg_equiv.symm_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :
e.symm.symm = e
@[simp]
theorem star_alg_equiv.mk_coe' {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (f : B A) (h₁ : function.left_inverse e f) (h₂ : function.right_inverse e f) (h₃ : (x y : B), f (x * y) = f x * f y) (h₄ : (x y : B), f (x + y) = f x + f y) (h₅ : (a : B), f (has_star.star a) = has_star.star (f a)) (h₆ : (r : R) (a : B), f (r a) = r f a) :
{to_fun := f, inv_fun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆} = e.symm
@[simp]
theorem star_alg_equiv.symm_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (f : A B) (f' : B A) (h₁ : function.left_inverse f' f) (h₂ : function.right_inverse f' f) (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)) (h₆ : (r : R) (a : A), f (r a) = r f a) :
{to_fun := f, inv_fun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆}.symm = {to_fun := f', inv_fun := f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}
theorem star_alg_equiv.to_ring_equiv_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (f : A ≃⋆ₐ[R] B) :
@[simp]
theorem star_alg_equiv.symm_to_ring_equiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :
@[trans]
def star_alg_equiv.trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :

Star algebra equivalences are transitive.

Equations
@[simp]
theorem star_alg_equiv.apply_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (x : B) :
e ((e.symm) x) = x
@[simp]
theorem star_alg_equiv.symm_apply_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (x : A) :
(e.symm) (e x) = x
@[simp]
theorem star_alg_equiv.symm_trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : C) :
((e₁.trans e₂).symm) x = (e₁.symm) ((e₂.symm) x)
@[simp]
theorem star_alg_equiv.coe_trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem star_alg_equiv.trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : A) :
(e₁.trans e₂) x = e₂ (e₁ x)
theorem star_alg_equiv.left_inverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :
theorem star_alg_equiv.right_inverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) :
def star_alg_equiv.of_star_alg_hom {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : 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] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : (x : A), g (f x) = x) (h₂ : (x : B), f (g x) = x) :

If a (unital or non-unital) star algebra morphism has an inverse, it is an isomorphism of star algebras.

Equations
@[simp]
theorem star_alg_equiv.of_star_alg_hom_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : 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] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : (x : A), g (f x) = x) (h₂ : (x : B), f (g x) = x) (a : A) :
@[simp]
theorem star_alg_equiv.of_star_alg_hom_symm_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : 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] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : (x : A), g (f x) = x) (h₂ : (x : B), f (g x) = x) (a : B) :

Promote a bijective star algebra homomorphism to a star algebra equivalence.

Equations