Documentation

LeanPool.Stafford38.AlgebraicAnalysis.DifferentialOperators.Basic

Finite-order differential operators #

Neutral extraction of the intrinsic finite-order differential-operator algebra from Stafford38 commit 1585e4c7, originally Stafford38/DifferentialOperators.lean. No Weyl presentation or application-specific hypothesis is used.

source
@[reducible, inline]
abbrev AlgebraicAnalysis.DifferentialOperators.End {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] :
Type u_2

k-linear endomorphisms of the k-algebra R.

Equations
Instances For
    source
    def AlgebraicAnalysis.DifferentialOperators.multiplication {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (a : R) :
    End

    Multiplication by an element of R, as a k-linear endomorphism.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicAnalysis.DifferentialOperators.multiplication_apply {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (a x : R) :
      (multiplication a) x = a * x
      source
      def AlgebraicAnalysis.DifferentialOperators.commutator {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) (a : R) :
      End

      The commutator of an endomorphism with multiplication by a.

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicAnalysis.DifferentialOperators.commutator_apply {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) (a x : R) :
        (commutator P a) x = P (a * x) - a * P x
        source
        def AlgebraicAnalysis.DifferentialOperators.order {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] :
        ℕ → Submodule k End

        Differential operators of order at most n.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem AlgebraicAnalysis.DifferentialOperators.mem_order_zero_iff {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) :
          P ∈ order 0 ↔ ∀ (a : R), commutator P a = 0
          source
          @[simp]
          theorem AlgebraicAnalysis.DifferentialOperators.mem_order_succ_iff {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) (n : ℕ) :
          P ∈ order (n + 1) ↔ ∀ (a : R), commutator P a ∈ order n
          source
          theorem AlgebraicAnalysis.DifferentialOperators.mem_order_zero_iff_eq_multiplication {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) :
          P ∈ order 0 ↔ P = multiplication (P 1)
          source
          theorem AlgebraicAnalysis.DifferentialOperators.order_mono_step {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (n : ℕ) :
          order n ≤ order (n + 1)
          source
          theorem AlgebraicAnalysis.DifferentialOperators.order_mono {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {m n : ℕ} (h : m ≤ n) :
          order m ≤ order n
          source
          theorem AlgebraicAnalysis.DifferentialOperators.commutator_mul {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P Q : End) (a : R) :
          commutator (P * Q) a = P * commutator Q a + commutator P a * Q
          source
          theorem AlgebraicAnalysis.DifferentialOperators.mul_mem_order {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] {P Q : End} {m n : ℕ} (hP : P ∈ order m) (hQ : Q ∈ order n) :
          P * Q ∈ order (m + n)

          Orders add under composition.

          source
          def AlgebraicAnalysis.DifferentialOperators.algebra {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] :
          Subalgebra k End

          The algebra of all finite-order k-linear differential operators on R.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem AlgebraicAnalysis.DifferentialOperators.mem_algebra_iff {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (P : End) :
            P ∈ algebra ↔ ∃ (n : ℕ), P ∈ order n

            The two basic kinds of operators are finite-order without any geometric assumption. Keeping these witnesses public lets a concrete carrier expose its coefficient and derivation generators through this neutral API.

            source
            theorem AlgebraicAnalysis.DifferentialOperators.multiplication_mem_algebra {k : Type u_1} {R : Type u_2} [CommRing k] [CommRing R] [Algebra k R] (a : R) :
            multiplication a ∈ algebra

            Multiplication by a coefficient is an intrinsic differential operator of order zero.