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)

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.

• toFun : A → B
• map_smul' : ∀ (m : R) (x : A), self.toMulActionHom.toFun (m • x) = m • self.toMulActionHom.toFun x
• map_zero' : self.toMulActionHom.toFun 0 = 0
• map_add' : ∀ (x y : A), self.toMulActionHom.toFun (x + y) = self.toMulActionHom.toFun x + self.toMulActionHom.toFun y
• map_mul' : ∀ (x y : A), self.toMulActionHom.toFun (x * y) = self.toMulActionHom.toFun x * self.toMulActionHom.toFun y
• map_star' : ∀ (a : A), self.toMulActionHom.toFun (star a) = star (self.toMulActionHom.toFun a)

  By definition, a non-unital ⋆-algebra homomorphism preserves the star operation.

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.

Equations

• «term_→⋆ₙₐ_» = Lean.ParserDescr.trailingNode `term_→⋆ₙₐ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →⋆ₙₐ ") (Lean.ParserDescr.cat `term 25))

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.

Equations

• One or more equations did not get rendered due to their size.

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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] extends StarHomClass : Prop

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] [FunLike F A B] [NonUnitalAlgHomClass F R A 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.

Equations

• ↑f = let src := ↑f; { toNonUnitalAlgHom := src, map_star' := (_ : ∀ (r : A), f (star r) = star (f r)) }

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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] : CoeTC F (A →⋆ₙₐ[R] B)

Equations

• NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHom = { coe := NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom }

instance NonUnitalStarAlgHom.instFunLikeNonUnitalStarAlgHom {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] : FunLike (A →⋆ₙₐ[R] B) A B

Equations

• One or more equations did not get rendered due to their size.

instance NonUnitalStarAlgHom.instNonUnitalAlgHomClassNonUnitalStarAlgHomInstFunLikeNonUnitalStarAlgHom {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] : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B

Equations

• (_ : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B) = (_ : NonUnitalAlgHomClass (A →⋆ₙₐ[R] B) R A B)

instance NonUnitalStarAlgHom.instNonUnitalStarAlgHomClassNonUnitalStarAlgHomInstFunLikeNonUnitalStarAlgHomInstNonUnitalAlgHomClassNonUnitalStarAlgHomInstFunLikeNonUnitalStarAlgHom {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

Equations

• (_ : NonUnitalStarAlgHomClass (A →⋆ₙₐ[R] B) R A 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]

Equations

• NonUnitalStarAlgHom.Simps.apply f = ⇑f

@[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} [FunLike F A B] [NonUnitalAlgHomClass F R A B] [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.

Equations

• One or more equations did not get rendered due to their size.

@[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₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := f, map_smul' := h₁ }.toFun (x + y) = { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun (x * y) = { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun x * { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun y) (h₅ : ∀ (a : A), { toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom.toFun (star a) = star ({ toDistribMulActionHom := { toMulActionHom := { toFun := f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom.toFun 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), f.toMulActionHom.toFun (star a) = star (f.toMulActionHom.toFun 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₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : A), { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y) (h₄ : ∀ (x y : A), { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun (x * y) = { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun x * { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }.toMulActionHom.toFun y) (h₅ : ∀ (a : A), { toDistribMulActionHom := { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom.toFun (star a) = star ({ toDistribMulActionHom := { toMulActionHom := { toFun := ⇑f, map_smul' := h₁ }, map_zero' := h₂, map_add' := h₃ }, map_mul' := h₄ }.toDistribMulActionHom.toMulActionHom.toFun 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.

Equations

• NonUnitalStarAlgHom.id R A = let src := 1; { toNonUnitalAlgHom := src, map_star' := (_ : ∀ (x : A), 1.toMulActionHom.toFun (star x) = 1.toMulActionHom.toFun (star x)) }

@[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.

Equations

• NonUnitalStarAlgHom.comp f g = let src := NonUnitalAlgHom.comp f.toNonUnitalAlgHom g.toNonUnitalAlgHom; { toNonUnitalAlgHom := src, map_star' := (_ : ∀ (a : A), f (g (star a)) = star (f (g a))) }

@[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)

Equations

• One or more equations did not get rendered due to their size.

@[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)

Equations

• One or more equations did not get rendered due to their size.

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)

Equations

• NonUnitalStarAlgHom.instInhabitedNonUnitalStarAlgHomToStarToInvolutiveStarToAddMonoidToAddCommMonoidToStarToInvolutiveStarToAddMonoidToAddCommMonoid = { default := 0 }

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

Equations

• One or more equations did not get rendered due to their size.

@[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)

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.

• toFun : A → B
• map_one' : (↑↑↑self.toAlgHom).toFun 1 = 1
• map_mul' : ∀ (x y : A), (↑↑↑self.toAlgHom).toFun (x * y) = (↑↑↑self.toAlgHom).toFun x * (↑↑↑self.toAlgHom).toFun y
• map_zero' : (↑↑↑self.toAlgHom).toFun 0 = 0
• map_add' : ∀ (x y : A), (↑↑↑self.toAlgHom).toFun (x + y) = (↑↑↑self.toAlgHom).toFun x + (↑↑↑self.toAlgHom).toFun y
• commutes' : ∀ (r : R), (↑↑↑self.toAlgHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
• map_star' : ∀ (x : A), (↑↑↑self.toAlgHom).toFun (star x) = star ((↑↑↑self.toAlgHom).toFun x)

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

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.

Equations

• «term_→⋆ₐ_» = Lean.ParserDescr.trailingNode `term_→⋆ₐ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →⋆ₐ ") (Lean.ParserDescr.cat `term 25))

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.

Equations

• One or more equations did not get rendered due to their size.

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] [FunLike F A B] [AlgHomClass F R A B] extends StarHomClass : Prop

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) : ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] [inst_1 : Star A] {x_2 : Semiring B} [inst_2 : Algebra R B] [inst_3 : Star B] [inst_4 : FunLike F A B] [inst_5 : AlgHomClass F R A B] [inst_6 : StarAlgHomClass F R A B], NonUnitalStarAlgHomClass F R A B

Equations

• (_ : NonUnitalStarAlgHomClass 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] [FunLike F A B] [AlgHomClass F R A B] [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.

Equations

• ↑f = let src := ↑f; { toAlgHom := src, map_star' := (_ : ∀ (r : A), f (star r) = star (f r)) }

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] [FunLike F A B] [AlgHomClass F R A B] [StarAlgHomClass F R A B] : CoeTC F (A →⋆ₐ[R] B)

Equations

• StarAlgHomClass.instCoeTCStarAlgHom F R A B = { coe := StarAlgHomClass.toStarAlgHom }

instance StarAlgHom.instFunLikeStarAlgHom {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] : FunLike (A →⋆ₐ[R] B) A B

Equations

• One or more equations did not get rendered due to their size.

instance StarAlgHom.instAlgHomClassStarAlgHomInstFunLikeStarAlgHom {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] : AlgHomClass (A →⋆ₐ[R] B) R A B

Equations

• (_ : AlgHomClass (A →⋆ₐ[R] B) R A B) = (_ : AlgHomClass (A →⋆ₐ[R] B) R A B)

instance StarAlgHom.instStarAlgHomClassStarAlgHomInstFunLikeStarAlgHomInstAlgHomClassStarAlgHomInstFunLikeStarAlgHom {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

Equations

• (_ : StarAlgHomClass (A →⋆ₐ[R] B) R A 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} [FunLike F A B] [AlgHomClass F R A B] [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]

Equations

• StarAlgHom.Simps.apply f = ⇑f

@[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.

Equations

• One or more equations did not get rendered due to their size.

@[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), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }).toFun (x + y) = (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }).toFun x + (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ (x : A), (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }).toFun (star x) = star ((↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }).toFun 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), (↑↑↑f).toFun (star x) = star ((↑↑↑f).toFun 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), { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x y : A), (↑{ toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }).toFun (x + y) = (↑{ toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }).toFun x + (↑{ toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }).toFun y) (h₅ : ∀ (r : R), (↑↑{ toMonoidHom := { toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r) (h₆ : ∀ (x : A), (↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }).toFun (star x) = star ((↑↑↑{ toRingHom := { toMonoidHom := { toOneHom := { toFun := ⇑f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ }, commutes' := h₅ }).toFun 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.

Equations

• StarAlgHom.id R A = let src := AlgHom.id R A; { toAlgHom := src, map_star' := (_ : ∀ (x : A), (↑↑↑(AlgHom.id R A)).toFun (star x) = (↑↑↑(AlgHom.id R A)).toFun (star x)) }

@[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

@[simp]

theorem StarAlgHom.ofId_apply (R : Type u_7) (A : Type u_8) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] (a : R) : (StarAlgHom.ofId R A) a = (algebraMap R A) a

def StarAlgHom.ofId (R : Type u_7) (A : Type u_8) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] : R →⋆ₐ[R] A

algebraMap R A as a StarAlgHom when A is a star algebra over R.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• StarAlgHom.instInhabitedStarAlgHom = { default := StarAlgHom.id 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.

Equations

• StarAlgHom.comp f g = let src := AlgHom.comp f.toAlgHom g.toAlgHom; { toAlgHom := src, map_star' := (_ : ∀ (a : A), f (g (star a)) = star (f (g a))) }

@[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)

Equations

• StarAlgHom.instMonoidStarAlgHom = Monoid.mk (_ : ∀ (f : A →⋆ₐ[R] A), StarAlgHom.comp (StarAlgHom.id R A) f = f) (_ : ∀ (f : A →⋆ₐ[R] A), StarAlgHom.comp f (StarAlgHom.id R A) = f) npowRec

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.1

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

Equations

• One or more equations did not get rendered due to their size.

@[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.2

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• One or more equations did not get rendered due to their size.

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_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.1 f.2

@[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)

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• NonUnitalStarAlgHom.inl R A B = NonUnitalStarAlgHom.prod 1 0

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.

Equations

• NonUnitalStarAlgHom.inr R A B = NonUnitalStarAlgHom.prod 0 1

@[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 : A) => (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.1

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

Equations

• StarAlgHom.fst R A B = let src := AlgHom.fst R A B; { toAlgHom := src, map_star' := (_ : ∀ (x : A × B), (↑↑↑(AlgHom.fst R A B)).toFun (star x) = (↑↑↑(AlgHom.fst R A B)).toFun (star x)) }

@[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.2

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.

Equations

• StarAlgHom.snd R A B = let src := AlgHom.snd R A B; { toAlgHom := src, map_star' := (_ : ∀ (x : A × B), (↑↑↑(AlgHom.snd R A B)).toFun (star x) = (↑↑↑(AlgHom.snd R A B)).toFun (star x)) }

@[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.

Equations

• StarAlgHom.prod f g = let src := AlgHom.prod f.toAlgHom g.toAlgHom; { toAlgHom := src, map_star' := (_ : ∀ (x : A), (f (star x), g (star x)) = (star (f x), star (g x))) }

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_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.1 f.2

@[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)

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.

Equations

• One or more equations did not get rendered due to their size.

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)

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.

• toFun : A → B
• invFun : B → A
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_mul' : ∀ (x y : A), self.toEquiv.toFun (x * y) = self.toEquiv.toFun x * self.toEquiv.toFun y
• map_add' : ∀ (x y : A), self.toEquiv.toFun (x + y) = self.toEquiv.toFun x + self.toEquiv.toFun y
• map_star' : ∀ (a : A), self.toEquiv.toFun (star a) = star (self.toEquiv.toFun a)

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

• map_smul' : ∀ (r : R) (a : A), self.toEquiv.toFun (r • a) = r • self.toEquiv.toFun a

  By definition, a ⋆-algebra equivalence commutes with the action of scalars.

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.

Equations

• «term_≃⋆ₐ_» = Lean.ParserDescr.trailingNode `term_≃⋆ₐ_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃⋆ₐ ") (Lean.ParserDescr.cat `term 25))

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.

Equations

• One or more equations did not get rendered due to their size.

class NonUnitalAlgEquivClass (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] [Add B] [Mul B] [SMul R B] [EquivLike F A B] extends RingEquivClass , SMulHomClass : Prop

The class that directly extends RingEquivClass and SMulHomClass.

Mostly an implementation detail for StarAlgEquivClass.

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] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] : Prop

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.

• map_star : ∀ (f : F) (a : A), f (star a) = star (f a)

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

instance StarAlgEquivClass.instStarHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} : ∀ {x : Add A} {x_1 : Mul A} [inst : SMul R A] {x_2 : Star A} {x_3 : Add B} {x_4 : Mul B} [inst_1 : SMul R B] {x_5 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [hF : StarAlgEquivClass F R A B], StarHomClass F A B

Equations

• (_ : StarHomClass F A B) = (_ : StarHomClass F A B)

instance StarAlgEquivClass.instNonUnitalAlgHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} : ∀ {x : Monoid R} {x_1 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_2 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction R B] [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B], NonUnitalAlgHomClass F R A B

Equations

• (_ : NonUnitalAlgHomClass F R A B) = (_ : NonUnitalAlgHomClass F R A B)

instance StarAlgEquivClass.instNonUnitalStarAlgHomClassToFunLikeInstNonUnitalAlgHomClassToFunLike {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} : ∀ {x : Monoid R} {x_1 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A] {x_2 : Star A} {x_3 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction R B] {x_4 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [inst_4 : StarAlgEquivClass F R A B], NonUnitalStarAlgHomClass F R A B

Equations

• (_ : NonUnitalStarAlgHomClass F R A B) = (_ : NonUnitalStarAlgHomClass F R A B)

instance StarAlgEquivClass.instAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) : ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] {x_2 : Semiring B} [inst_1 : Algebra R B] [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B], AlgEquivClass F R A B

Equations

• (_ : AlgEquivClass F R A B) = (_ : AlgEquivClass F R A B)

instance StarAlgEquivClass.instStarAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) : ∀ {x : CommSemiring R} {x_1 : Semiring A} [inst : Algebra R A] {x_2 : Star A} {x_3 : Semiring B} [inst_1 : Algebra R B] {x_4 : Star B} [inst_2 : EquivLike F A B] [inst_3 : NonUnitalAlgEquivClass F R A B] [inst_4 : StarAlgEquivClass F R A B], StarAlgHomClass F R A B

Equations

• (_ : StarAlgHomClass F R A B) = (_ : StarAlgHomClass F R A B)

instance StarAlgEquiv.instEquivLikeStarAlgEquiv {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] : EquivLike (A ≃⋆ₐ[R] B) A B

Equations

• One or more equations did not get rendered due to their size.

instance StarAlgEquiv.instNonUnitalAlgEquivClassStarAlgEquivInstEquivLikeStarAlgEquiv {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] : NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B

Equations

• (_ : NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B) = (_ : NonUnitalAlgEquivClass (A ≃⋆ₐ[R] B) R A B)

instance StarAlgEquiv.instStarAlgEquivClassStarAlgEquivInstEquivLikeStarAlgEquivInstNonUnitalAlgEquivClassStarAlgEquivInstEquivLikeStarAlgEquiv {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

Equations

• (_ : StarAlgEquivClass (A ≃⋆ₐ[R] B) R A B) = (_ : StarAlgEquivClass (A ≃⋆ₐ[R] B) R A B)

instance StarAlgEquiv.instFunLikeStarAlgEquiv {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] : FunLike (A ≃⋆ₐ[R] B) A B

Helper instance for cases where the inference via EquivLike is too hard.

Equations

• StarAlgEquiv.instFunLikeStarAlgEquiv = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, coe_injective' := (_ : Function.Injective fun (f : A ≃⋆ₐ[R] B) => ⇑f) }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• StarAlgEquiv.instInhabitedStarAlgEquiv = { default := StarAlgEquiv.refl }

@[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.

Equations

• One or more equations did not get rendered due to their size.

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]

Equations

• StarAlgEquiv.Simps.apply e = ⇑e

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]

Equations

• StarAlgEquiv.Simps.symm_apply e = ⇑(StarAlgEquiv.symm e)

@[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), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : B), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (a : B), { toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun (star a) = star ({ toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun a)) (h₆ : ∀ (r : R) (a : B), { toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun (r • a) = r • { toEquiv := { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun 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), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y) (h₅ : ∀ (a : A), { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun (star a) = star ({ toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun a)) (h₆ : ∀ (r : R) (a : A), { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun (r • a) = r • { toEquiv := { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }.toEquiv.toFun 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), src.toEquiv.toFun (x * y) = src.toEquiv.toFun x * src.toEquiv.toFun y), map_add' := (_ : ∀ (x y : B), src.toEquiv.toFun (x + y) = src.toEquiv.toFun x + src.toEquiv.toFun y) }, map_star' := (_ : ∀ (a : B), src.toEquiv.toFun (star a) = star (src.toEquiv.toFun a)), map_smul' := (_ : ∀ (r : R) (a : B), src.toEquiv.toFun (r • a) = r • src.toEquiv.toFun 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.

Equations

• One or more equations did not get rendered due to their size.

@[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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G 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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G 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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] [FunLike G 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.

Equations

• One or more equations did not get rendered due to their size.

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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [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.

Equations

• One or more equations did not get rendered due to their size.

@[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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [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] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [NonUnitalStarAlgHomClass F R A B] {f : F} (hf : Function.Bijective ⇑f) (a : A) : (StarAlgEquiv.ofBijective f hf) a = f a