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-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 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 StarAlgHoms) and of C⋆-algebras (with NonUnitalStarAlgHoms).

Main definitions

• NonUnitalStarAlgHom
• StarAlgHom

Tags

non-unital, algebra, morphism, star

Non-unital star algebra homomorphisms

structure NonUnitalStarAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] extends NonUnitalAlgHom : Type (max u_2 u_3)

• 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.

def «term_→⋆ₙₐ_» : Lean.TrailingParserDescr

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.

def «term_→⋆ₙₐ[_]_» : Lean.TrailingParserDescr

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.

class NonUnitalStarAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Monoid R] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] extends NonUnitalAlgHomClass : Type (max (max u_1 u_3) u_4)

• coe : F → A → B
• coe_injective' : Function.Injective FunLike.coe
• map_smul : ∀ (f : F) (c : R) (x : A), ↑f (c • x) = c • ↑f x
• map_add : ∀ (f : F) (x y : A), ↑f (x + y) = ↑f x + ↑f y
• map_zero : ∀ (f : F), ↑f 0 = 0
• map_mul : ∀ (f : F) (x y : A), ↑f (x * y) = ↑f x * ↑f y
• map_star : ∀ (f : F) (r : A), ↑f (star r) = star (↑f r)

  the maps preserve star

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

def NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalStarAlgHomClass F R A B] (f : F) : A →⋆ₙₐ[R] B

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.

instance NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalStarAlgHomClass F R A B] : CoeTC F (A →⋆ₙₐ[R] B)

instance NonUnitalStarAlgHom.instNonUnitalStarAlgHomClassNonUnitalStarAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] : NonUnitalStarAlgHomClass (A →⋆ₙₐ[R] B) R A B

def NonUnitalStarAlgHom.Simps.apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) : A → B

See Note [custom simps projection]

@[simp]

theorem NonUnitalStarAlgHom.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {F : Type u_6} [NonUnitalStarAlgHomClass F R A B] (f : F) : ↑↑f = ↑f

@[simp]

theorem NonUnitalStarAlgHom.coe_toNonUnitalAlgHom {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {f : A →⋆ₙₐ[R] B} : ↑f.toNonUnitalAlgHom = ↑f

theorem NonUnitalStarAlgHom.ext {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] {f : A →⋆ₙₐ[R] B} {g : A →⋆ₙₐ[R] B} (h : ∀ (x : A), ↑f x = ↑g x) : f = g

def NonUnitalStarAlgHom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ↑f) : A →⋆ₙₐ[R] B

Copy of a NonUnitalStarAlgHom with a new toFun equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem NonUnitalStarAlgHom.coe_copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ↑f) : ↑(NonUnitalStarAlgHom.copy f f' h) = f'

theorem NonUnitalStarAlgHom.copy_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ↑f) : NonUnitalStarAlgHom.copy f f' h = f

@[simp]

theorem NonUnitalStarAlgHom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A → B) (h₁ : ∀ (m : R) (x : A), f (m • x) = m • f x) (h₂ : MulActionHom.toFun { toFun := f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) (h₅ : ∀ (a : A), MulActionHom.toFun { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom (star a) = star (MulActionHom.toFun { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom a)) : ↑{ toNonUnitalAlgHom := { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }, map_star' := h₅ } = f

@[simp]

theorem NonUnitalStarAlgHom.coe_mk' {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →ₙₐ[R] B) (h : ∀ (a : A), MulActionHom.toFun f.toMulActionHom (star a) = star (MulActionHom.toFun f.toMulActionHom a)) : ↑{ toNonUnitalAlgHom := f, map_star' := h } = ↑f

@[simp]

theorem NonUnitalStarAlgHom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), ↑f (m • x) = m • ↑f x) (h₂ : MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } 0 = 0) (h₃ : ∀ (x y : A), MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } (x + y) = MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } x + MulActionHom.toFun { toFun := ↑f, map_smul' := h₁ } y) (h₄ : ∀ (x y : A), MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom (x * y) = MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom x * MulActionHom.toFun { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom y) (h₅ : ∀ (a : A), MulActionHom.toFun { toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom (star a) = star (MulActionHom.toFun { toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom a)) : { toNonUnitalAlgHom := { toDistribMulActionHom := { toMulActionHom := { toFun := ↑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }, map_star' := h₅ } = f

def NonUnitalStarAlgHom.id (R : Type u_1) (A : Type u_2) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] : A →⋆ₙₐ[R] A

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

@[simp]

theorem NonUnitalStarAlgHom.coe_id (R : Type u_1) (A : Type u_2) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] : ↑(NonUnitalStarAlgHom.id R A) = id

def NonUnitalStarAlgHom.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) : A →⋆ₙₐ[R] C

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

@[simp]

theorem NonUnitalStarAlgHom.coe_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) : ↑(NonUnitalStarAlgHom.comp f g) = ↑f ∘ ↑g

@[simp]

theorem NonUnitalStarAlgHom.comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A) : ↑(NonUnitalStarAlgHom.comp f g) a = ↑f (↑g a)

@[simp]

theorem NonUnitalStarAlgHom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] [NonUnitalNonAssocSemiring D] [DistribMulAction R D] [Star D] (f : C →⋆ₙₐ[R] D) (g : B →⋆ₙₐ[R] C) (h : A →⋆ₙₐ[R] B) : NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.comp f g) h = NonUnitalStarAlgHom.comp f (NonUnitalStarAlgHom.comp g h)

@[simp]

theorem NonUnitalStarAlgHom.id_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) : NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.id R B) f = f

@[simp]

theorem NonUnitalStarAlgHom.comp_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) : NonUnitalStarAlgHom.comp f (NonUnitalStarAlgHom.id R A) = f

instance NonUnitalStarAlgHom.instMonoidNonUnitalStarAlgHom {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] : Monoid (A →⋆ₙₐ[R] A)

@[simp]

theorem NonUnitalStarAlgHom.coe_one {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] : ↑1 = id

theorem NonUnitalStarAlgHom.one_apply {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] (a : A) : ↑1 a = a

instance NonUnitalStarAlgHom.instZeroNonUnitalStarAlgHomToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarToInvolutiveStarToAddMonoidToAddCommMonoid {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : Zero (A →⋆ₙₐ[R] B)

instance NonUnitalStarAlgHom.instInhabitedNonUnitalStarAlgHomToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarToInvolutiveStarToAddMonoidToAddCommMonoid {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : Inhabited (A →⋆ₙₐ[R] B)

instance NonUnitalStarAlgHom.instMonoidWithZeroNonUnitalStarAlgHomToStarToInvolutiveStarToAddMonoidToAddCommMonoid {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] : MonoidWithZero (A →⋆ₙₐ[R] A)

@[simp]

theorem NonUnitalStarAlgHom.coe_zero {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : ↑0 = 0

theorem NonUnitalStarAlgHom.zero_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] (a : A) : ↑0 a = 0

Unital star algebra homomorphisms

structure StarAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] extends AlgHom : Type (max u_2 u_3)

• 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.

def «term_→⋆ₐ_» : Lean.TrailingParserDescr

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.

def «term_→⋆ₐ[_]_» : Lean.TrailingParserDescr

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.

class StarAlgHomClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] extends AlgHomClass : Type (max (max u_1 u_3) u_4)

• coe : F → A → B
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : A), ↑f (x * y) = ↑f x * ↑f y
• map_one : ∀ (f : F), ↑f 1 = 1
• map_add : ∀ (f : F) (x y : A), ↑f (x + y) = ↑f x + ↑f y
• map_zero : ∀ (f : F), ↑f 0 = 0
• commutes : ∀ (f : F) (r : R), ↑f (↑(algebraMap R A) r) = ↑(algebraMap R B) r
• map_star : ∀ (f : F) (r : A), ↑f (star r) = star (↑f 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.

instance StarAlgHomClass.toNonUnitalStarAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [StarAlgHomClass F R A B] : NonUnitalStarAlgHomClass F R A B

def StarAlgHomClass.toStarAlgHom {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [hF : StarAlgHomClass F R A B] (f : F) : A →⋆ₐ[R] B

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.

instance StarAlgHomClass.instCoeTCStarAlgHom (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [hF : StarAlgHomClass F R A B] : CoeTC F (A →⋆ₐ[R] B)

instance StarAlgHom.instStarAlgHomClassStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] : StarAlgHomClass (A →⋆ₐ[R] B) R A B

@[simp]

theorem StarAlgHom.coe_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {F : Type u_7} [StarAlgHomClass F R A B] (f : F) : ↑↑f = ↑f

def StarAlgHom.Simps.apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) : A → B

See Note [custom simps projection]

@[simp]

theorem StarAlgHom.coe_toAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {f : A →⋆ₐ[R] B} : ↑f.toAlgHom = ↑f

theorem StarAlgHom.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] {f : A →⋆ₐ[R] B} {g : A →⋆ₐ[R] B} (h : ∀ (x : A), ↑f x = ↑g x) : f = g

def StarAlgHom.copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ↑f) : A →⋆ₐ[R] B

Copy of a StarAlgHom with a new toFun equal to the old one. Useful to fix definitional equalities.

@[simp]

theorem StarAlgHom.coe_copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ↑f) : ↑(StarAlgHom.copy f f' h) = f'

theorem StarAlgHom.copy_eq {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ↑f) : StarAlgHom.copy f f' h = f

@[simp]

theorem StarAlgHom.coe_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A → B) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), OneHom.toFun { toFun := f, map_one' := h₁ } (x * y) = OneHom.toFun { toFun := f, map_one' := h₁ } x * OneHom.toFun { toFun := f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x y : A), OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x + OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y) (h₅ : ∀ (r : R), OneHom.toFun (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) (h₆ : ∀ (x : A), OneHom.toFun (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }) (star x) = star (OneHom.toFun (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }) x)) : ↑{ toAlgHom := { toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }, map_star' := h₆ } = f

@[simp]

theorem StarAlgHom.coe_mk' {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →ₐ[R] B) (h : ∀ (x : A), OneHom.toFun (↑↑↑f) (star x) = star (OneHom.toFun (↑↑↑f) x)) : ↑{ toAlgHom := f, map_star' := h } = ↑f

@[simp]

theorem StarAlgHom.mk_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (h₁ : ↑f 1 = 1) (h₂ : ∀ (x y : A), OneHom.toFun { toFun := ↑f, map_one' := h₁ } (x * y) = OneHom.toFun { toFun := ↑f, map_one' := h₁ } x * OneHom.toFun { toFun := ↑f, map_one' := h₁ } y) (h₃ : OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x y : A), OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) x + OneHom.toFun (↑{ toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }) y) (h₅ : ∀ (r : R), OneHom.toFun (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }) (↑(algebraMap R A) r) = ↑(algebraMap R B) r) (h₆ : ∀ (x : A), OneHom.toFun (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }) (star x) = star (OneHom.toFun (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }) x)) : { toAlgHom := { toRingHom := { toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }, map_star' := h₆ } = f

def StarAlgHom.id (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] : A →⋆ₐ[R] A

The identity as a StarAlgHom.

@[simp]

theorem StarAlgHom.coe_id (R : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] : ↑(StarAlgHom.id R A) = id

instance StarAlgHom.instInhabitedStarAlgHom {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] : Inhabited (A →⋆ₐ[R] A)

def StarAlgHom.comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) : A →⋆ₐ[R] C

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

@[simp]

theorem StarAlgHom.coe_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) : ↑(StarAlgHom.comp f g) = ↑f ∘ ↑g

@[simp]

theorem StarAlgHom.comp_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) (a : A) : ↑(StarAlgHom.comp f g) a = ↑f (↑g a)

@[simp]

theorem StarAlgHom.comp_assoc {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] [Semiring D] [Algebra R D] [Star D] (f : C →⋆ₐ[R] D) (g : B →⋆ₐ[R] C) (h : A →⋆ₐ[R] B) : StarAlgHom.comp (StarAlgHom.comp f g) h = StarAlgHom.comp f (StarAlgHom.comp g h)

@[simp]

theorem StarAlgHom.id_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) : StarAlgHom.comp (StarAlgHom.id R B) f = f

@[simp]

theorem StarAlgHom.comp_id {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) : StarAlgHom.comp f (StarAlgHom.id R A) = f

instance StarAlgHom.instMonoidStarAlgHom {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] : Monoid (A →⋆ₐ[R] A)

def StarAlgHom.toNonUnitalStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) : A →⋆ₙₐ[R] B

A unital morphism of ⋆-algebras is a NonUnitalStarAlgHom.

@[simp]

theorem StarAlgHom.coe_toNonUnitalStarAlgHom {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) : ↑(StarAlgHom.toNonUnitalStarAlgHom f) = ↑f

Operations on the product type

Note that this is copied from Algebra.Hom.NonUnitalAlg.

@[simp]

theorem NonUnitalStarAlgHom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (self : A × B) : ↑(NonUnitalStarAlgHom.fst R A B) self = self.fst

def NonUnitalStarAlgHom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] : A × B →⋆ₙₐ[R] A

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

@[simp]

theorem NonUnitalStarAlgHom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (self : A × B) : ↑(NonUnitalStarAlgHom.snd R A B) self = self.snd

def NonUnitalStarAlgHom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] : A × B →⋆ₙₐ[R] B

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

@[simp]

theorem NonUnitalStarAlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) (i : A) : ↑(NonUnitalStarAlgHom.prod f g) i = (↑f i, ↑g i)

def NonUnitalStarAlgHom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : A →⋆ₙₐ[R] B × C

The Pi.prod of two morphisms is a morphism.

theorem NonUnitalStarAlgHom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ↑(NonUnitalStarAlgHom.prod f g) = Pi.prod ↑f ↑g

@[simp]

theorem NonUnitalStarAlgHom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.fst R B C) (NonUnitalStarAlgHom.prod f g) = f

@[simp]

theorem NonUnitalStarAlgHom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.snd R B C) (NonUnitalStarAlgHom.prod f g) = g

@[simp]

theorem NonUnitalStarAlgHom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] : NonUnitalStarAlgHom.prod (NonUnitalStarAlgHom.fst R A B) (NonUnitalStarAlgHom.snd R A B) = 1

@[simp]

theorem NonUnitalStarAlgHom.prodEquiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : A →⋆ₙₐ[R] B × C) : ↑NonUnitalStarAlgHom.prodEquiv.symm f = (NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.fst R B C) f, NonUnitalStarAlgHom.comp (NonUnitalStarAlgHom.snd R B C) f)

@[simp]

theorem NonUnitalStarAlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [Star C] (f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)) : ↑NonUnitalStarAlgHom.prodEquiv f = NonUnitalStarAlgHom.prod f.fst f.snd

def NonUnitalStarAlgHom.prodEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [NonUnitalNonAssocSemiring C] [DistribMulAction R C] [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.

def NonUnitalStarAlgHom.inl (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : A →⋆ₙₐ[R] A × B

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

def NonUnitalStarAlgHom.inr (R : Type u_1) (A : Type u_2) (B : Type u_3) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : B →⋆ₙₐ[R] A × B

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

@[simp]

theorem NonUnitalStarAlgHom.coe_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : ↑(NonUnitalStarAlgHom.inl R A B) = fun x => (x, 0)

theorem NonUnitalStarAlgHom.inl_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] (x : A) : ↑(NonUnitalStarAlgHom.inl R A B) x = (x, 0)

@[simp]

theorem NonUnitalStarAlgHom.coe_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] : ↑(NonUnitalStarAlgHom.inr R A B) = Prod.mk 0

theorem NonUnitalStarAlgHom.inr_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [StarAddMonoid B] (x : B) : ↑(NonUnitalStarAlgHom.inr R A B) x = (0, x)

@[simp]

theorem StarAlgHom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (self : A × B) : ↑(StarAlgHom.fst R A B) self = self.fst

def StarAlgHom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] : A × B →⋆ₐ[R] A

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

@[simp]

theorem StarAlgHom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (self : A × B) : ↑(StarAlgHom.snd R A B) self = self.snd

def StarAlgHom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] : A × B →⋆ₐ[R] B

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

@[simp]

theorem StarAlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) (x : A) : ↑(StarAlgHom.prod f g) x = (↑f x, ↑g x)

def StarAlgHom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : A →⋆ₐ[R] B × C

The Pi.prod of two morphisms is a morphism.

theorem StarAlgHom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : ↑(StarAlgHom.prod f g) = Pi.prod ↑f ↑g

@[simp]

theorem StarAlgHom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : StarAlgHom.comp (StarAlgHom.fst R B C) (StarAlgHom.prod f g) = f

@[simp]

theorem StarAlgHom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : StarAlgHom.comp (StarAlgHom.snd R B C) (StarAlgHom.prod f g) = g

@[simp]

theorem StarAlgHom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] : StarAlgHom.prod (StarAlgHom.fst R A B) (StarAlgHom.snd R A B) = 1

@[simp]

theorem StarAlgHom.prodEquiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : A →⋆ₐ[R] B × C) : ↑StarAlgHom.prodEquiv.symm f = (StarAlgHom.comp (StarAlgHom.fst R B C) f, StarAlgHom.comp (StarAlgHom.snd R B C) f)

@[simp]

theorem StarAlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [Star C] (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)) : ↑StarAlgHom.prodEquiv f = StarAlgHom.prod f.fst f.snd

def StarAlgHom.prodEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [Semiring C] [Algebra R C] [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.

Star algebra equivalences

structure StarAlgEquiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] extends RingEquiv : Type (max u_2 u_3)

• 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.

def «term_≃⋆ₐ_» : Lean.TrailingParserDescr

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.

def «term_≃⋆ₐ[_]_» : Lean.TrailingParserDescr

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.

class StarAlgEquivClass (F : Type u_1) (R : outParam (Type u_2)) (A : outParam (Type u_3)) (B : outParam (Type u_4)) [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B] [Star B] extends RingEquivClass : Type (max (max u_1 u_3) u_4)

• 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
• map_mul : ∀ (f : F) (a b : A), ↑f (a * b) = ↑f a * ↑f b
• map_add : ∀ (f : F) (a b : A), ↑f (a + b) = ↑f a + ↑f b
• map_star : ∀ (f : F) (a : A), ↑f (star a) = star (↑f a)

  By definition, a ⋆-algebra equivalence preserves the star operation.

• map_smul : ∀ (f : F) (r : R) (a : A), ↑f (r • a) = r • ↑f a

  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.

instance StarAlgEquivClass.instStarHomClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Mul A] [SMul R A] [Star A] [Add B] [Mul B] [SMul R B] [Star B] [hF : StarAlgEquivClass F R A B] : StarHomClass F A B

instance StarAlgEquivClass.instSMulHomClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Mul A] [Star A] [SMul R A] [Add B] [Mul B] [SMul R B] [Star B] [hF : StarAlgEquivClass F R A B] : SMulHomClass F R A B

instance StarAlgEquivClass.instNonUnitalStarAlgHomClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : StarAlgEquivClass F R A B] : NonUnitalStarAlgHomClass F R A B

instance StarAlgEquivClass.instStarAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] [hF : StarAlgEquivClass F R A B] : StarAlgHomClass F R A B

instance StarAlgEquivClass.toAlgEquivClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] [Star A] [Star B] [StarAlgEquivClass F R A B] : AlgEquivClass F R A B

instance StarAlgEquiv.instStarAlgEquivClassStarAlgEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] : StarAlgEquivClass (A ≃⋆ₐ[R] B) R A B

@[simp]

theorem StarAlgEquiv.toRingEquiv_eq_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : e.toRingEquiv = ↑e

theorem StarAlgEquiv.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {f : A ≃⋆ₐ[R] B} {g : A ≃⋆ₐ[R] B} (h : ∀ (a : A), ↑f a = ↑g a) : f = g

theorem StarAlgEquiv.ext_iff {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {f : A ≃⋆ₐ[R] B} {g : A ≃⋆ₐ[R] B} : f = g ↔ ∀ (a : A), ↑f a = ↑g a

def StarAlgEquiv.refl {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] : A ≃⋆ₐ[R] A

Star algebra equivalences are reflexive.

instance StarAlgEquiv.instInhabitedStarAlgEquiv {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] : Inhabited (A ≃⋆ₐ[R] A)

@[simp]

theorem StarAlgEquiv.coe_refl {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] : ↑StarAlgEquiv.refl = id

def StarAlgEquiv.symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : B ≃⋆ₐ[R] A

Star algebra equivalences are symmetric.

def StarAlgEquiv.Simps.apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : A → B

See Note [custom simps projection]

def StarAlgEquiv.Simps.symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : B → A

See Note [custom simps projection]

@[simp]

theorem StarAlgEquiv.invFun_eq_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] {e : A ≃⋆ₐ[R] B} : EquivLike.inv e = ↑(StarAlgEquiv.symm e)

@[simp]

theorem StarAlgEquiv.symm_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : StarAlgEquiv.symm (StarAlgEquiv.symm e) = e

theorem StarAlgEquiv.symm_bijective {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] : Function.Bijective StarAlgEquiv.symm

@[simp]

theorem StarAlgEquiv.mk_coe' {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (f : B → A) (h₁ : Function.LeftInverse (↑e) f) (h₂ : Function.RightInverse (↑e) f) (h₃ : ∀ (x y : B), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : B), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) (h₅ : ∀ (a : B), Equiv.toFun { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv (star a) = star (Equiv.toFun { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv a)) (h₆ : ∀ (r : R) (a : B), Equiv.toFun { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv (r • a) = r • Equiv.toFun { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv a) : { toRingEquiv := { toEquiv := { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ } = StarAlgEquiv.symm e

@[simp]

theorem StarAlgEquiv.symm_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (f : A → B) (f' : B → A) (h₁ : Function.LeftInverse f' f) (h₂ : Function.RightInverse f' f) (h₃ : ∀ (x y : A), Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : A), Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ } y) (h₅ : ∀ (a : A), Equiv.toFun { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv (star a) = star (Equiv.toFun { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv a)) (h₆ : ∀ (r : R) (a : A), Equiv.toFun { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv (r • a) = r • Equiv.toFun { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv a) : StarAlgEquiv.symm { toRingEquiv := { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ } = let src := StarAlgEquiv.symm { toRingEquiv := { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }, map_star' := h₅, map_smul' := h₆ }; { toRingEquiv := { toEquiv := { toFun := f', invFun := f, left_inv := (_ : Function.LeftInverse src.invFun src.toFun), right_inv := (_ : Function.RightInverse src.invFun src.toFun) }, map_mul' := (_ : ∀ (x y : B), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y), map_add' := (_ : ∀ (x y : B), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }, map_star' := (_ : ∀ (a : B), Equiv.toFun src.toEquiv (star a) = star (Equiv.toFun src.toEquiv a)), map_smul' := (_ : ∀ (r : R) (a : B), Equiv.toFun src.toEquiv (r • a) = r • Equiv.toFun src.toEquiv a) }

@[simp]

theorem StarAlgEquiv.refl_symm {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] : StarAlgEquiv.symm StarAlgEquiv.refl = StarAlgEquiv.refl

theorem StarAlgEquiv.to_ringEquiv_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) : RingEquiv.symm ↑f = ↑(StarAlgEquiv.symm f)

@[simp]

theorem StarAlgEquiv.symm_to_ringEquiv {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : ↑(StarAlgEquiv.symm e) = RingEquiv.symm ↑e

def StarAlgEquiv.trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) : A ≃⋆ₐ[R] C

Star algebra equivalences are transitive.

@[simp]

theorem StarAlgEquiv.apply_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (x : B) : ↑e (↑(StarAlgEquiv.symm e) x) = x

@[simp]

theorem StarAlgEquiv.symm_apply_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) (x : A) : ↑(StarAlgEquiv.symm e) (↑e x) = x

@[simp]

theorem StarAlgEquiv.symm_trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : C) : ↑(StarAlgEquiv.symm (StarAlgEquiv.trans e₁ e₂)) x = ↑(StarAlgEquiv.symm e₁) (↑(StarAlgEquiv.symm e₂) x)

@[simp]

theorem StarAlgEquiv.coe_trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) : ↑(StarAlgEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

@[simp]

theorem StarAlgEquiv.trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] [Add C] [Mul C] [SMul R C] [Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : A) : ↑(StarAlgEquiv.trans e₁ e₂) x = ↑e₂ (↑e₁ x)

theorem StarAlgEquiv.leftInverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : Function.LeftInverse ↑(StarAlgEquiv.symm e) ↑e

theorem StarAlgEquiv.rightInverse_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [Add A] [Add B] [Mul A] [Mul B] [SMul R A] [SMul R B] [Star A] [Star B] (e : A ≃⋆ₐ[R] B) : Function.RightInverse ↑(StarAlgEquiv.symm e) ↑e

@[simp]

theorem StarAlgEquiv.ofStarAlgHom_symm_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] [NonUnitalStarAlgHomClass G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ↑g (↑f x) = x) (h₂ : ∀ (x : B), ↑f (↑g x) = x) (a : B) : ↑(StarAlgEquiv.symm (StarAlgEquiv.ofStarAlgHom f g h₁ h₂)) a = ↑g a

@[simp]

theorem StarAlgEquiv.ofStarAlgHom_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] [NonUnitalStarAlgHomClass G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ↑g (↑f x) = x) (h₂ : ∀ (x : B), ↑f (↑g x) = x) (a : A) : ↑(StarAlgEquiv.ofStarAlgHom f g h₁ h₂) a = ↑f a

def StarAlgEquiv.ofStarAlgHom {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] [NonUnitalStarAlgHomClass G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ↑g (↑f x) = x) (h₂ : ∀ (x : B), ↑f (↑g x) = x) : A ≃⋆ₐ[R] B

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

noncomputable def StarAlgEquiv.ofBijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] (f : F) (hf : Function.Bijective ↑f) : A ≃⋆ₐ[R] B

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

@[simp]

theorem StarAlgEquiv.coe_ofBijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Bijective ↑f) : ↑(StarAlgEquiv.ofBijective f hf) = ↑f

theorem StarAlgEquiv.ofBijective_apply {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] [hF : NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Bijective ↑f) (a : A) : ↑(StarAlgEquiv.ofBijective f hf) a = ↑f a