def StarAlgEquiv.restrictScalars' (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [SMul R S] [Module S A] [Module S B] [Module R A] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) : A ≃⋆ₐ[R] B

Restrict the scalar ring of a star algebra equivalence.

Equations

• StarAlgEquiv.restrictScalars' R f = { toFun := ⇑f, invFun := f.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

@[simp]

theorem StarAlgEquiv.restrictScalars'_symm_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [SMul R S] [Module S A] [Module S B] [Module R A] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) (a✝ : B) : (restrictScalars' R f).symm a✝ = f.invFun a✝

@[simp]

theorem StarAlgEquiv.restrictScalars'_apply (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [SMul R S] [Module S A] [Module S B] [Module R A] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] (f : A ≃⋆ₐ[S] B) (a : A) : (restrictScalars' R f) a = f a

theorem StarAlgEquiv.restrictScalars_injective' (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [CommSemiring S] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [SMul R S] [Module S A] [Module S B] [Module R A] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [Star A] [Star B] : Function.Injective (restrictScalars' R)

def StarAlgEquiv.toNonUnitalStarAlgHom {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) : A₁ →⋆ₙₐ[R] A₂

Reintrepret a star algebra equivalence as a non-unital star algebra homomorphism.

Equations

• e.toNonUnitalStarAlgHom = { toFun := ⇑e, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem StarAlgEquiv.toNonUnitalStarAlgHom_apply {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) (a : A₁) : e.toNonUnitalStarAlgHom a = e a

@[simp]

theorem StarAlgEquiv.toNonUnitalStarAlgHom_comp {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₃] [DistribMulAction R A₃] [Star A₃] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃) : e₂.toNonUnitalStarAlgHom.comp e₁.toNonUnitalStarAlgHom = (e₁.trans e₂).toNonUnitalStarAlgHom

def StarAlgEquiv.arrowCongr' {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁'] [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') : (A₁ →⋆ₙₐ[R] A₂) ≃ (A₁' →⋆ₙₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂' as star algebras, then the type of maps A₁ →⋆ₙₐ[R] A₂ is equivalent to the type of maps A₁' →⋆ₙₐ[R] A₂'.

Equations

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

@[simp]

theorem StarAlgEquiv.arrowCongr'_apply {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁'] [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (f : A₁ →⋆ₙₐ[R] A₂) : (e₁.arrowCongr' e₂) f = (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom

theorem StarAlgEquiv.arrowCongr'_comp {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₃] [DistribMulAction R A₃] [Star A₃] [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁'] [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂'] [NonUnitalNonAssocSemiring A₃'] [DistribMulAction R A₃'] [Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₃) : (e₁.arrowCongr' e₃) (g.comp f) = ((e₂.arrowCongr' e₃) g).comp ((e₁.arrowCongr' e₂) f)

@[simp]

theorem StarAlgEquiv.arrowCongr'_refl {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] : refl.arrowCongr' refl = Equiv.refl (A₁ →⋆ₙₐ[R] A₂)

@[simp]

theorem StarAlgEquiv.arrowCongr'_trans {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₃] [DistribMulAction R A₃] [Star A₃] [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁'] [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂'] [NonUnitalNonAssocSemiring A₃'] [DistribMulAction R A₃'] [Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₁' : A₁' ≃⋆ₐ[R] A₂') (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃') : (e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')

@[simp]

theorem StarAlgEquiv.arrowCongr'_symm {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [Monoid R] [NonUnitalNonAssocSemiring A₁] [DistribMulAction R A₁] [Star A₁] [NonUnitalNonAssocSemiring A₂] [DistribMulAction R A₂] [Star A₂] [NonUnitalNonAssocSemiring A₁'] [DistribMulAction R A₁'] [Star A₁'] [NonUnitalNonAssocSemiring A₂'] [DistribMulAction R A₂'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') : (e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm

def StarAlgEquiv.ofHomInv' {R : Type u_8} {A : Type u_9} {B : Type u_10} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] A) (h₁ : g.comp f = NonUnitalStarAlgHom.id R A) (h₂ : f.comp g = NonUnitalStarAlgHom.id R B) : A ≃⋆ₐ[R] B

Construct a star algebra equivalence from a pair of non-unital star algebra homomorphisms.

Equations

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

@[simp]

theorem StarAlgEquiv.ofHomInv'_symm_apply {R : Type u_8} {A : Type u_9} {B : Type u_10} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] A) (h₁ : g.comp f = NonUnitalStarAlgHom.id R A) (h₂ : f.comp g = NonUnitalStarAlgHom.id R B) (a : B) : (ofHomInv' f g h₁ h₂).symm a = g a

@[simp]

theorem StarAlgEquiv.ofHomInv'_apply {R : Type u_8} {A : Type u_9} {B : Type u_10} [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] [Star A] [NonUnitalNonAssocSemiring B] [DistribMulAction R B] [Star B] (f : A →⋆ₙₐ[R] B) (g : B →⋆ₙₐ[R] A) (h₁ : g.comp f = NonUnitalStarAlgHom.id R A) (h₂ : f.comp g = NonUnitalStarAlgHom.id R B) (a : A) : (ofHomInv' f g h₁ h₂) a = f a

def StarAlgEquiv.toStarAlgHom {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] [Star A₁] [Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) : A₁ →⋆ₐ[R] A₂

Reintrepret a star algebra equivalence as a star algebra homomorphism.

Equations

• e.toStarAlgHom = { toFun := ⇑e, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem StarAlgEquiv.toStarAlgHom_apply {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] [Star A₁] [Star A₂] (e : A₁ ≃⋆ₐ[R] A₂) (a : A₁) : e.toStarAlgHom a = e a

@[simp]

theorem StarAlgEquiv.toStarAlgHom_comp {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Star A₁] [Star A₂] [Star A₃] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₂ : A₂ ≃⋆ₐ[R] A₃) : e₂.toStarAlgHom.comp e₁.toStarAlgHom = (e₁.trans e₂).toStarAlgHom

def StarAlgEquiv.arrowCongr {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] [Star A₁] [Star A₂] [Star A₁'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') : (A₁ →⋆ₐ[R] A₂) ≃ (A₁' →⋆ₐ[R] A₂')

If A₁ is equivalent to A₁' and A₂ is equivalent to A₂' as star algebras, then the type of maps A₁ →⋆ₐ[R] A₂ is equivalent to the type of maps A₁' →⋆ₐ[R] A₂'.

Equations

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

@[simp]

theorem StarAlgEquiv.arrowCongr_apply {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] [Star A₁] [Star A₂] [Star A₁'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (f : A₁ →⋆ₐ[R] A₂) : (e₁.arrowCongr e₂) f = (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom

theorem StarAlgEquiv.arrowCongr_comp {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Semiring A₁'] [Semiring A₂'] [Semiring A₃'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] [Star A₁] [Star A₂] [Star A₃] [Star A₁'] [Star A₂'] [Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₐ[R] A₂) (g : A₂ →⋆ₐ[R] A₃) : (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)

@[simp]

theorem StarAlgEquiv.arrowCongr_refl {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] [Star A₁] [Star A₂] : refl.arrowCongr refl = Equiv.refl (A₁ →⋆ₐ[R] A₂)

@[simp]

theorem StarAlgEquiv.arrowCongr_trans {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₃] [Semiring A₁'] [Semiring A₂'] [Semiring A₃'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₃] [Algebra R A₁'] [Algebra R A₂'] [Algebra R A₃'] [Star A₁] [Star A₂] [Star A₃] [Star A₁'] [Star A₂'] [Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₂) (e₁' : A₁' ≃⋆ₐ[R] A₂') (e₂ : A₂ ≃⋆ₐ[R] A₃) (e₂' : A₂' ≃⋆ₐ[R] A₃') : (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')

@[simp]

theorem StarAlgEquiv.arrowCongr_symm {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₁' : Type u_5} {A₂' : Type u_6} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Semiring A₁'] [Semiring A₂'] [Algebra R A₁] [Algebra R A₂] [Algebra R A₁'] [Algebra R A₂'] [Star A₁] [Star A₂] [Star A₁'] [Star A₂'] (e₁ : A₁ ≃⋆ₐ[R] A₁') (e₂ : A₂ ≃⋆ₐ[R] A₂') : (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm

def StarAlgEquiv.ofHomInv {R : Type u_8} {A : Type u_9} {B : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A) (h₁ : g.comp f = StarAlgHom.id R A) (h₂ : f.comp g = StarAlgHom.id R B) : A ≃⋆ₐ[R] B

Construct a star algebra equivalence from a pair of star algebra homomorphisms.

Equations

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

@[simp]

theorem StarAlgEquiv.ofHomInv_symm_apply {R : Type u_8} {A : Type u_9} {B : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A) (h₁ : g.comp f = StarAlgHom.id R A) (h₂ : f.comp g = StarAlgHom.id R B) (a : B) : (ofHomInv f g h₁ h₂).symm a = g a

@[simp]

theorem StarAlgEquiv.ofHomInv_apply {R : Type u_8} {A : Type u_9} {B : Type u_10} [CommSemiring R] [Semiring A] [Algebra R A] [Star A] [Semiring B] [Algebra R B] [Star B] (f : A →⋆ₐ[R] B) (g : B →⋆ₐ[R] A) (h₁ : g.comp f = StarAlgHom.id R A) (h₂ : f.comp g = StarAlgHom.id R B) (a : A) : (ofHomInv f g h₁ h₂) a = f a