algebra.star.star_alg_hom

source

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

Type (max u_2 u_3)

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

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

Instances for non_unital_star_alg_hom

non_unital_star_alg_hom.has_sizeof_inst
non_unital_star_alg_hom_class.non_unital_star_alg_hom.has_coe_t
non_unital_star_alg_hom.non_unital_star_alg_hom_class
non_unital_star_alg_hom.has_coe_to_fun
non_unital_star_alg_hom.monoid
non_unital_star_alg_hom.has_zero
non_unital_star_alg_hom.inhabited
non_unital_star_alg_hom.monoid_with_zero

source

def non_unital_star_alg_hom.to_non_unital_alg_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (self : A →⋆ₙₐ[R] B) :

A →ₙₐ[R] B

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

source

@[instance]

def non_unital_star_alg_hom_class.to_non_unital_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [has_star A] [has_star B] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] [self : non_unital_star_alg_hom_class F R A B] :

non_unital_alg_hom_class F R A B

source

@[nolint, instance]

def non_unital_star_alg_hom_class.to_star_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [has_star A] [has_star B] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] [self : non_unital_star_alg_hom_class F R A B] :

star_hom_class F A B

source

@[class]

structure non_unital_star_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [monoid R] [has_star A] [has_star B] [non_unital_non_assoc_semiring A] [non_unital_non_assoc_semiring B] [distrib_mul_action R A] [distrib_mul_action R B] :

Type (max u_1 u_3 u_4)

coe : F → Π (a : A), (λ (_x : A), B) a
coe_injective' : function.injective non_unital_star_alg_hom_class.coe
map_smul : ∀ (f : F) (c : R) (x : A), ⇑f (c • x) = c • ⇑f x
map_add : ∀ (f : F) (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y
map_zero : ∀ (f : F), ⇑f 0 = 0
map_mul : ∀ (f : F) (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y
map_star : ∀ (f : F) (r : A), ⇑f (has_star.star r) = has_star.star (⇑f r)

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

Instances of this typeclass

Instances of other typeclasses for non_unital_star_alg_hom_class

non_unital_star_alg_hom_class.has_sizeof_inst

source

@[protected, instance]

def non_unital_star_alg_hom_class.non_unital_star_alg_hom.has_coe_t {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_star_alg_hom_class F R A B] :

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

Equations

non_unital_star_alg_hom_class.non_unital_star_alg_hom.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}}

source

@[protected, instance]

def non_unital_star_alg_hom.non_unital_star_alg_hom_class {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :

non_unital_star_alg_hom_class (A →⋆ₙₐ[R] B) R A B

Equations

non_unital_star_alg_hom.non_unital_star_alg_hom_class = {coe := non_unital_star_alg_hom.to_fun _inst_7, coe_injective' := _, map_smul := _, map_add := _, map_zero := _, map_mul := _, map_star := _}

source

@[protected, instance]

def non_unital_star_alg_hom.has_coe_to_fun {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :

has_coe_to_fun (A →⋆ₙₐ[R] B) (λ (_x : A →⋆ₙₐ[R] B), A → B)

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

Equations

non_unital_star_alg_hom.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[protected, simp]

theorem non_unital_star_alg_hom.coe_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] {F : Type u_4} [non_unital_star_alg_hom_class F R A B] (f : F) :

⇑↑f = ⇑f

source

@[simp]

theorem non_unital_star_alg_hom.coe_to_non_unital_alg_hom {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] {f : A →⋆ₙₐ[R] B} :

⇑(f.to_non_unital_alg_hom) = ⇑f

source

@[ext]

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

f = g

source

@[protected]

def non_unital_star_alg_hom.copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

A →⋆ₙₐ[R] B

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

Equations

f.copy f' h = {to_fun := f', map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

theorem non_unital_star_alg_hom.coe_copy {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem non_unital_star_alg_hom.copy_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

f.copy f' h = f

source

@[simp]

theorem non_unital_star_alg_hom.coe_mk {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A → B) (h₁ : ∀ (m : R) (x : A), f (m • x) = m • f x) (h₂ : f 0 = 0) (h₃ : ∀ (x y : A), f (x + y) = f x + f y) (h₄ : ∀ (x y : A), f (x * y) = f x * f y) (h₅ : ∀ (a : A), f (has_star.star a) = has_star.star (f a)) :

⇑{to_fun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅} = f

source

@[simp]

theorem non_unital_star_alg_hom.mk_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) (h₁ : ∀ (m : R) (x : A), ⇑f (m • x) = m • ⇑f x) (h₂ : ⇑f 0 = 0) (h₃ : ∀ (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y) (h₄ : ∀ (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y) (h₅ : ∀ (a : A), ⇑f (has_star.star a) = has_star.star (⇑f a)) :

{to_fun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅} = f

source

@[protected]

def non_unital_star_alg_hom.id (R : Type u_1) (A : Type u_2) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] :

A →⋆ₙₐ[R] A

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

Equations

non_unital_star_alg_hom.id R A = {to_fun := 1.to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

theorem non_unital_star_alg_hom.coe_id (R : Type u_1) (A : Type u_2) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] :

⇑(non_unital_star_alg_hom.id R A) = id

source

def non_unital_star_alg_hom.comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) :

A →⋆ₙₐ[R] C

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

Equations

f.comp g = {to_fun := (f.to_non_unital_alg_hom.comp g.to_non_unital_alg_hom).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

theorem non_unital_star_alg_hom.coe_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem non_unital_star_alg_hom.comp_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : B →⋆ₙₐ[R] C) (g : A →⋆ₙₐ[R] B) (a : A) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

@[simp]

theorem non_unital_star_alg_hom.comp_assoc {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] [non_unital_non_assoc_semiring D] [distrib_mul_action R D] [has_star D] (f : C →⋆ₙₐ[R] D) (g : B →⋆ₙₐ[R] C) (h : A →⋆ₙₐ[R] B) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

theorem non_unital_star_alg_hom.id_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) :

(non_unital_star_alg_hom.id R B).comp f = f

source

@[simp]

theorem non_unital_star_alg_hom.comp_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (f : A →⋆ₙₐ[R] B) :

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

source

@[protected, instance]

def non_unital_star_alg_hom.monoid {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] :

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

Equations

non_unital_star_alg_hom.monoid = {mul := non_unital_star_alg_hom.comp _inst_4, mul_assoc := _, one := non_unital_star_alg_hom.id R A _inst_4, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (A →⋆ₙₐ[R] A)), npow_zero' := _, npow_succ' := _}

source

@[simp]

theorem non_unital_star_alg_hom.coe_one {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] :

⇑1 = id

source

theorem non_unital_star_alg_hom.one_apply {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] (a : A) :

⇑1 a = a

source

@[protected, instance]

def non_unital_star_alg_hom.has_zero {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

has_zero (A →⋆ₙₐ[R] B)

Equations

non_unital_star_alg_hom.has_zero = {zero := {to_fun := 0.to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}}

source

@[protected, instance]

def non_unital_star_alg_hom.inhabited {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

inhabited (A →⋆ₙₐ[R] B)

Equations

non_unital_star_alg_hom.inhabited = {default := 0}

source

@[protected, instance]

def non_unital_star_alg_hom.monoid_with_zero {R : Type u_1} {A : Type u_2} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] :

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

Equations

non_unital_star_alg_hom.monoid_with_zero = {mul := monoid.mul non_unital_star_alg_hom.monoid, mul_assoc := _, one := monoid.one non_unital_star_alg_hom.monoid, one_mul := _, mul_one := _, npow := monoid.npow non_unital_star_alg_hom.monoid, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}

source

@[simp]

theorem non_unital_star_alg_hom.coe_zero {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

⇑0 = 0

source

theorem non_unital_star_alg_hom.zero_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] (a : A) :

⇑0 a = 0

source

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

A →ₐ[R] B

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

source

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

Type (max u_2 u_3)

to_fun : A → B
map_one' : self.to_fun 1 = 1
map_mul' : ∀ (x y : A), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_zero' : self.to_fun 0 = 0
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
commutes' : ∀ (r : R), self.to_fun (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
map_star' : ∀ (x : A), self.to_fun (has_star.star x) = has_star.star (self.to_fun x)

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

Instances for star_alg_hom

star_alg_hom.has_sizeof_inst
star_alg_hom_class.star_alg_hom.has_coe_t
star_alg_hom.star_alg_hom_class
star_alg_hom.has_coe_to_fun
star_alg_hom.inhabited
star_alg_hom.monoid

source

@[nolint, instance]

def star_alg_hom_class.to_star_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [self : star_alg_hom_class F R A B] :

star_hom_class F A B

source

@[instance]

def star_alg_hom_class.to_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [self : star_alg_hom_class F R A B] :

alg_hom_class F R A B

source

@[class]

structure star_alg_hom_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

Type (max u_1 u_3 u_4)

coe : F → Π (a : A), (λ (_x : A), B) a
coe_injective' : function.injective star_alg_hom_class.coe
map_mul : ∀ (f : F) (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y
map_one : ∀ (f : F), ⇑f 1 = 1
map_add : ∀ (f : F) (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y
map_zero : ∀ (f : F), ⇑f 0 = 0
commutes : ∀ (f : F) (r : R), ⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r
map_star : ∀ (f : F) (r : A), ⇑f (has_star.star r) = has_star.star (⇑f r)

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

You should also extend this typeclass when you extend star_alg_hom.

Instances of this typeclass

Instances of other typeclasses for star_alg_hom_class

star_alg_hom_class.has_sizeof_inst

source

@[protected, instance]

def star_alg_hom_class.to_non_unital_star_alg_hom_class (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [hF : star_alg_hom_class F R A B] :

non_unital_star_alg_hom_class F R A B

Equations

star_alg_hom_class.to_non_unital_star_alg_hom_class F R A B = {coe := alg_hom_class.coe (star_alg_hom_class.to_alg_hom_class F R A B), coe_injective' := _, map_smul := _, map_add := _, map_zero := _, map_mul := _, map_star := _}

source

@[protected, instance]

def star_alg_hom_class.star_alg_hom.has_coe_t (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [hF : star_alg_hom_class F R A B] :

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

Equations

star_alg_hom_class.star_alg_hom.has_coe_t F R A B = {coe := λ (f : F), {to_fun := ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}}

source

@[protected, instance]

def star_alg_hom.star_alg_hom_class {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

star_alg_hom_class (A →⋆ₐ[R] B) R A B

Equations

star_alg_hom.star_alg_hom_class = {coe := λ (f : A →⋆ₐ[R] B), f.to_fun, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _, map_star := _}

source

@[protected, instance]

def star_alg_hom.has_coe_to_fun {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

has_coe_to_fun (A →⋆ₐ[R] B) (λ (_x : A →⋆ₐ[R] B), A → B)

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

Equations

star_alg_hom.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[protected, simp]

theorem star_alg_hom.coe_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] {F : Type u_1} [star_alg_hom_class F R A B] (f : F) :

⇑↑f = ⇑f

source

@[simp]

theorem star_alg_hom.coe_to_alg_hom {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] {f : A →⋆ₐ[R] B} :

⇑(f.to_alg_hom) = ⇑f

source

@[ext]

theorem star_alg_hom.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] {f g : A →⋆ₐ[R] B} (h : ∀ (x : A), ⇑f x = ⇑g x) :

f = g

source

@[protected]

def star_alg_hom.copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

A →⋆ₐ[R] B

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

Equations

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

source

@[simp]

theorem star_alg_hom.coe_copy {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem star_alg_hom.copy_eq {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (f' : A → B) (h : f' = ⇑f) :

f.copy f' h = f

source

@[simp]

theorem star_alg_hom.coe_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A → B) (h₁ : f 1 = 1) (h₂ : ∀ (x y : A), f (x * y) = f x * f y) (h₃ : f 0 = 0) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (r : R), f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r) (h₆ : ∀ (x : A), f (has_star.star x) = has_star.star (f x)) :

⇑{to_fun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆} = f

source

@[simp]

theorem star_alg_hom.mk_coe {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) (h₁ : ⇑f 1 = 1) (h₂ : ∀ (x y : A), ⇑f (x * y) = ⇑f x * ⇑f y) (h₃ : ⇑f 0 = 0) (h₄ : ∀ (x y : A), ⇑f (x + y) = ⇑f x + ⇑f y) (h₅ : ∀ (r : R), ⇑f (⇑(algebra_map R A) r) = ⇑(algebra_map R B) r) (h₆ : ∀ (x : A), ⇑f (has_star.star x) = has_star.star (⇑f x)) :

{to_fun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆} = f

source

@[protected]

def star_alg_hom.id (R : Type u_2) (A : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] :

A →⋆ₐ[R] A

The identity as a star_alg_hom.

Equations

star_alg_hom.id R A = {to_fun := (alg_hom.id R A).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}

source

@[simp]

theorem star_alg_hom.coe_id (R : Type u_2) (A : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] :

⇑(star_alg_hom.id R A) = id

source

@[protected, instance]

def star_alg_hom.inhabited {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] :

inhabited (A →⋆ₐ[R] A)

Equations

star_alg_hom.inhabited = {default := star_alg_hom.id R A _inst_4}

source

def star_alg_hom.comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :

A →⋆ₐ[R] C

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

Equations

f.comp g = {to_fun := (f.to_alg_hom.comp g.to_alg_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}

source

@[simp]

theorem star_alg_hom.coe_comp {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) :

⇑(f.comp g) = ⇑f ∘ ⇑g

source

@[simp]

theorem star_alg_hom.comp_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : B →⋆ₐ[R] C) (g : A →⋆ₐ[R] B) (a : A) :

⇑(f.comp g) a = ⇑f (⇑g a)

source

@[simp]

theorem star_alg_hom.comp_assoc {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] [semiring D] [algebra R D] [has_star D] (f : C →⋆ₐ[R] D) (g : B →⋆ₐ[R] C) (h : A →⋆ₐ[R] B) :

(f.comp g).comp h = f.comp (g.comp h)

source

@[simp]

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

(star_alg_hom.id R B).comp f = f

source

@[simp]

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

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

source

@[protected, instance]

def star_alg_hom.monoid {R : Type u_2} {A : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] :

monoid (A →⋆ₐ[R] A)

Equations

star_alg_hom.monoid = {mul := star_alg_hom.comp _inst_4, mul_assoc := _, one := star_alg_hom.id R A _inst_4, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (A →⋆ₐ[R] A)), npow_zero' := _, npow_succ' := _}

source

def star_alg_hom.to_non_unital_star_alg_hom {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (f : A →⋆ₐ[R] B) :

A →⋆ₙₐ[R] B

A unital morphism of ⋆-algebras is a non_unital_star_alg_hom.

Equations

f.to_non_unital_star_alg_hom = {to_fun := f.to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

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

⇑(f.to_non_unital_star_alg_hom) = ⇑f

source

def non_unital_star_alg_hom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :

A × B →⋆ₙₐ[R] A

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

Equations

non_unital_star_alg_hom.fst R A B = {to_fun := (non_unital_alg_hom.fst R A B).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

theorem non_unital_star_alg_hom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (ᾰ : A × B) :

⇑(non_unital_star_alg_hom.fst R A B) ᾰ = (non_unital_alg_hom.fst R A B).to_fun ᾰ

source

@[simp]

theorem non_unital_star_alg_hom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] (ᾰ : A × B) :

⇑(non_unital_star_alg_hom.snd R A B) ᾰ = (non_unital_alg_hom.snd R A B).to_fun ᾰ

source

def non_unital_star_alg_hom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :

A × B →⋆ₙₐ[R] B

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

Equations

non_unital_star_alg_hom.snd R A B = {to_fun := (non_unital_alg_hom.snd R A B).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

def non_unital_star_alg_hom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) :

A →⋆ₙₐ[R] B × C

The pi.prod of two morphisms is a morphism.

Equations

f.prod g = {to_fun := (f.to_non_unital_alg_hom.prod g.to_non_unital_alg_hom).to_fun, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _, map_star' := _}

source

@[simp]

theorem non_unital_star_alg_hom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) (ᾰ : A) :

⇑(f.prod g) ᾰ = (f.to_non_unital_alg_hom.prod g.to_non_unital_alg_hom).to_fun ᾰ

source

theorem non_unital_star_alg_hom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

@[simp]

theorem non_unital_star_alg_hom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) :

(non_unital_star_alg_hom.fst R B C).comp (f.prod g) = f

source

@[simp]

theorem non_unital_star_alg_hom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) :

(non_unital_star_alg_hom.snd R B C).comp (f.prod g) = g

source

@[simp]

theorem non_unital_star_alg_hom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] :

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

source

@[simp]

theorem non_unital_star_alg_hom.prod_equiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : A →⋆ₙₐ[R] B × C) :

⇑(non_unital_star_alg_hom.prod_equiv.symm) f = ((non_unital_star_alg_hom.fst R B C).comp f, (non_unital_star_alg_hom.snd R B C).comp f)

source

def non_unital_star_alg_hom.prod_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] :

(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

non_unital_star_alg_hom.prod_equiv = {to_fun := λ (f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)), f.fst.prod f.snd, inv_fun := λ (f : A →⋆ₙₐ[R] B × C), ((non_unital_star_alg_hom.fst R B C).comp f, (non_unital_star_alg_hom.snd R B C).comp f), left_inv := _, right_inv := _}

source

@[simp]

theorem non_unital_star_alg_hom.prod_equiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [non_unital_non_assoc_semiring C] [distrib_mul_action R C] [has_star C] (f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)) :

⇑non_unital_star_alg_hom.prod_equiv f = f.fst.prod f.snd

source

def non_unital_star_alg_hom.inl (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

A →⋆ₙₐ[R] A × B

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

Equations

non_unital_star_alg_hom.inl R A B = 1.prod 0

source

def non_unital_star_alg_hom.inr (R : Type u_1) (A : Type u_2) (B : Type u_3) [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

B →⋆ₙₐ[R] A × B

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

Equations

non_unital_star_alg_hom.inr R A B = 0.prod 1

source

@[simp]

theorem non_unital_star_alg_hom.coe_inl {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

⇑(non_unital_star_alg_hom.inl R A B) = λ (x : A), (x, 0)

source

theorem non_unital_star_alg_hom.inl_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] (x : A) :

⇑(non_unital_star_alg_hom.inl R A B) x = (x, 0)

source

@[simp]

theorem non_unital_star_alg_hom.coe_inr {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] :

⇑(non_unital_star_alg_hom.inr R A B) = prod.mk 0

source

theorem non_unital_star_alg_hom.inr_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [star_add_monoid A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [star_add_monoid B] (x : B) :

⇑(non_unital_star_alg_hom.inr R A B) x = (0, x)

source

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

A × B →⋆ₐ[R] A

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

Equations

star_alg_hom.fst R A B = {to_fun := (alg_hom.fst R A B).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}

source

@[simp]

theorem star_alg_hom.fst_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (ᾰ : A × B) :

⇑(star_alg_hom.fst R A B) ᾰ = (alg_hom.fst R A B).to_fun ᾰ

source

@[simp]

theorem star_alg_hom.snd_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] (ᾰ : A × B) :

⇑(star_alg_hom.snd R A B) ᾰ = (alg_hom.snd R A B).to_fun ᾰ

source

def star_alg_hom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

A × B →⋆ₐ[R] B

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

Equations

star_alg_hom.snd R A B = {to_fun := (alg_hom.snd R A B).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}

source

@[simp]

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

⇑(f.prod g) ᾰ = (f.to_alg_hom.prod g.to_alg_hom).to_fun ᾰ

source

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

A →⋆ₐ[R] B × C

The pi.prod of two morphisms is a morphism.

Equations

f.prod g = {to_fun := (f.to_alg_hom.prod g.to_alg_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _, map_star' := _}

source

theorem star_alg_hom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

@[simp]

theorem star_alg_hom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :

(star_alg_hom.fst R B C).comp (f.prod g) = f

source

@[simp]

theorem star_alg_hom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) :

(star_alg_hom.snd R B C).comp (f.prod g) = g

source

@[simp]

theorem star_alg_hom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] :

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

source

@[simp]

theorem star_alg_hom.prod_equiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : A →⋆ₐ[R] B × C) :

⇑(star_alg_hom.prod_equiv.symm) f = ((star_alg_hom.fst R B C).comp f, (star_alg_hom.snd R B C).comp f)

source

@[simp]

theorem star_alg_hom.prod_equiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)) :

⇑star_alg_hom.prod_equiv f = f.fst.prod f.snd

source

def star_alg_hom.prod_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [semiring C] [algebra R C] [has_star C] :

(A →⋆ₐ[R] B) × (A →⋆ₐ[R] C) ≃ (A →⋆ₐ[R] B × C)

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

Equations

star_alg_hom.prod_equiv = {to_fun := λ (f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)), f.fst.prod f.snd, inv_fun := λ (f : A →⋆ₐ[R] B × C), ((star_alg_hom.fst R B C).comp f, (star_alg_hom.snd R B C).comp f), left_inv := _, right_inv := _}

source

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

Type (max u_2 u_3)

to_fun : A → B
inv_fun : B → A
left_inv : function.left_inverse self.inv_fun self.to_fun
right_inv : function.right_inverse self.inv_fun self.to_fun
map_mul' : ∀ (x y : A), self.to_fun (x * y) = self.to_fun x * self.to_fun y
map_add' : ∀ (x y : A), self.to_fun (x + y) = self.to_fun x + self.to_fun y
map_star' : ∀ (a : A), self.to_fun (has_star.star a) = has_star.star (self.to_fun a)
map_smul' : ∀ (r : R) (a : A), self.to_fun (r • a) = r • self.to_fun a

A ⋆-algebra equivalence is an equivalence preserving addition, multiplication, scalar multiplication and the star operation, which allows for considering both unital and non-unital equivalences with a single structure. Currently, alg_equiv requires unital algebras, which is why this structure does not extend it.

Instances for star_alg_equiv

source

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

A ≃+* B

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

source

@[class]

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

Type (max u_1 u_3 u_4)

coe : F → A → B
inv : F → B → A
left_inv : ∀ (e : F), function.left_inverse (star_alg_equiv_class.inv e) (star_alg_equiv_class.coe e)
right_inv : ∀ (e : F), function.right_inverse (star_alg_equiv_class.inv e) (star_alg_equiv_class.coe e)
coe_injective' : ∀ (e g : F), star_alg_equiv_class.coe e = star_alg_equiv_class.coe g → star_alg_equiv_class.inv e = star_alg_equiv_class.inv g → e = g
map_mul : ∀ (f : F) (a b : A), ⇑f (a * b) = ⇑f a * ⇑f b
map_add : ∀ (f : F) (a b : A), ⇑f (a + b) = ⇑f a + ⇑f b
map_star : ∀ (f : F) (a : A), ⇑f (has_star.star a) = has_star.star (⇑f a)
map_smul : ∀ (f : F) (r : R) (a : A), ⇑f (r • a) = r • ⇑f a

star_alg_equiv_class F R A B asserts F is a type of bundled ⋆-algebra equivalences between A and B.

You should also extend this typeclass when you extend star_alg_equiv.

Instances of this typeclass

star_alg_equiv.star_alg_equiv_class

Instances of other typeclasses for star_alg_equiv_class

star_alg_equiv_class.has_sizeof_inst

source

@[nolint, instance]

def star_alg_equiv_class.to_ring_equiv_class (F : Type u_1) (R : out_param (Type u_2)) (A : out_param (Type u_3)) (B : out_param (Type u_4)) [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [self : star_alg_equiv_class F R A B] :

ring_equiv_class F A B

source

@[protected, nolint, instance]

def star_alg_equiv_class.star_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [hF : star_alg_equiv_class F R A B] :

star_hom_class F A B

Equations

star_alg_equiv_class.star_hom_class = {coe := λ (f : F), ⇑f, coe_injective' := _, map_star := _}

source

@[protected, nolint, instance]

def star_alg_equiv_class.smul_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_star A] [has_smul R A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [hF : star_alg_equiv_class F R A B] :

smul_hom_class F R A B

Equations

star_alg_equiv_class.smul_hom_class = {coe := λ (f : F), ⇑f, coe_injective' := _, map_smul := _}

source

@[protected, instance]

def star_alg_equiv_class.non_unital_star_alg_hom_class {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : star_alg_equiv_class F R A B] :

non_unital_star_alg_hom_class F R A B

Equations

star_alg_equiv_class.non_unital_star_alg_hom_class = {coe := λ (f : F), ⇑f, coe_injective' := _, map_smul := _, map_add := _, map_zero := _, map_mul := _, map_star := _}

source

@[protected, instance]

def star_alg_equiv_class.star_alg_hom_class (F : Type u_1) (R : Type u_2) (A : Type u_3) (B : Type u_4) [comm_semiring R] [semiring A] [algebra R A] [has_star A] [semiring B] [algebra R B] [has_star B] [hF : star_alg_equiv_class F R A B] :

star_alg_hom_class F R A B

Equations

star_alg_equiv_class.star_alg_hom_class F R A B = {coe := λ (f : F), ⇑f, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _, map_star := _}

source

@[protected, instance]

def star_alg_equiv.star_alg_equiv_class {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :

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

Equations

star_alg_equiv.star_alg_equiv_class = {coe := star_alg_equiv.to_fun _inst_8, inv := star_alg_equiv.inv_fun _inst_8, left_inv := _, right_inv := _, coe_injective' := _, map_mul := _, map_add := _, map_star := _, map_smul := _}

source

@[protected, instance]

def star_alg_equiv.has_coe_to_fun {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :

has_coe_to_fun (A ≃⋆ₐ[R] B) (λ (_x : A ≃⋆ₐ[R] B), A → B)

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

Equations

star_alg_equiv.has_coe_to_fun = {coe := star_alg_equiv.to_fun _inst_8}

source

@[ext]

theorem star_alg_equiv.ext {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {f g : A ≃⋆ₐ[R] B} (h : ∀ (a : A), ⇑f a = ⇑g a) :

f = g

source

theorem star_alg_equiv.ext_iff {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {f g : A ≃⋆ₐ[R] B} :

f = g ↔ ∀ (a : A), ⇑f a = ⇑g a

source

@[refl]

def star_alg_equiv.refl {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :

A ≃⋆ₐ[R] A

Star algebra equivalences are reflexive.

Equations

star_alg_equiv.refl = {to_fun := (ring_equiv.refl A).to_fun, inv_fun := (ring_equiv.refl A).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

@[protected, instance]

def star_alg_equiv.inhabited {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :

inhabited (A ≃⋆ₐ[R] A)

Equations

star_alg_equiv.inhabited = {default := star_alg_equiv.refl _inst_4}

source

@[simp]

theorem star_alg_equiv.coe_refl {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :

⇑star_alg_equiv.refl = id

source

@[symm]

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

B ≃⋆ₐ[R] A

Star algebra equivalences are symmetric.

Equations

e.symm = {to_fun := e.to_ring_equiv.symm.to_fun, inv_fun := e.to_ring_equiv.symm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

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

B → A

See Note [custom simps projection]

Equations

star_alg_equiv.simps.symm_apply e = ⇑(e.symm)

source

@[simp]

theorem star_alg_equiv.inv_fun_eq_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] {e : A ≃⋆ₐ[R] B} :

e.inv_fun = ⇑(e.symm)

source

@[simp]

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

e.symm.symm = e

source

theorem star_alg_equiv.symm_bijective {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] :

function.bijective star_alg_equiv.symm

source

@[simp]

theorem star_alg_equiv.mk_coe' {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (f : B → A) (h₁ : function.left_inverse ⇑e f) (h₂ : function.right_inverse ⇑e f) (h₃ : ∀ (x y : B), f (x * y) = f x * f y) (h₄ : ∀ (x y : B), f (x + y) = f x + f y) (h₅ : ∀ (a : B), f (has_star.star a) = has_star.star (f a)) (h₆ : ∀ (r : R) (a : B), f (r • a) = r • f a) :

{to_fun := f, inv_fun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆} = e.symm

source

@[simp]

theorem star_alg_equiv.symm_mk {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (f : A → B) (f' : B → A) (h₁ : function.left_inverse f' f) (h₂ : function.right_inverse f' f) (h₃ : ∀ (x y : A), f (x * y) = f x * f y) (h₄ : ∀ (x y : A), f (x + y) = f x + f y) (h₅ : ∀ (a : A), f (has_star.star a) = has_star.star (f a)) (h₆ : ∀ (r : R) (a : A), f (r • a) = r • f a) :

{to_fun := f, inv_fun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆}.symm = {to_fun := f', inv_fun := f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

@[simp]

theorem star_alg_equiv.refl_symm {R : Type u_2} {A : Type u_3} [has_add A] [has_mul A] [has_smul R A] [has_star A] :

star_alg_equiv.refl.symm = star_alg_equiv.refl

source

theorem star_alg_equiv.to_ring_equiv_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (f : A ≃⋆ₐ[R] B) :

↑f.symm = ↑(f.symm)

source

@[simp]

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

↑(e.symm) = ↑e.symm

source

@[trans]

def star_alg_equiv.trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :

A ≃⋆ₐ[R] C

Star algebra equivalences are transitive.

Equations

e₁.trans e₂ = {to_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).to_fun, inv_fun := (e₁.to_ring_equiv.trans e₂.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

@[simp]

theorem star_alg_equiv.apply_symm_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (x : B) :

⇑e (⇑(e.symm) x) = x

source

@[simp]

theorem star_alg_equiv.symm_apply_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] (e : A ≃⋆ₐ[R] B) (x : A) :

⇑(e.symm) (⇑e x) = x

source

@[simp]

theorem star_alg_equiv.symm_trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : C) :

⇑((e₁.trans e₂).symm) x = ⇑(e₁.symm) (⇑(e₂.symm) x)

source

@[simp]

theorem star_alg_equiv.coe_trans {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) :

⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁

source

@[simp]

theorem star_alg_equiv.trans_apply {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [has_add A] [has_mul A] [has_smul R A] [has_star A] [has_add B] [has_mul B] [has_smul R B] [has_star B] [has_add C] [has_mul C] [has_smul R C] [has_star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : A) :

⇑(e₁.trans e₂) x = ⇑e₂ (⇑e₁ x)

source

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

function.left_inverse ⇑(e.symm) ⇑e

source

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

function.right_inverse ⇑(e.symm) ⇑e

source

def star_alg_equiv.of_star_alg_hom {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ⇑g (⇑f x) = x) (h₂ : ∀ (x : B), ⇑f (⇑g x) = x) :

A ≃⋆ₐ[R] B

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

Equations

star_alg_equiv.of_star_alg_hom f g h₁ h₂ = {to_fun := ⇑f, inv_fun := ⇑g, left_inv := h₁, right_inv := h₂, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

@[simp]

theorem star_alg_equiv.of_star_alg_hom_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ⇑g (⇑f x) = x) (h₂ : ∀ (x : B), ⇑f (⇑g x) = x) (a : A) :

⇑(star_alg_equiv.of_star_alg_hom f g h₁ h₂) a = ⇑f a

source

@[simp]

theorem star_alg_equiv.of_star_alg_hom_symm_apply {F : Type u_1} {G : Type u_2} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] [non_unital_star_alg_hom_class G R B A] (f : F) (g : G) (h₁ : ∀ (x : A), ⇑g (⇑f x) = x) (h₂ : ∀ (x : B), ⇑f (⇑g x) = x) (a : B) :

⇑((star_alg_equiv.of_star_alg_hom f g h₁ h₂).symm) a = ⇑g a

source

noncomputable def star_alg_equiv.of_bijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] (f : F) (hf : function.bijective ⇑f) :

A ≃⋆ₐ[R] B

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

Equations

star_alg_equiv.of_bijective f hf = {to_fun := ⇑f, inv_fun := (ring_equiv.of_bijective f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

source

@[simp]

theorem star_alg_equiv.coe_of_bijective {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] {f : F} (hf : function.bijective ⇑f) :

⇑(star_alg_equiv.of_bijective f hf) = ⇑f

source

theorem star_alg_equiv.of_bijective_apply {F : Type u_1} {R : Type u_3} {A : Type u_4} {B : Type u_5} [monoid R] [non_unital_non_assoc_semiring A] [distrib_mul_action R A] [has_star A] [non_unital_non_assoc_semiring B] [distrib_mul_action R B] [has_star B] [hF : non_unital_star_alg_hom_class F R A B] {f : F} (hf : function.bijective ⇑f) (a : A) :

⇑(star_alg_equiv.of_bijective f hf) a = ⇑f a

mathlib3 documentation

Morphisms of star algebras #

Main definitions #

Tags #

Non-unital star algebra homomorphisms #

Unital star algebra homomorphisms #

Operations on the product type #

Star algebra equivalences #