Documentation

Mathlib.Topology.Algebra.Module.Star

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

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
  • One or more equations did not get rendered due to their size.
Instances For

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[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
      @[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
      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] :

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

      Equations
      Instances For
        @[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
        @[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)
        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

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

          Equations
          Instances For
            @[simp]
            @[simp]

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

            Equations
            Instances For

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

              Equations
              Instances For