Documentation

Mathlib.Topology.Algebra.Module.Star

The star operation, bundled as a continuous star-linear equiv #

source
@[simp]
theorem starL_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
∀ (a : A), ↑(ContinuousLinearEquiv.symm (starL R)) a = ↑(AddEquiv.symm starAddEquiv) a
source
@[simp]
theorem starL_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
∀ (a : A), ↑(starL R) a = star a
source
def starL (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
A ≃L⋆[R] A

If A is a topological module over a commutative R with compatible actions, then star is a continuous semilinear equivalence.

Equations
Instances For
    source
    @[simp]
    theorem starL'_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
    ∀ (a : A), ↑(ContinuousLinearEquiv.symm (starL' R)) a = ↑↑(LinearEquiv.symm (starL R).toLinearEquiv) (↑↑(LinearEquiv.symm { toLinearMap := { toAddHom := { toFun := id, map_add' := (_ : ∀ (x y : A), Equiv.toFun (AddEquiv.refl A).toEquiv (x + y) = Equiv.toFun (AddEquiv.refl A).toEquiv x + Equiv.toFun (AddEquiv.refl A).toEquiv y) }, map_smul' := (_ : ∀ (r : R) (a : A), r • a = star r • a) }, invFun := id, left_inv := (_ : Function.LeftInverse (AddEquiv.refl A).toEquiv.invFun (AddEquiv.refl A).toEquiv.toFun), right_inv := (_ : Function.RightInverse (AddEquiv.refl A).toEquiv.invFun (AddEquiv.refl A).toEquiv.toFun) }) a)
    source
    @[simp]
    theorem starL'_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
    ∀ (a : A), ↑(starL' R) a = star a
    source
    def starL' (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] :
    A ≃L[R] A

    If A is a topological module over a commutative R with trivial star and compatible actions, then star is a continuous linear equivalence.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem continuous_selfAdjointPart (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] :
      Continuous ↑(selfAdjointPart R)
      source
      theorem continuous_skewAdjointPart (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] :
      Continuous ↑(skewAdjointPart R)
      source
      theorem continuous_decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] :
      Continuous ↑(StarModule.decomposeProdAdjoint R A)
      source
      theorem continuous_decomposeProdAdjoint_symm (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] :
      Continuous ↑(LinearEquiv.symm (StarModule.decomposeProdAdjoint R A))
      source
      @[simp]
      theorem selfAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) :
      ↑(↑(selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x
      source
      @[simp]
      theorem selfAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) :
      ↑(↑(selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x
      source
      def selfAdjointPartL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] :
      A →L[R] { x // x ∈ selfAdjoint A }

      The self-adjoint part of an element of a star module, as a continuous linear map.

      Equations
      Instances For
        source
        @[simp]
        theorem skewAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) :
        ↑(↑(skewAdjointPartL R A) x) = ⅟2 • (x - star x)
        source
        @[simp]
        theorem skewAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) :
        ↑(↑(skewAdjointPartL R A) x) = ⅟2 • (x - star x)
        source
        def skewAdjointPartL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] :
        A →L[R] { x // x ∈ skewAdjoint A }

        The skew-adjoint part of an element of a star module, as a continuous linear map.

        Equations
        Instances For
          source
          @[simp]
          theorem StarModule.decomposeProdAdjointL_symm_apply (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (a : { x // x ∈ selfAdjoint A } × { x // x ∈ skewAdjoint A }) :
          ↑(ContinuousLinearEquiv.symm (StarModule.decomposeProdAdjointL R A)) a = ↑(Submodule.subtype (selfAdjoint.submodule R A)) a.fst + ↑(Submodule.subtype (skewAdjoint.submodule R A)) a.snd
          source
          @[simp]
          theorem StarModule.decomposeProdAdjointL_apply (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (i : A) :
          ↑(StarModule.decomposeProdAdjointL R A) i = (↑(selfAdjointPart R) i, ↑(skewAdjointPart R) i)
          source
          def StarModule.decomposeProdAdjointL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] :
          A ≃L[R] { x // x ∈ selfAdjoint A } × { x // x ∈ skewAdjoint A }

          The decomposition of elements of a star module into their self- and skew-adjoint parts, as a continuous linear equivalence.

          Equations
          Instances For