Ore extensions by a skew derivation

This file constructs the Ore extension associated to an algebra endomorphism σ and a σ-derivation δ. Its elements are finitely supported left-coefficient sequences ∑ i, aᵢ Xⁱ, and multiplication is characterized by

X * C a = C (σ a) * X + C (δ a).

The direct finitely supported model makes the left monomials a basis without any injectivity assumption on σ. Multiplication is constructed through the faithful action on the same free module: C a acts coefficientwise on the left, while X sends a Xⁿ to σ(a) Xⁿ⁺¹ + δ(a) Xⁿ.

Main definitions

• TauCeti.SigmaDerivation: a linear map satisfying the skew Leibniz rule.
• TauCeti.OreExtension: the associated Ore extension with left coefficients.
• TauCeti.OreExtension.C and TauCeti.OreExtension.X: its constants and variable.
• TauCeti.OreExtension.monomialBasis: the left monomial basis Xⁿ over R.
• TauCeti.OreExtension.CRingHom and TauCeti.OreExtension.CAlgHom: the inclusion of the coefficients as a ring and as a k-algebra homomorphism.
• TauCeti.OreExtension.eval₂: evaluation along a coefficient homomorphism at a chosen element.
• TauCeti.OreExtension.lift and TauCeti.OreExtension.liftAlgHom: the universal ring and k-algebra homomorphisms out of the Ore extension.
• TauCeti.OreExtension.mapAlgHom and TauCeti.OreExtension.mapAlgEquiv: the algebra homomorphisms and equivalences induced by coefficient maps intertwining the twists and the skew derivations.

Main statements

• TauCeti.OreExtension.X_mul_C: the Ore commutation relation.
• TauCeti.OreExtension.coeff_X_mul_zero and coeff_X_mul_succ: the coefficient recursion for left multiplication by the variable.
• TauCeti.OreExtension.sum_monomial_eq: the left-coefficient expansion.
• TauCeti.OreExtension.lift_C, TauCeti.OreExtension.lift_X, and TauCeti.OreExtension.ringHom_ext: the universal property for ring homomorphisms.
• TauCeti.OreExtension.liftAlgHom_C, TauCeti.OreExtension.liftAlgHom_X, and TauCeti.OreExtension.algHom_ext: the universal property for k-algebra homomorphisms.

References

• P. M. Cohn, Free Rings and Their Relations, second edition, Chapter 2.
• The finitely supported normal-form design follows Mathlib's SkewPolynomial; the extra degree-preserving term implements the skew derivation.

structure TauCeti.SigmaDerivation {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] (σ : R →ₐ[k] R) extends R →ₗ[k] R : Type v

A σ-derivation is a linear map satisfying δ (a * b) = σ a * δ b + δ a * b and sending one to zero.

• toFun : R → R
• map_add' (x y : R) : self.toFun (x + y) = self.toFun x + self.toFun y
• map_smul' (m : k) (x : R) : self.toFun (m • x) = (RingHom.id k) m • self.toFun x
• leibniz' (a b : R) : self.toLinearMap (a * b) = σ a * self.toLinearMap b + self.toLinearMap a * b

  The skew Leibniz rule.

• map_one' : self.toLinearMap 1 = 0

  A skew derivation sends one to zero.

@[instance_reducible]

instance TauCeti.SigmaDerivation.instZero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} : Zero (SigmaDerivation σ)

@[instance_reducible]

instance TauCeti.SigmaDerivation.instFunLike {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} : FunLike (SigmaDerivation σ) R R

instance TauCeti.SigmaDerivation.instLinearMapClass {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} : LinearMapClass (SigmaDerivation σ) k R R

theorem TauCeti.SigmaDerivation.ext {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ ε : SigmaDerivation σ} (h : ∀ (a : R), δ a = ε a) : δ = ε

Two skew derivations are equal when they agree at every point.

theorem TauCeti.SigmaDerivation.ext_iff {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ ε : SigmaDerivation σ} : δ = ε ↔ ∀ (a : R), δ a = ε a

@[simp]

theorem TauCeti.SigmaDerivation.coe_toLinearMap {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} (δ : SigmaDerivation σ) : ⇑δ.toLinearMap = ⇑δ

@[simp]

theorem TauCeti.SigmaDerivation.coe_zero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} : ⇑0 = 0

theorem TauCeti.SigmaDerivation.leibniz {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} (δ : SigmaDerivation σ) (a b : R) : δ (a * b) = σ a * δ b + δ a * b

The skew Leibniz rule.

@[simp]

theorem TauCeti.SigmaDerivation.map_one {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} (δ : SigmaDerivation σ) : δ 1 = 0

A skew derivation sends one to zero.

structure TauCeti.OreExtension {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] (σ : R →ₐ[k] R) (δ : SigmaDerivation σ) : Type v

The Ore extension R[X; σ, δ], represented by its finitely supported left coefficients.

• ofFinsupp :: (
• toFinsupp : ℕ →₀ R

  The finitely supported sequence of left coefficients.

• )

theorem TauCeti.OreExtension.toFinsupp_injective {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Function.Injective toFinsupp

def TauCeti.OreExtension.coeff {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (n : ℕ) : R

The coefficient of Xⁿ in an Ore polynomial.

theorem TauCeti.OreExtension.coeff_def {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (n : ℕ) : p.coeff n = p.toFinsupp n

theorem TauCeti.OreExtension.ext {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p q : OreExtension σ δ} (h : ∀ (n : ℕ), p.coeff n = q.coeff n) : p = q

Ore polynomials are equal when all their left coefficients agree.

theorem TauCeti.OreExtension.ext_iff {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {p q : OreExtension σ δ} : p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

@[instance_reducible]

instance TauCeti.OreExtension.instZero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Zero (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instAdd {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Add (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instNSMul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : SMul ℕ (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.smulZeroClass {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [SMulZeroClass S R] : SMulZeroClass S (OreExtension σ δ)

@[simp]

theorem TauCeti.OreExtension.toFinsupp_zero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : toFinsupp 0 = 0

@[simp]

theorem TauCeti.OreExtension.ofFinsupp_zero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : { toFinsupp := 0 } = 0

@[simp]

theorem TauCeti.OreExtension.toFinsupp_add {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p q : OreExtension σ δ) : (p + q).toFinsupp = p.toFinsupp + q.toFinsupp

@[simp]

theorem TauCeti.OreExtension.toFinsupp_nsmul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (n : ℕ) : (n • p).toFinsupp = n • p.toFinsupp

@[simp]

theorem TauCeti.OreExtension.toFinsupp_smul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [SMulZeroClass S R] (s : S) (p : OreExtension σ δ) : (s • p).toFinsupp = s • p.toFinsupp

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instAddCommMonoid {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : AddCommMonoid (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.module {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] [Module S R] : Module S (OreExtension σ δ)

instance TauCeti.OreExtension.smulCommClass {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S₁ : Type u_1} {S₂ : Type u_2} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] : SMulCommClass S₁ S₂ (OreExtension σ δ)

instance TauCeti.OreExtension.isScalarTower {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S₁ : Type u_1} {S₂ : Type u_2} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] : IsScalarTower S₁ S₂ (OreExtension σ δ)

def TauCeti.OreExtension.leftCoeffLinearEquiv {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : OreExtension σ δ ≃ₗ[R] ℕ →₀ R

The linear equivalence recording the left coefficients of an Ore polynomial.

@[simp]

theorem TauCeti.OreExtension.leftCoeffLinearEquiv_apply {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : leftCoeffLinearEquiv p = p.toFinsupp

@[simp]

theorem TauCeti.OreExtension.leftCoeffLinearEquiv_symm_apply {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (f : ℕ →₀ R) : leftCoeffLinearEquiv.symm f = { toFinsupp := f }

instance TauCeti.OreExtension.instNontrivial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} [Nontrivial R] : Nontrivial (OreExtension σ δ)

noncomputable def TauCeti.OreExtension.monomialBasis {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Module.Basis ℕ R (OreExtension σ δ)

The left monomial basis of an Ore extension.

@[simp]

theorem TauCeti.OreExtension.monomialBasis_repr {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : monomialBasis.repr p = p.toFinsupp

noncomputable def TauCeti.OreExtension.monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : R →ₗ[k] OreExtension σ δ

The left-coefficient monomial a Xⁿ.

@[simp]

theorem TauCeti.OreExtension.toFinsupp_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (a : R) : ((monomial n) a).toFinsupp = Finsupp.single n a

theorem TauCeti.OreExtension.induction_on {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {P : OreExtension σ δ → Prop} (p : OreExtension σ δ) (zero : P 0) (add : ∀ (n : ℕ) (a : R) (p : OreExtension σ δ), n ∉ p.toFinsupp.support → a ≠ 0 → P p → P ((monomial n) a + p)) : P p

Induction on an Ore polynomial by adjoining one left monomial at a time.

@[simp]

theorem TauCeti.OreExtension.coeff_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (m : ℕ) (a : R) (n : ℕ) : ((monomial m) a).coeff n = if m = n then a else 0

theorem TauCeti.OreExtension.monomial_injective {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : Function.Injective ⇑(monomial n)

@[simp]

theorem TauCeti.OreExtension.monomialBasis_apply {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : monomialBasis n = (monomial n) 1

@[simp]

theorem TauCeti.OreExtension.coeff_zero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : coeff 0 n = 0

@[simp]

theorem TauCeti.OreExtension.coeff_add {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p q : OreExtension σ δ) (n : ℕ) : (p + q).coeff n = p.coeff n + q.coeff n

@[simp]

theorem TauCeti.OreExtension.coeff_smul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [SMulZeroClass S R] (s : S) (p : OreExtension σ δ) (n : ℕ) : (s • p).coeff n = s • p.coeff n

@[simp]

theorem TauCeti.OreExtension.smul_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [SMulZeroClass S R] (s : S) (n : ℕ) (a : R) : s • (monomial n) a = (monomial n) (s • a)

@[simp]

theorem TauCeti.OreExtension.finsetSum_coeff {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {ι : Type u_1} (s : Finset ι) (p : ι → OreExtension σ δ) (n : ℕ) : (∑ i ∈ s, p i).coeff n = ∑ i ∈ s, (p i).coeff n

Coefficients commute with finite sums.

theorem TauCeti.OreExtension.sum_monomial_eq {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : ∑ n ∈ p.toFinsupp.support, (monomial n) (p.coeff n) = p

Every Ore polynomial is the sum of its left-coefficient monomials.

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instMul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Mul (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instNonUnitalNonAssocSemiring {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : NonUnitalNonAssocSemiring (OreExtension σ δ)

noncomputable def TauCeti.OreExtension.C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : R →ₗ[k] OreExtension σ δ

The constant Ore polynomial.

noncomputable def TauCeti.OreExtension.X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : OreExtension σ δ

The Ore variable.

@[simp]

theorem TauCeti.OreExtension.monomial_zero_left {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : (monomial 0) a = C a

theorem TauCeti.OreExtension.X_eq_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : X = (monomial 1) 1

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instOne {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : One (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instNatCast {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : NatCast (OreExtension σ δ)

@[simp]

theorem TauCeti.OreExtension.toFinsupp_one {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : toFinsupp 1 = Finsupp.single 0 1

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instNonUnitalSemiring {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : NonUnitalSemiring (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instNonAssocSemiring {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : NonAssocSemiring (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instSemiring {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Semiring (OreExtension σ δ)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instAlgebra {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Algebra k (OreExtension σ δ)

@[simp]

theorem TauCeti.OreExtension.C_one {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : C 1 = 1

@[simp]

theorem TauCeti.OreExtension.algebraMap_apply {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (c : k) : (algebraMap k (OreExtension σ δ)) c = C ((algebraMap k R) c)

@[simp]

theorem TauCeti.OreExtension.C_mul_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a b : R) (n : ℕ) : C a * (monomial n) b = (monomial n) (a * b)

@[simp]

theorem TauCeti.OreExtension.C_mul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a b : R) : C (a * b) = C a * C b

theorem TauCeti.OreExtension.smul_eq_C_mul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) (p : OreExtension σ δ) : a • p = C a * p

@[simp]

theorem TauCeti.OreExtension.coeff_C_mul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) (p : OreExtension σ δ) (n : ℕ) : (C a * p).coeff n = a * p.coeff n

noncomputable def TauCeti.OreExtension.CRingHom {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : R →+* OreExtension σ δ

Constants embed into the Ore extension as a ring homomorphism.

@[simp]

theorem TauCeti.OreExtension.CRingHom_eq_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : CRingHom a = C a

theorem TauCeti.OreExtension.CRingHom_injective {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : Function.Injective ⇑CRingHom

noncomputable def TauCeti.OreExtension.CAlgHom {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} : R →ₐ[k] OreExtension σ δ

Constants embed into the Ore extension as a k-algebra homomorphism.

@[simp]

theorem TauCeti.OreExtension.CAlgHom_eq_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : CAlgHom a = C a

@[simp]

theorem TauCeti.OreExtension.coeff_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) (n : ℕ) : (C a).coeff n = if n = 0 then a else 0

@[simp]

theorem TauCeti.OreExtension.coeff_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : X.coeff n = if n = 1 then 1 else 0

theorem TauCeti.OreExtension.X_mul_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) : X * C a = C (σ a) * X + C (δ a)

The defining Ore commutation relation.

theorem TauCeti.OreExtension.X_pow_eq_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) : X ^ n = (monomial n) 1

@[simp]

theorem TauCeti.OreExtension.C_mul_X_pow_eq_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (a : R) (n : ℕ) : C a * X ^ n = (monomial n) a

theorem TauCeti.OreExtension.induction_on_mul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {P : OreExtension σ δ → Prop} (p : OreExtension σ δ) (C : ∀ (a : R), P (C a)) (X : P X) (add : ∀ (p q : OreExtension σ δ), P p → P q → P (p + q)) (mul : ∀ (p q : OreExtension σ δ), P p → P q → P (p * q)) : P p

Induction on an Ore polynomial through the constants, the variable, sums and products.

@[simp]

theorem TauCeti.OreExtension.X_mul_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (n : ℕ) (a : R) : X * (monomial n) a = (monomial (n + 1)) (σ a) + (monomial n) (δ a)

Multiplication by the variable has the skew-derivation coefficient recursion.

@[simp]

theorem TauCeti.OreExtension.coeff_X_mul_zero {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) : (X * p).coeff 0 = δ (p.coeff 0)

The constant coefficient of left multiplication by the variable.

@[simp]

theorem TauCeti.OreExtension.coeff_X_mul_succ {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} (p : OreExtension σ δ) (n : ℕ) : (X * p).coeff (n + 1) = σ (p.coeff n) + δ (p.coeff (n + 1))

The positive-degree coefficients of left multiplication by the variable.

noncomputable def TauCeti.OreExtension.eval₂ {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) : OreExtension σ δ →+ S

Evaluate an Ore polynomial along a coefficient homomorphism f at an element x, without yet assuming that x satisfies the Ore commutation relation.

@[simp]

theorem TauCeti.OreExtension.eval₂_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (n : ℕ) (a : R) : (eval₂ f x) ((monomial n) a) = f a * x ^ n

theorem TauCeti.OreExtension.eval₂_mul {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) (p q : OreExtension σ δ) : (eval₂ f x) (p * q) = (eval₂ f x) p * (eval₂ f x) q

Evaluation is multiplicative when the chosen image of X satisfies the Ore relation.

noncomputable def TauCeti.OreExtension.lift {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) : OreExtension σ δ →+* S

The universal map from an Ore extension. The chosen image x of the variable must satisfy the defining Ore commutation relation with every coefficient.

theorem TauCeti.OreExtension.lift_apply {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) (p : OreExtension σ δ) : (lift f x h) p = (eval₂ f x) p

@[simp]

theorem TauCeti.OreExtension.lift_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) (a : R) : (lift f x h) (C a) = f a

@[simp]

theorem TauCeti.OreExtension.lift_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] (f : R →+* S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) : (lift f x h) X = x

theorem TauCeti.OreExtension.ringHom_ext {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] {f g : OreExtension σ δ →+* S} (hC : ∀ (a : R), f (C a) = g (C a)) (hX : f X = g X) : f = g

A ring homomorphism from an Ore extension is determined by its values on the coefficients and the Ore variable.

noncomputable def TauCeti.OreExtension.liftAlgHom {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] [Algebra k S] (f : R →ₐ[k] S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) : OreExtension σ δ →ₐ[k] S

The universal k-algebra map from an Ore extension. The chosen image x of the variable must satisfy the defining Ore commutation relation with every coefficient.

@[simp]

theorem TauCeti.OreExtension.liftAlgHom_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] [Algebra k S] (f : R →ₐ[k] S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) (a : R) : (liftAlgHom f x h) (C a) = f a

@[simp]

theorem TauCeti.OreExtension.liftAlgHom_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] [Algebra k S] (f : R →ₐ[k] S) (x : S) (h : ∀ (a : R), x * f a = f (σ a) * x + f (δ a)) : (liftAlgHom f x h) X = x

theorem TauCeti.OreExtension.algHom_ext {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {S : Type u_1} [Semiring S] [Algebra k S] {f g : OreExtension σ δ →ₐ[k] S} (hC : ∀ (a : R), f (C a) = g (C a)) (hX : f X = g X) : f = g

A k-algebra homomorphism from an Ore extension is determined by its values on the coefficients and the Ore variable.

noncomputable def TauCeti.OreExtension.mapAlgHom {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (f : R →ₐ[k] R') (hσ : ∀ (a : R), f (σ a) = σ' (f a)) (hδ : ∀ (a : R), f (δ a) = δ' (f a)) : OreExtension σ δ →ₐ[k] OreExtension σ' δ'

An algebra map of coefficients intertwining the twists and the skew derivations induces a k-algebra map of Ore extensions, which is f on the coefficients and fixes the variable.

@[simp]

theorem TauCeti.OreExtension.mapAlgHom_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (f : R →ₐ[k] R') (hσ : ∀ (a : R), f (σ a) = σ' (f a)) (hδ : ∀ (a : R), f (δ a) = δ' (f a)) (a : R) : (mapAlgHom f hσ hδ) (C a) = C (f a)

@[simp]

theorem TauCeti.OreExtension.mapAlgHom_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (f : R →ₐ[k] R') (hσ : ∀ (a : R), f (σ a) = σ' (f a)) (hδ : ∀ (a : R), f (δ a) = δ' (f a)) : (mapAlgHom f hσ hδ) X = X

@[simp]

theorem TauCeti.OreExtension.mapAlgHom_monomial {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (f : R →ₐ[k] R') (hσ : ∀ (a : R), f (σ a) = σ' (f a)) (hδ : ∀ (a : R), f (δ a) = δ' (f a)) (n : ℕ) (a : R) : (mapAlgHom f hσ hδ) ((monomial n) a) = (monomial n) (f a)

noncomputable def TauCeti.OreExtension.mapAlgEquiv {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (e : R ≃ₐ[k] R') (hσ : ∀ (a : R), e (σ a) = σ' (e a)) (hδ : ∀ (a : R), e (δ a) = δ' (e a)) : OreExtension σ δ ≃ₐ[k] OreExtension σ' δ'

An algebra equivalence of coefficients intertwining the twists and the skew derivations induces a k-algebra equivalence of Ore extensions, which is e on the coefficients and fixes the variable.

@[simp]

theorem TauCeti.OreExtension.mapAlgEquiv_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (e : R ≃ₐ[k] R') (hσ : ∀ (a : R), e (σ a) = σ' (e a)) (hδ : ∀ (a : R), e (δ a) = δ' (e a)) (a : R) : (mapAlgEquiv e hσ hδ) (C a) = C (e a)

@[simp]

theorem TauCeti.OreExtension.mapAlgEquiv_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (e : R ≃ₐ[k] R') (hσ : ∀ (a : R), e (σ a) = σ' (e a)) (hδ : ∀ (a : R), e (δ a) = δ' (e a)) : (mapAlgEquiv e hσ hδ) X = X

@[simp]

theorem TauCeti.OreExtension.mapAlgEquiv_symm_C {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (e : R ≃ₐ[k] R') (hσ : ∀ (a : R), e (σ a) = σ' (e a)) (hδ : ∀ (a : R), e (δ a) = δ' (e a)) (b : R') : (mapAlgEquiv e hσ hδ).symm (C b) = C (e.symm b)

@[simp]

theorem TauCeti.OreExtension.mapAlgEquiv_symm_X {k : Type u} {R : Type v} [CommSemiring k] [Semiring R] [Algebra k R] {σ : R →ₐ[k] R} {δ : SigmaDerivation σ} {R' : Type u_1} [Semiring R'] [Algebra k R'] {σ' : R' →ₐ[k] R'} {δ' : SigmaDerivation σ'} (e : R ≃ₐ[k] R') (hσ : ∀ (a : R), e (σ a) = σ' (e a)) (hδ : ∀ (a : R), e (δ a) = δ' (e a)) : (mapAlgEquiv e hσ hδ).symm X = X

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instAddCommGroup {k : Type u} [CommSemiring k] {S : Type u_1} [Ring S] [Algebra k S] {τ : S →ₐ[k] S} {ε : SigmaDerivation τ} : AddCommGroup (OreExtension τ ε)

@[instance_reducible]

noncomputable instance TauCeti.OreExtension.instRing {k : Type u} [CommSemiring k] {S : Type u_1} [Ring S] [Algebra k S] {τ : S →ₐ[k] S} {ε : SigmaDerivation τ} : Ring (OreExtension τ ε)

@[simp]

theorem TauCeti.OreExtension.coeff_neg {k : Type u} [CommSemiring k] {S : Type u_1} [Ring S] [Algebra k S] {τ : S →ₐ[k] S} {ε : SigmaDerivation τ} (p : OreExtension τ ε) (n : ℕ) : (-p).coeff n = -p.coeff n

Negation acts coefficientwise on Ore polynomials.

@[simp]

theorem TauCeti.OreExtension.coeff_sub {k : Type u} [CommSemiring k] {S : Type u_1} [Ring S] [Algebra k S] {τ : S →ₐ[k] S} {ε : SigmaDerivation τ} (p q : OreExtension τ ε) (n : ℕ) : (p - q).coeff n = p.coeff n - q.coeff n

Subtraction acts coefficientwise on Ore polynomials.