Documentation

LeanPool.Stafford38.Stafford38.Characteristic.CanonicalTangentialPageOperators

Tangential filtered operators on the canonical quotient #

Right multiplication by every tangential Weyl generator gives an actual filtered operator on the canonical quotient. The distinguished coordinate commutes with these operators, so they induce operators on every page.

source
@[reducible, inline]
abbrev Stafford38.Characteristic.CanonicalTangentialPageOperators.CanonicalIdeal (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) :
EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k (n + 1))

The canonical right ideal in the presented Weyl algebra.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev Stafford38.Characteristic.CanonicalTangentialPageOperators.CanonicalComplex (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) :
    FilteredTwoTermPages.FilteredTwoTerm k (CanonicalFilteredTwoTerm.CanonicalQuotient k n N d)

    The canonical filtered two-term complex associated with the Weyl element.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Stafford38.Characteristic.CanonicalTangentialPageOperators.PageOperator (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (e : ℤ) :
      Type u

      A filtered page operator on the canonical two-term complex for the Weyl element.

      Equations
      Instances For
        source
        def Stafford38.Characteristic.CanonicalTangentialPageOperators.tangentialPageOperator (k : Type u) [Field k] (n N : ℕ) (d a : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (e : ℕ) (ha : a ∈ WeylFiltration.orderPiece k (n + 1) e) (hax : a * WeylIteratedEquivalence.presentedCoordinate k n = WeylIteratedEquivalence.presentedCoordinate k n * a) :
        PageOperator k n N d ↑e

        Right multiplication by a symbol of bounded order, packaged as a filtered page operator.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Stafford38.Characteristic.CanonicalTangentialPageOperators.tangentialCoordinatePageOperator (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (i : Fin n) :
          PageOperator k n N d 0

          The degree-zero page operator induced by a tangential position generator.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Stafford38.Characteristic.CanonicalTangentialPageOperators.tangentialMomentumPageOperator (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (i : Fin n) :
            PageOperator k n N d 1

            The degree-one page operator induced by a tangential momentum generator.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Stafford38.Characteristic.CanonicalTangentialPageOperators.tangentialDegree {n : ℕ} :
              Fin n ⊕ Fin n → ℕ

              The order degree of a tangential generator: zero for positions and one for momenta.

              Equations
              Instances For
                source
                theorem Stafford38.Characteristic.CanonicalTangentialPageOperators.tangential_commutator_lower (k : Type u) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (i j : Fin n ⊕ Fin n) (p : ℤ) (z : CanonicalFilteredTwoTerm.CanonicalQuotient k n N d) (hz : z ∈ (CanonicalComplex k n N d).G p) :
                (CanonicalFilteredTwoTerm.rightMulLinearMap k (CanonicalIdeal k n N d) (WeylIteratedEquivalence.oldGenerator k n i)) ((CanonicalFilteredTwoTerm.rightMulLinearMap k (CanonicalIdeal k n N d) (WeylIteratedEquivalence.oldGenerator k n j)) z) - (CanonicalFilteredTwoTerm.rightMulLinearMap k (CanonicalIdeal k n N d) (WeylIteratedEquivalence.oldGenerator k n j)) ((CanonicalFilteredTwoTerm.rightMulLinearMap k (CanonicalIdeal k n N d) (WeylIteratedEquivalence.oldGenerator k n i)) z) ∈ (CanonicalComplex k n N d).G (p - (↑(tangentialDegree i) + ↑(tangentialDegree j)) + 1)