Documentation

Mathlib.Topology.Algebra.Module.Star

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

source
def «term_→L⋆[_]_» :
Lean.TrailingParserDescr

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations
    Instances For
      source
      def «term_≃L⋆[_]_» :
      Lean.TrailingParserDescr

      Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

      Equations
        Instances For
          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] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] (a✝ : A) :
              (starL R).symm a✝ = starAddEquiv.symm 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] [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
                Instances For
                  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
                  @[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) :
                  (starL' R).symm a✝ = (starL R).symm ({ toFun := id, map_add' := ⋯, map_smul' := ⋯, invFun := id, left_inv := ⋯, right_inv := ⋯ }.symm a✝)
                  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] [IsTopologicalAddGroup 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] [ContinuousAdd A] :
                  Continuous ⇑(StarModule.decomposeProdAdjoint R A).symm
                  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] ↥(selfAdjoint A)

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

                  Equations
                    Instances For
                      source
                      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
                      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] ↥(skewAdjoint A)

                      The skew-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
                          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] [IsTopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] :
                          A ≃L[R] ↥(selfAdjoint A) × ↥(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
                              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] [IsTopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (i : A) :
                              (decomposeProdAdjointL R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)
                              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] [IsTopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (a : ↥(selfAdjoint A) × ↥(skewAdjoint A)) :
                              (decomposeProdAdjointL R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2