Documentation

LeanPool.Stafford38.Stafford38.Weyl.Transposition

Transposition of the presented Weyl algebra #

This file constructs the scalar-preserving Weyl transposition as an algebra equivalence with the opposite algebra. Coordinates are fixed and momenta change sign. The construction uses only the checked universal property of the quotient presentation.

source
def Stafford38.WeylTransposition.coordinate (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
WeylIteratedEquivalence.PresentedWeyl k n

The coordinate generator with index i.

Equations
Instances For
    source
    def Stafford38.WeylTransposition.momentum (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
    WeylIteratedEquivalence.PresentedWeyl k n

    The momentum generator with index i.

    Equations
    Instances For
      source
      def Stafford38.WeylTransposition.transposedGenerator (k : Type u) [Field k] (n : ℕ) :
      Fin n ⊕ Fin n → (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ

      Generator images for the Weyl transposition.

      Equations
      Instances For
        source
        theorem Stafford38.WeylTransposition.underlying_transposedGenerator_commutator (k : Type u) [Field k] (n : ℕ) (i j : Fin n ⊕ Fin n) :
        -Stafford.commutator (MulOpposite.unop (transposedGenerator k n i)) (MulOpposite.unop (transposedGenerator k n j)) = (algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)) (Matrix.J (Fin n) k i j)
        source
        theorem Stafford38.WeylTransposition.transposedGenerator_commutator (k : Type u) [Field k] (n : ℕ) (i j : Fin n ⊕ Fin n) :
        Stafford.commutator (transposedGenerator k n i) (transposedGenerator k n j) = (algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ) (Matrix.J (Fin n) k i j)
        source
        def Stafford38.WeylTransposition.transpositionHom (k : Type u) [Field k] (n : ℕ) :
        WeylIteratedEquivalence.PresentedWeyl k n →ₐ[k] (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ

        The scalar-preserving anti-homomorphism x_i ↦ x_i, p_i ↦ -p_i, represented as an algebra homomorphism to the opposite algebra.

        Equations
        Instances For
          source
          @[simp]
          theorem Stafford38.WeylTransposition.transpositionHom_coordinate (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
          (transpositionHom k n) (coordinate k n i) = MulOpposite.op (coordinate k n i)
          source
          @[simp]
          theorem Stafford38.WeylTransposition.transpositionHom_momentum (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
          (transpositionHom k n) (momentum k n i) = MulOpposite.op (-momentum k n i)
          source
          theorem Stafford38.WeylTransposition.opComm_transpositionHom_comp_transpositionHom (k : Type u) [Field k] (n : ℕ) :
          (AlgHom.opComm (transpositionHom k n)).comp (transpositionHom k n) = AlgHom.id k (WeylIteratedEquivalence.PresentedWeyl k n)

          Applying transposition once on each side of the opposite equivalence is the identity.

          source
          theorem Stafford38.WeylTransposition.transpositionHom_comp_opComm_transpositionHom (k : Type u) [Field k] (n : ℕ) :
          (transpositionHom k n).comp (AlgHom.opComm (transpositionHom k n)) = AlgHom.id k (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ
          source
          def Stafford38.WeylTransposition.transpositionEquiv (k : Type u) [Field k] (n : ℕ) :
          WeylIteratedEquivalence.PresentedWeyl k n ≃ₐ[k] (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ

          Transposition is a scalar-preserving equivalence with the opposite Weyl algebra.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Stafford38.WeylTransposition.transpositionEquiv_apply (k : Type u) [Field k] (n : ℕ) (a : WeylIteratedEquivalence.PresentedWeyl k n) :
            (transpositionEquiv k n) a = (transpositionHom k n) a
            source
            theorem Stafford38.WeylTransposition.transpositionEquiv_coordinate (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
            (transpositionEquiv k n) (coordinate k n i) = MulOpposite.op (coordinate k n i)
            source
            theorem Stafford38.WeylTransposition.transpositionEquiv_momentum (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
            (transpositionEquiv k n) (momentum k n i) = MulOpposite.op (-momentum k n i)
            source
            theorem Stafford38.WeylTransposition.transpositionEquiv_injective (k : Type u) [Field k] (n : ℕ) :
            Function.Injective ⇑(transpositionEquiv k n)
            source
            theorem Stafford38.WeylTransposition.transpositionEquiv_surjective (k : Type u) [Field k] (n : ℕ) :
            Function.Surjective ⇑(transpositionEquiv k n)
            source
            def Stafford38.WeylTransposition.transpose (k : Type u) [Field k] (n : ℕ) (a : WeylIteratedEquivalence.PresentedWeyl k n) :
            WeylIteratedEquivalence.PresentedWeyl k n

            The usual unbundled anti-automorphism underlying transpositionEquiv.

            Equations
            Instances For
              source
              @[simp]
              theorem Stafford38.WeylTransposition.transpose_coordinate (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
              transpose k n (coordinate k n i) = coordinate k n i
              source
              @[simp]
              theorem Stafford38.WeylTransposition.transpose_momentum (k : Type u) [Field k] (n : ℕ) (i : Fin n) :
              transpose k n (momentum k n i) = -momentum k n i
              source
              @[simp]
              theorem Stafford38.WeylTransposition.transpose_algebraMap (k : Type u) [Field k] (n : ℕ) (c : k) :
              transpose k n ((algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)) c) = (algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)) c
              source
              theorem Stafford38.WeylTransposition.transpose_mul (k : Type u) [Field k] (n : ℕ) (a b : WeylIteratedEquivalence.PresentedWeyl k n) :
              transpose k n (a * b) = transpose k n b * transpose k n a
              source
              @[simp]
              theorem Stafford38.WeylTransposition.transpose_transpose (k : Type u) [Field k] (n : ℕ) (a : WeylIteratedEquivalence.PresentedWeyl k n) :
              transpose k n (transpose k n a) = a
              source
              theorem Stafford38.WeylTransposition.transpose_injective (k : Type u) [Field k] (n : ℕ) :
              Function.Injective (transpose k n)
              source
              @[instance_reducible]
              def Stafford38.WeylTransposition.transposedLeftModule (k : Type u) [Field k] (n : ℕ) (M : Type v) [AddCommMonoid M] [Module (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ M] :
              Module (WeylIteratedEquivalence.PresentedWeyl k n) M

              A right PresentedWeyl-module becomes a left module by restriction of scalars along transposition.

              Equations
              Instances For
                source
                theorem Stafford38.WeylTransposition.transposedLeftModule_smul (k : Type u) [Field k] (n : ℕ) (M : Type v) [AddCommMonoid M] [Module (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ M] (a : WeylIteratedEquivalence.PresentedWeyl k n) (m : M) :
                SMul.smul a m = (transpositionEquiv k n) a • m
                source
                theorem Stafford38.WeylTransposition.transposedLeftModule_coordinate_smul (k : Type u) [Field k] (n : ℕ) (M : Type v) [AddCommMonoid M] [Module (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ M] (i : Fin n) (m : M) :
                SMul.smul (coordinate k n i) m = MulOpposite.op (coordinate k n i) • m
                source
                theorem Stafford38.WeylTransposition.transposedLeftModule_momentum_smul (k : Type u) [Field k] (n : ℕ) (M : Type v) [AddCommMonoid M] [Module (WeylIteratedEquivalence.PresentedWeyl k n)ᵐᵒᵖ M] (i : Fin n) (m : M) :
                SMul.smul (momentum k n i) m = MulOpposite.op (-momentum k n i) • m