Some stuff on star algebra equivalences #

This file contains some obvious definitions and lemmas on star algebra equivalences.

theorem AlgEquiv.comp_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : B ≃ₐ[R] C) (S T : A →ₗ[R] B) :

f.toLinearMap ∘ₗ S = f.toLinearMap ∘ₗ T ↔ S = T

source

theorem AlgEquiv.inj_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] (f : C ≃ₐ[R] A) (S T : A →ₗ[R] B) :

S ∘ₗ f.toLinearMap = T ∘ₗ f.toLinearMap ↔ S = T

source

def StarAlgEquiv.toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :

A →ₗ[R] B

Equations

f.toLinearMap = { toFun := fun (x : A) => f x, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem StarAlgEquiv.toLinearMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) (x : A) :

f.toLinearMap x = f x

source

theorem StarAlgEquiv.injective {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] (f : A ≃⋆ₐ[R] B) :

Function.Injective ⇑f

source

theorem StarAlgEquiv.comp_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Mul B] [Mul C] [Module R A] [Module R B] [Module R C] [Star B] [Star C] (f : B ≃⋆ₐ[R] C) (S T : A →ₗ[R] B) :

f.toLinearMap ∘ₗ S = f.toLinearMap ∘ₗ T ↔ S = T

source

theorem StarAlgEquiv.inj_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [Mul A] [Mul C] [Module R A] [Module R B] [Module R C] [Star A] [Star C] (f : C ≃⋆ₐ[R] A) (S T : A →ₗ[R] B) :

S ∘ₗ f.toLinearMap = T ∘ₗ f.toLinearMap ↔ S = T

source

def StarAlgEquiv.toLinearEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :

A ≃ₗ[R] B

Equations

f.toLinearEquiv = { toFun := fun (x : A) => f x, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : B) => f.symm x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem StarAlgEquiv.toLinearEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) (x : A) :

f.toLinearEquiv x = f x

source

@[simp]

theorem StarAlgEquiv.toLinearEquiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) (x : B) :

f.toLinearEquiv.symm x = f.symm x

source

def StarAlgEquiv.toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :

A ≃ₐ[R] B

Equations

f.toAlgEquiv = { toFun := fun (x : A) => f x, invFun := fun (x : B) => f.symm x, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem StarAlgEquiv.coe_toAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) :

⇑f.toAlgEquiv = ⇑f

source

theorem StarAlgEquiv.symm_apply_eq {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] (f : A ≃⋆ₐ[R] B) (x : A) (y : B) :

f.symm y = x ↔ y = f x

source

def StarAlgEquiv.ofAlgEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), f (star x) = star (f x)) :

A ≃⋆ₐ[R] B

Equations

StarAlgEquiv.ofAlgEquiv f hf = { toFun := fun (x : A) => f x, invFun := fun (x : B) => f.symm x, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem StarAlgEquiv.ofAlgEquiv_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), f (star x) = star (f x)) :

⇑(ofAlgEquiv f hf) = ⇑f

source

@[simp]

theorem StarAlgEquiv.ofAlgEquiv_symm_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), f (star x) = star (f x)) :

⇑(ofAlgEquiv f hf).symm = ⇑f.symm

source

theorem StarAlgEquiv.comp_eq_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [CommSemiring R] [AddCommMonoid E₁] [AddCommMonoid E₂] [AddCommMonoid E₃] [Module R E₁] [Module R E₂] [Module R E₃] [Star E₁] [Star E₂] [Mul E₁] [Mul E₂] (f : E₁ ≃⋆ₐ[R] E₂) (x : E₂ →ₗ[R] E₃) (y : E₁ →ₗ[R] E₃) :

x ∘ₗ f.toLinearMap = y ↔ x = y ∘ₗ f.symm.toLinearMap

source

theorem AlgEquiv.map_eq_zero_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [CommSemiring R] [Semiring E₁] [Semiring E₂] [Algebra R E₁] [Algebra R E₂] (f : E₁ ≃ₐ[R] E₂) (x : E₁) :

f x = 0 ↔ x = 0

source

theorem StarAlgEquiv.map_eq_zero_iff {R : Type u_1} {A : Type u_2} {B : Type u_3} [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [SMul R A] [SMul R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) (x : A) :

f x = 0 ↔ x = 0

source

theorem IsIdempotentElem.mulEquiv {H₁ : Type u_2} {H₂ : Type u_3} [Mul H₁] [Mul H₂] {F : Type u_1} [EquivLike F H₁ H₂] [MulEquivClass F H₁ H₂] {f : F} {x : H₁} :

IsIdempotentElem (f x) ↔ IsIdempotentElem x

source

theorem IsIdempotentElem.algEquiv {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Algebra R H₁] [Algebra R H₂] (f : H₁ ≃ₐ[R] H₂) {x : H₁} :

IsIdempotentElem (f x) ↔ IsIdempotentElem x

source

theorem IsIdempotentElem.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] (f : A ≃⋆ₐ[R] B) {x : A} :

IsIdempotentElem (f x) ↔ IsIdempotentElem x

source

theorem isIdempotentElem_pi_iff {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → Mul (A i)] {a : (i : ι) → A i} :

IsIdempotentElem a ↔ ∀ (i : ι), IsIdempotentElem (a i)

source

theorem AlgEquiv.eq_apply_iff_symm_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {a : B} {b : A} :

a = f b ↔ f.symm a = b

source

theorem StarAlgEquiv.eq_apply_iff_symm_eq {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] (f : A ≃⋆ₐ[R] B) {a : B} {b : A} :

a = f b ↔ f.symm a = b

source

theorem AlgEquiv.apply_eq_iff_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A ≃ₐ[R] B) {x y : A} :

f x = f y ↔ x = y

source

theorem MulEquiv.image_center {F : Type u_1} {A : Type u_2} {B : Type u_3} [Semigroup A] [Semigroup B] [EquivLike F A B] [MulEquivClass F A B] (f : F) :

⇑f '' Set.center A = Set.center B

source

instance instMulEquivClassOfNonUnitalAlgHomClass_monlib {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Monoid R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [DistribMulAction R A] [DistribMulAction R B] [EquivLike F A B] [NonUnitalAlgHomClass F R A B] :

MulEquivClass F A B

source

theorem NonUnitalAlgEquiv.image_span_center {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Semiring R] [NonUnitalSemiring A] [NonUnitalSemiring B] [Module R A] [Module R B] [EquivLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) :

⇑f '' ↑(Submodule.span R (Set.center A)) = ↑(Submodule.span R (Set.center B))

source

theorem NonUnitalAlgEquiv.map_span_center {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [Semiring R] [NonUnitalSemiring A] [NonUnitalSemiring B] [Module R A] [Module R B] [EquivLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) :

Submodule.map f (Submodule.span R (Set.center A)) = Submodule.span R (Set.center B)

source

def StarAlgEquiv.piCongrRight {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} [(i : ι) → Add (A₁ i)] [(i : ι) → Add (A₂ i)] [(i : ι) → Mul (A₁ i)] [(i : ι) → Mul (A₂ i)] [(i : ι) → Star (A₁ i)] [(i : ι) → Star (A₂ i)] [(i : ι) → SMul R (A₁ i)] [(i : ι) → SMul R (A₂ i)] (e : (i : ι) → A₁ i ≃⋆ₐ[R] A₂ i) :

((i : ι) → A₁ i) ≃⋆ₐ[R] (i : ι) → A₂ i

Equations

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

Instances For

source

@[simp]

theorem StarAlgEquiv.piCongrRight_apply {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} [(i : ι) → Add (A₁ i)] [(i : ι) → Add (A₂ i)] [(i : ι) → Mul (A₁ i)] [(i : ι) → Mul (A₂ i)] [(i : ι) → Star (A₁ i)] [(i : ι) → Star (A₂ i)] [(i : ι) → SMul R (A₁ i)] [(i : ι) → SMul R (A₂ i)] (e : (i : ι) → A₁ i ≃⋆ₐ[R] A₂ i) (x : (i : ι) → A₁ i) (j : ι) :

(piCongrRight e) x j = (e j) (x j)

source

@[simp]

theorem AlgEquiv.coe_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₃] (e : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :

e₂.toLinearMap ∘ₗ e.toLinearMap = (e.trans e₂).toLinearMap

source

@[simp]

theorem AlgEquiv.self_trans_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

f.trans f.symm = refl

source

@[simp]

theorem AlgEquiv.symm_trans_self {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

f.symm.trans f = refl

source

theorem AlgEquiv.refl_toLinearMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :

refl.toLinearMap = LinearMap.id

source

theorem AlgEquiv.symm_comp_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) :

e.symm.toLinearMap ∘ₗ e.toLinearMap = LinearMap.id

source

theorem AlgEquiv.comp_symm_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) :

e.toLinearMap ∘ₗ e.symm.toLinearMap = LinearMap.id

Documentation

Monlib.Preq.StarAlgEquiv

Some stuff on star algebra equivalences #