Documentation

Mathlib.Algebra.Star.StarAlgHom

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 A →ₙₐ[R] B :

Type (max u_2 u_3)

A non-unital ⋆-algebra homomorphism is a non-unital algebra homomorphism between non-unital R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

toFun : A → B
map_smul' (m : R) (x : A) : self.toFun (m • x) = (MonoidHom.id R) m • self.toFun x
map_zero' : self.toFun 0 = 0
map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
map_mul' (x y : A) : self.toFun (x * y) = self.toFun x * self.toFun y
map_star' (a : A) : self.toFun (star a) = star (self.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.

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] [StarHomClass F A B] (f : F) :

A →⋆ₙₐ[R] B

Turn an element of a type F satisfying NonUnitalAlgHomClass F R A B and StarHomClass F A B into an actual NonUnitalStarAlgHom. This is declared as the default coercion from F to A →⋆ₙₐ[R] B.

Equations

↑f = { toNonUnitalAlgHom := NonUnitalAlgHomClass.toNonUnitalAlgHom f, map_star' := ⋯ }

instance NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHomOfStarHomClass {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] [StarHomClass F A B] :

CoeTC F (A →⋆ₙₐ[R] B)

Equations

NonUnitalStarAlgHomClass.instCoeTCNonUnitalStarAlgHomOfStarHomClass = { coe := NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom }

instance NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass {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] [StarHomClass F A B] :

NonUnitalStarRingHomClass F A B

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

NonUnitalStarAlgHom.instFunLike = { coe := fun (f : A →⋆ₙₐ[R] B) => f.toFun, coe_injective' := ⋯ }

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

instance NonUnitalStarAlgHom.instStarHomClass {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] :

StarHomClass (A →⋆ₙₐ[R] B) 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] [StarHomClass F 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 g : A →⋆ₙₐ[R] B} (h : ∀ (x : A), f x = g x) :

f = g

theorem NonUnitalStarAlgHom.ext_iff {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 g : A →⋆ₙₐ[R] B} :

f = g ↔ ∀ (x : A), f x = g x

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

f.copy f' h = { toFun := f', map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

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

⇑(f.copy 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) :

f.copy 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) = (MonoidHom.id R) 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), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) = { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x * { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y) (h₅ : ∀ (a : A), { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun (star a) = star ({ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ }.toFun a)) :

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

{ 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 = { toNonUnitalAlgHom := 1, map_star' := ⋯ }

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

f.comp g = { toNonUnitalAlgHom := f.comp g.toNonUnitalAlgHom, map_star' := ⋯ }

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

⇑(f.comp 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) :

(f.comp 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) :

(f.comp g).comp h = f.comp (g.comp 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.id R B).comp 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) :

f.comp (NonUnitalStarAlgHom.id R A) = f

instance NonUnitalStarAlgHom.instMonoid {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] :

Monoid (A →⋆ₙₐ[R] A)

Equations

NonUnitalStarAlgHom.instMonoid = { mul := NonUnitalStarAlgHom.comp, mul_assoc := ⋯, one := NonUnitalStarAlgHom.id R A, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

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

NonUnitalStarAlgHom.instZero = { zero := let __src := 0; { toNonUnitalAlgHom := __src, map_star' := ⋯ } }

instance NonUnitalStarAlgHom.instInhabited {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.instInhabited = { default := 0 }

instance NonUnitalStarAlgHom.instMonoidWithZero {R : Type u_1} {A : Type u_2} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [StarAddMonoid A] :

MonoidWithZero (A →⋆ₙₐ[R] A)

Equations

NonUnitalStarAlgHom.instMonoidWithZero = { toMonoid := inferInstanceAs (Monoid (A →⋆ₙₐ[R] A)), toZero := inferInstanceAs (Zero (A →⋆ₙₐ[R] A)), zero_mul := ⋯, mul_zero := ⋯ }

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

def NonUnitalStarAlgHom.restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) :

A →⋆ₙₐ[R] B

If a monoid R acts on another monoid S, then a non-unital star algebra homomorphism over S can be viewed as a non-unital star algebra homomorphism over R.

Equations

NonUnitalStarAlgHom.restrictScalars R f = { toNonUnitalAlgHom := NonUnitalAlgHom.restrictScalars R (NonUnitalAlgHomClass.toNonUnitalAlgHom f), map_star' := ⋯ }

@[simp]

theorem NonUnitalStarAlgHom.restrictScalars_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) (x : A) :

(restrictScalars R f) x = f x

theorem NonUnitalStarAlgHom.coe_restrictScalars (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) :

↑(restrictScalars R f) = ↑f

theorem NonUnitalStarAlgHom.coe_restrictScalars' (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] (f : A →⋆ₙₐ[S] B) :

⇑(restrictScalars R f) = ⇑f

theorem NonUnitalStarAlgHom.restrictScalars_injective (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [Monoid S] [Star A] [Star B] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [MulAction R S] [DistribMulAction S A] [DistribMulAction S B] [DistribMulAction R A] [DistribMulAction R B] [IsScalarTower R S A] [IsScalarTower R S B] :

Function.Injective (restrictScalars R)

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 A →ₐ[R] B :

Type (max u_2 u_3)

A ⋆-algebra homomorphism is an algebra homomorphism between R-algebras A and B equipped with a star operation, and this homomorphism is also star-preserving.

toFun : A → B
map_one' : (↑↑self.toRingHom).toFun 1 = 1
map_mul' (x y : A) : (↑↑self.toRingHom).toFun (x * y) = (↑↑self.toRingHom).toFun x * (↑↑self.toRingHom).toFun y
map_zero' : (↑↑self.toRingHom).toFun 0 = 0
map_add' (x y : A) : (↑↑self.toRingHom).toFun (x + y) = (↑↑self.toRingHom).toFun x + (↑↑self.toRingHom).toFun y
commutes' (r : R) : (↑↑self.toRingHom).toFun ((algebraMap R A) r) = (algebraMap R B) r
map_star' (x : A) : (↑↑self.toRingHom).toFun (star x) = star ((↑↑self.toRingHom).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.

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] [StarHomClass F A B] (f : F) :

A →⋆ₐ[R] B

Turn an element of a type F satisfying AlgHomClass F R A B and StarHomClass F A B into an actual StarAlgHom. This is declared as the default coercion from F to A →⋆ₐ[R] B.

Equations

↑f = { toAlgHom := ↑f, map_star' := ⋯ }

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] [StarHomClass F A B] :

CoeTC F (A →⋆ₐ[R] B)

Equations

StarAlgHomClass.instCoeTCStarAlgHom = { coe := StarAlgHomClass.toStarAlgHom }

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

StarAlgHom.instFunLike = { coe := fun (f : A →⋆ₐ[R] B) => (↑↑f.toRingHom).toFun, coe_injective' := ⋯ }

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

instance StarAlgHom.instStarHomClass {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] :

StarHomClass (A →⋆ₐ[R] B) 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] [StarHomClass F 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 g : A →⋆ₐ[R] B} (h : ∀ (x : A), f x = g x) :

f = g

theorem StarAlgHom.ext_iff {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 g : A →⋆ₐ[R] B} :

f = g ↔ ∀ (x : A), f x = g x

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

f.copy f' h = { toFun := f', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

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

⇑(f.copy 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) :

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

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

{ 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 = { toAlgHom := AlgHom.id R A, map_star' := ⋯ }

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

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

StarAlgHom.ofId R A = { toFun := ⇑(algebraMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

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

(ofId R A) a = (algebraMap R A) a

instance StarAlgHom.instInhabited {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :

Inhabited (A →⋆ₐ[R] A)

Equations

StarAlgHom.instInhabited = { 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

f.comp g = { toAlgHom := f.comp g.toAlgHom, map_star' := ⋯ }

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

⇑(f.comp 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) :

(f.comp 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) :

(f.comp g).comp h = f.comp (g.comp 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.id R B).comp 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) :

f.comp (StarAlgHom.id R A) = f

instance StarAlgHom.instMonoid {R : Type u_2} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] :

Monoid (A →⋆ₐ[R] A)

Equations

StarAlgHom.instMonoid = { mul := StarAlgHom.comp, mul_assoc := ⋯, one := StarAlgHom.id R A, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

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

f.toNonUnitalStarAlgHom = { toFun := (↑↑f.toRingHom).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

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

⇑f.toNonUnitalStarAlgHom = ⇑f

Operations on the product type #

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

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

NonUnitalStarAlgHom.fst R A B = { toNonUnitalAlgHom := NonUnitalAlgHom.fst R A B, map_star' := ⋯ }

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

(fst R A B) self = self.1

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

NonUnitalStarAlgHom.snd R A B = { toNonUnitalAlgHom := NonUnitalAlgHom.snd R A B, map_star' := ⋯ }

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

(snd R A B) self = self.2

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

f.prod g = { toNonUnitalAlgHom := f.prod g.toNonUnitalAlgHom, map_star' := ⋯ }

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

(f.prod g) i = (f i, g i)

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) :

⇑(f.prod 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) :

(fst R B C).comp (f.prod 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) :

(snd R B C).comp (f.prod 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] :

(fst R A B).prod (snd R A B) = 1

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.

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

prodEquiv f = f.1.prod 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) :

prodEquiv.symm f = ((fst R B C).comp f, (snd R B C).comp f)

def Pi.evalNonUnitalStarAlgHom {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [Monoid R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → DistribMulAction R (A i)] [(i : ι) → Star (A i)] :

((i : ι) → A i) →⋆ₙₐ[R] A j

Function.eval as a NonUnitalStarAlgHom.

Equations

Pi.evalNonUnitalStarAlgHom R A j = { toFun := (Pi.evalMulHom A j).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem Pi.evalNonUnitalStarAlgHom_apply {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [Monoid R] [(i : ι) → NonUnitalNonAssocSemiring (A i)] [(i : ι) → DistribMulAction R (A i)] [(i : ι) → Star (A i)] (a✝ : (i : ι) → A i) :

(evalNonUnitalStarAlgHom R A j) a✝ = (evalMulHom A j).toFun a✝

def Pi.evalStarAlgHom {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → Star (A i)] :

((i : ι) → A i) →⋆ₐ[R] A j

Function.eval as a StarAlgHom.

Equations

Pi.evalStarAlgHom R A j = { toFun := (Pi.evalNonUnitalStarAlgHom R A j).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem Pi.evalStarAlgHom_apply {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) (j : ι) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] [(i : ι) → Star (A i)] (a✝ : (i : ι) → A i) :

(evalStarAlgHom R A j) a✝ = (evalNonUnitalStarAlgHom R A j).toFun a✝

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] :

⇑(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) :

(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] :

⇑(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) :

(inr R A B) x = (0, x)

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 = { toAlgHom := AlgHom.fst R A B, map_star' := ⋯ }

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

(fst R A B) self = self.1

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 = { toAlgHom := AlgHom.snd R A B, map_star' := ⋯ }

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

(snd R A B) self = self.2

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

f.prod g = { toAlgHom := f.prod g.toAlgHom, map_star' := ⋯ }

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

(f.prod g) x = (f x, 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) :

⇑(f.prod 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) :

(fst R B C).comp (f.prod 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) :

(snd R B C).comp (f.prod 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] :

(fst R A B).prod (snd R A B) = 1

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.

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

prodEquiv f = f.1.prod 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) :

prodEquiv.symm f = ((fst R B C).comp f, (snd R B C).comp f)

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 A ≃+* B :

Type (max u_2 u_3)

A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure. Currently, 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.toFun (x * y) = self.toFun x * self.toFun y
map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y
map_star' (a : A) : self.toFun (star a) = star (self.toFun a)
By definition, a ⋆-algebra equivalence preserves the star operation.
map_smul' (r : R) (a : A) : self.toFun (r • a) = r • self.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 F A B, MulActionSemiHomClass F id A B :

The class that directly extends RingEquivClass and SMulHomClass.

Mostly an implementation detail for StarAlgEquivClass.

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_smulₛₗ (f : F) (c : R) (x : A) : f (c • x) = id c • f x

Instances

@[instance 100]

instance StarAlgEquivClass.instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :

NonUnitalAlgHomClass F R A B

@[instance 100]

instance StarAlgEquivClass.instAlgHomClass (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] :

AlgEquivClass F R A B

def StarAlgEquivClass.toStarAlgEquiv {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] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] (f : F) :

A ≃⋆ₐ[R] B

Turn an element of a type F satisfying AlgEquivClass F R A B and StarHomClass F A B into an actual StarAlgEquiv. This is declared as the default coercion from F to A ≃⋆ₐ[R] B.

Equations

↑f = { toRingEquiv := ↑f, map_star' := ⋯, map_smul' := ⋯ }

instance StarAlgEquivClass.instCoeHead {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] [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] :

CoeHead F (A ≃⋆ₐ[R] B)

Any type satisfying AlgEquivClass and StarHomClass can be cast into StarAlgEquiv via StarAlgEquivClass.toStarAlgEquiv.

Equations

StarAlgEquivClass.instCoeHead = { coe := StarAlgEquivClass.toStarAlgEquiv }

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

StarAlgEquiv.instEquivLike = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, inv := fun (f : A ≃⋆ₐ[R] B) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

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

instance StarAlgEquiv.instStarHomClass {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] :

StarHomClass (A ≃⋆ₐ[R] B) A B

instance StarAlgEquiv.instFunLike {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.instFunLike = { coe := fun (f : A ≃⋆ₐ[R] B) => f.toFun, coe_injective' := ⋯ }

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

The identity map is a star algebra isomorphism.

Equations

StarAlgEquiv.refl = { toRingEquiv := RingEquiv.refl A, map_star' := ⋯, map_smul' := ⋯ }

instance StarAlgEquiv.instInhabited {R : Type u_2} {A : Type u_3} [Add A] [Mul A] [SMul R A] [Star A] :

Inhabited (A ≃⋆ₐ[R] A)

Equations

StarAlgEquiv.instInhabited = { 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] :

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

The inverse of a star algebra isomorphism is a star algebra isomorphism.

Equations

e.symm = { toRingEquiv := e.symm, map_star' := ⋯, map_smul' := ⋯ }

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 = ⇑e.symm

@[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 = ⇑e.symm

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

e.symm.symm = 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 symm

@[simp]

theorem StarAlgEquiv.coe_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] (e : A ≃+* B) (h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)) (h₂ : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a) :

⇑{ toRingEquiv := e, map_star' := h₁, map_smul' := h₂ } = ⇑e

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

{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ } = e

def StarAlgEquiv.symm_mk.aux {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), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r • a) = r • { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a) :

B ≃⋆ₐ[R] A

Auxiliary definition to avoid looping in dsimp with StarAlgEquiv.symm_mk.

Equations

StarAlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ h₆ = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ }.symm

@[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), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)) (h₆ : ∀ (r : R) (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r • a) = r • { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a) :

{ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ }.symm = let __src := symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ h₆; { toFun := f', invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

@[simp]

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

refl.symm = 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) :

(↑f).symm = ↑f.symm

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

↑e.symm = (↑e).symm

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

Transitivity of StarAlgEquiv.

Equations

e₁.trans e₂ = { toRingEquiv := e₁.trans e₂.toRingEquiv, map_star' := ⋯, map_smul' := ⋯ }

@[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 (e.symm 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) :

e.symm (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) :

(e₁.trans e₂).symm x = e₁.symm (e₂.symm 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) :

⇑(e₁.trans 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) :

(e₁.trans 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 ⇑e.symm ⇑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 ⇑e.symm ⇑e

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] [StarHomClass F 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

StarAlgEquiv.ofStarAlgHom f g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := h₁, right_inv := h₂, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

@[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] [StarHomClass F 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) :

(ofStarAlgHom f g h₁ h₂).symm 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] [StarHomClass F 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) :

(ofStarAlgHom f g h₁ h₂) a = f a

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] [StarHomClass F A B] (f : F) (hf : Function.Bijective ⇑f) :

A ≃⋆ₐ[R] B

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

Equations

StarAlgEquiv.ofBijective f hf = { toFun := ⇑f, invFun := (RingEquiv.ofBijective f hf).invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

@[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] [StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f) :

⇑(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] [StarHomClass F A B] {f : F} (hf : Function.Bijective ⇑f) (a : A) :

(ofBijective f hf) a = f a