Documentation

Monlib.Preq.StarAlgEquiv

Some stuff on star algebra equivalences #

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

source
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 : A →ₗ[R] B) (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 : A →ₗ[R] B) (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 : A →ₗ[R] B) (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 : A →ₗ[R] B) (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)) :
          ⇑(StarAlgEquiv.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)) :
          ⇑(StarAlgEquiv.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 : A} {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
          Equations
          • ⋯ = ⋯
          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 : ι) :
            (StarAlgEquiv.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 = AlgEquiv.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 = AlgEquiv.refl
            source
            theorem AlgEquiv.refl_toLinearMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] :
            AlgEquiv.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