mathlib3 documentation

monlib / preq.star_alg_equiv

Some stuff on star algebra equivalences #

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

theorem alg_equiv.comp_inj {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring 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.to_linear_map.comp S = f.to_linear_map.comp T ↔ S = T

theorem alg_equiv.inj_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring 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.comp f.to_linear_map = T.comp f.to_linear_map ↔ S = T

def star_alg_equiv.to_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃⋆ₐ[R] B) :

Equations

f.to_alg_equiv = {to_fun := λ (x : A), ⇑f x, inv_fun := λ (x : B), ⇑(f.symm) x, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[simp]

theorem star_alg_equiv.coe_to_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃⋆ₐ[R] B) :

⇑(f.to_alg_equiv) = ⇑f

theorem star_alg_equiv.symm_apply_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃⋆ₐ[R] B) (x : A) (y : B) :

⇑(f.symm) y = x ↔ y = ⇑f x

def star_alg_equiv.of_alg_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), ⇑f (has_star.star x) = has_star.star (⇑f x)) :

A ≃⋆ₐ[R] B

Equations

star_alg_equiv.of_alg_equiv f hf = {to_fun := λ (x : A), ⇑f x, inv_fun := λ (x : B), ⇑(f.symm) x, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, map_star' := _, map_smul' := _}

@[simp]

theorem star_alg_equiv.of_alg_equiv_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), ⇑f (has_star.star x) = has_star.star (⇑f x)) :

⇑(star_alg_equiv.of_alg_equiv f hf) = ⇑f

@[simp]

theorem star_alg_equiv.of_alg_equiv_symm_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃ₐ[R] B) (hf : ∀ (x : A), ⇑f (has_star.star x) = has_star.star (⇑f x)) :

⇑((star_alg_equiv.of_alg_equiv f hf).symm) = ⇑(f.symm)

theorem star_alg_equiv.comp_eq_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [comm_semiring R] [semiring E₁] [semiring E₂] [add_comm_group E₃] [algebra R E₁] [algebra R E₂] [module R E₃] [has_star E₁] [has_star E₂] (f : E₁ ≃⋆ₐ[R] E₂) (x : E₂ →ₗ[R] E₃) (y : E₁ →ₗ[R] E₃) :

x.comp f.to_alg_equiv.to_linear_map = y ↔ x = y.comp f.symm.to_alg_equiv.to_linear_map

theorem alg_equiv.one_to_linear_map {R : Type u_1} {E : Type u_2} [comm_semiring R] [semiring E] [algebra R E] :

1.to_linear_map = 1

theorem alg_equiv.map_eq_zero_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [comm_semiring R] [semiring E₁] [semiring E₂] [algebra R E₁] [algebra R E₂] (f : E₁ ≃ₐ[R] E₂) (x : E₁) :

⇑f x = 0 ↔ x = 0

theorem star_alg_equiv.map_eq_zero_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [comm_semiring R] [semiring E₁] [semiring E₂] [algebra R E₁] [algebra R E₂] [has_star E₁] [has_star E₂] (f : E₁ ≃⋆ₐ[R] E₂) (x : E₁) :

⇑f x = 0 ↔ x = 0

theorem is_idempotent_elem.mul_equiv {H₁ : Type u_1} {H₂ : Type u_2} [semiring H₁] [semiring H₂] (f : H₁ ≃* H₂) (x : H₁) :

is_idempotent_elem (⇑f x) ↔ is_idempotent_elem x

theorem is_idempotent_elem.alg_equiv {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [comm_semiring R] [semiring H₁] [semiring H₂] [algebra R H₁] [algebra R H₂] (f : H₁ ≃ₐ[R] H₂) (x : H₁) :

is_idempotent_elem (⇑f x) ↔ is_idempotent_elem x

theorem is_idempotent_elem.star_alg_equiv {R : Type u_1} {H₁ : Type u_2} {H₂ : Type u_3} [comm_semiring R] [semiring H₁] [semiring H₂] [algebra R H₁] [algebra R H₂] [has_star H₁] [has_star H₂] (f : H₁ ≃⋆ₐ[R] H₂) (x : H₁) :

is_idempotent_elem (⇑f x) ↔ is_idempotent_elem x

theorem star_alg_equiv.injective {R : Type u_1} {α : Type u_2} {β : Type u_3} [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] [has_star α] [has_star β] (f : α ≃⋆ₐ[R] β) :

function.injective ⇑f

theorem alg_equiv.eq_apply_iff_symm_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring 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

theorem star_alg_equiv.eq_apply_iff_symm_eq {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B] [has_star A] [has_star B] (f : A ≃⋆ₐ[R] B) {a : B} {b : A} :

a = ⇑f b ↔ ⇑(f.symm) a = b