Documentation

LeanPool.Stafford38.AlgebraicAnalysis.Ore.Associativity

Associativity of derivation Ore normal forms over a noncommutative ring #

This removes the commutativity assumption from the faithful-operator proof of associativity for Stafford.OreDivision.rightMul.

source
theorem AlgebraicAnalysis.OreAssociativity.derivation_one {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
D.toFun 1 = 0
source
noncomputable def AlgebraicAnalysis.OreAssociativity.coefficientDerivation {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
Polynomial B →+ Polynomial B

Apply the coefficient derivation to every coefficient.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicAnalysis.OreAssociativity.coefficientDerivation_monomial {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (i : ℕ) (b : B) :
    (coefficientDerivation D) ((Polynomial.monomial i) b) = (Polynomial.monomial i) (D.toFun b)
    source
    @[simp]
    theorem AlgebraicAnalysis.OreAssociativity.coefficientDerivation_C_mul {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) (p : Polynomial B) :
    (coefficientDerivation D) (Polynomial.C b * p) = Polynomial.C b * (coefficientDerivation D) p + Polynomial.C (D.toFun b) * p
    source
    noncomputable def AlgebraicAnalysis.OreAssociativity.coefficientLeft {B : Type u_1} [Ring B] :
    B →+* AddMonoid.End (Polynomial B)

    Coefficients act by ordinary left multiplication.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicAnalysis.OreAssociativity.leftOreShift {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
      AddMonoid.End (Polynomial B)

      Left multiplication by the Ore variable on normal forms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def AlgebraicAnalysis.OreAssociativity.faithfulAmbient {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
        OreDivision.OreAmbient B (AddMonoid.End (Polynomial B)) D

        The faithful left-regular representation of the one-variable Ore model.

        Equations
        Instances For
          source
          @[simp]
          theorem AlgebraicAnalysis.OreAssociativity.coefficientDerivation_X_pow {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) :
          (coefficientDerivation D) (Polynomial.X ^ n) = 0
          source
          @[simp]
          theorem AlgebraicAnalysis.OreAssociativity.leftOreShift_X_pow {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) :
          (leftOreShift D) (Polynomial.X ^ n) = Polynomial.X ^ (n + 1)
          source
          theorem AlgebraicAnalysis.OreAssociativity.leftOreShift_pow_apply_one {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) :
          (leftOreShift D ^ n) 1 = Polynomial.X ^ n
          source
          theorem AlgebraicAnalysis.OreAssociativity.faithful_eval_apply_one {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) :
          (OreDivision.OreAmbient.eval D (faithfulAmbient D) p) 1 = p
          source
          theorem AlgebraicAnalysis.OreAssociativity.faithful_eval_injective {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
          Function.Injective (OreDivision.OreAmbient.eval D (faithfulAmbient D))
          source
          theorem AlgebraicAnalysis.OreAssociativity.faithful_eval_one {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
          OreDivision.OreAmbient.eval D (faithfulAmbient D) 1 = 1
          source
          theorem AlgebraicAnalysis.OreAssociativity.faithful_eval_C {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) :
          OreDivision.OreAmbient.eval D (faithfulAmbient D) (Polynomial.C b) = coefficientLeft b
          source
          theorem AlgebraicAnalysis.OreAssociativity.faithful_eval_X {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
          OreDivision.OreAmbient.eval D (faithfulAmbient D) Polynomial.X = leftOreShift D
          source
          theorem AlgebraicAnalysis.OreAssociativity.rightMul_assoc_of_ring {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p q r : Polynomial B) :
          OreDivision.rightMul D (OreDivision.rightMul D p q) r = OreDivision.rightMul D p (OreDivision.rightMul D q r)

          Associativity of the derivation-corrected normal-form product.

          The concrete associative Ore ring #

          source
          def AlgebraicAnalysis.OreAssociativity.faithfulRange {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
          Subring (AddMonoid.End (Polynomial B))

          The image of the faithful normal-form representation.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible, inline]
            abbrev AlgebraicAnalysis.OreAssociativity.NormalOre {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
            Subring (AddMonoid.End (Polynomial B))

            The one-variable derivation Ore extension, represented faithfully by its left-regular action on normal polynomials.

            Equations
            Instances For
              source
              noncomputable def AlgebraicAnalysis.OreAssociativity.normalForm {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) :
              ↥(NormalOre D)

              A coefficient-left polynomial regarded as an element of the Ore ring.

              Equations
              Instances For
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_injective {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                Function.Injective (normalForm D)
                source
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_surjective {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                Function.Surjective (normalForm D)
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_zero {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                normalForm D 0 = 0
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_one {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                normalForm D 1 = 1
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_add {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p q : Polynomial B) :
                normalForm D (p + q) = normalForm D p + normalForm D q
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_neg {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p : Polynomial B) :
                normalForm D (-p) = -normalForm D p
                source
                @[simp]
                theorem AlgebraicAnalysis.OreAssociativity.normalForm_mul {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (p q : Polynomial B) :
                normalForm D (OreDivision.rightMul D p q) = normalForm D p * normalForm D q
                source
                noncomputable def AlgebraicAnalysis.OreAssociativity.normalFormAddHom {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                Polynomial B →+ ↥(NormalOre D)

                The normal-form map as an additive homomorphism.

                Equations
                Instances For
                  source
                  noncomputable def AlgebraicAnalysis.OreAssociativity.normalFormAddEquiv {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                  Polynomial B ≃+ ↥(NormalOre D)

                  Normal forms are additively equivalent to ordinary coefficient-left polynomials.

                  Equations
                  Instances For
                    source
                    noncomputable def AlgebraicAnalysis.OreAssociativity.normalCoefficient {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                    B →+* ↥(NormalOre D)

                    The canonical coefficient embedding.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem AlgebraicAnalysis.OreAssociativity.normalForm_C {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) :
                      normalForm D (Polynomial.C b) = (normalCoefficient D) b
                      source
                      noncomputable def AlgebraicAnalysis.OreAssociativity.normalVariable {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) :
                      ↥(NormalOre D)

                      The canonical Ore variable.

                      Equations
                      Instances For
                        source
                        theorem AlgebraicAnalysis.OreAssociativity.normalForm_monomial {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (n : ℕ) (b : B) :
                        normalForm D ((Polynomial.monomial n) b) = (normalCoefficient D) b * normalVariable D ^ n
                        source
                        theorem AlgebraicAnalysis.OreAssociativity.normalVariable_mul_coefficient {B : Type u_1} [Ring B] (D : OreDivisionDerivation B) (b : B) :
                        normalVariable D * (normalCoefficient D) b = (normalCoefficient D) b * normalVariable D + (normalCoefficient D) (D.toFun b)

                        The defining derivation relation X b = b X + D(b).

                        Universal property #

                        source
                        theorem AlgebraicAnalysis.OreAssociativity.ambient_eval_one {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) :
                        OreDivision.OreAmbient.eval D O 1 = 1
                        source
                        theorem AlgebraicAnalysis.OreAssociativity.ambient_eval_C {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) (b : B) :
                        OreDivision.OreAmbient.eval D O (Polynomial.C b) = O.embed b
                        source
                        theorem AlgebraicAnalysis.OreAssociativity.ambient_eval_X {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) :
                        OreDivision.OreAmbient.eval D O Polynomial.X = O.x
                        source
                        noncomputable def AlgebraicAnalysis.OreAssociativity.oreLift {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) :
                        ↥(NormalOre D) →+* A

                        The universal map out of the concrete Ore ring.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem AlgebraicAnalysis.OreAssociativity.oreLift_normalForm {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) (p : Polynomial B) :
                          (oreLift D O) (normalForm D p) = OreDivision.OreAmbient.eval D O p
                          source
                          @[simp]
                          theorem AlgebraicAnalysis.OreAssociativity.oreLift_coefficient {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) (b : B) :
                          (oreLift D O) ((normalCoefficient D) b) = O.embed b
                          source
                          @[simp]
                          theorem AlgebraicAnalysis.OreAssociativity.oreLift_variable {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) :
                          (oreLift D O) (normalVariable D) = O.x
                          source
                          theorem AlgebraicAnalysis.OreAssociativity.oreLift_unique {B : Type u_1} [Ring B] {A : Type u_2} [Ring A] (D : OreDivisionDerivation B) (O : OreDivision.OreAmbient B A D) (g : ↥(NormalOre D) →+* A) (hCoefficient : ∀ (b : B), g ((normalCoefficient D) b) = O.embed b) (hVariable : g (normalVariable D) = O.x) :
                          g = oreLift D O

                          A ring map out of NormalOre D is uniquely determined by the coefficient map and the image of the Ore variable.