The order-Rees two-jet ring

This file constructs only the ring half of the order-Rees two-jet. The specialization map is defined directly as the finite sum of the order-principal components of the Rees coefficients. Its multiplication proof retains the written coefficient order in the noncommutative Weyl algebra.

No Rees-module action, quotient module, trace package, or Gabber theorem is constructed here.

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesScalarHom (k : Type u) [Field k] {n : ℕ} : k →+* ↥(WeylOrderRees.OrderReesRing k)

The scalar embedding into Rees degree zero.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Stafford38.CharacteristicOrderReesTwoJet.orderReesRingAlgebra (k : Type u) [Field k] {n : ℕ} : Algebra k ↥(WeylOrderRees.OrderReesRing k)

The inherited k-algebra structure on the order-Rees subring, with scalars placed in Rees degree zero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderPrincipalSum (k : Type u) [Field k] {n : ℕ} : Polynomial (WeylIteratedEquivalence.PresentedWeyl k n) →+ Characteristic.SymbolRing k n

The additive finite sum of degreewise order-principal components.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderPrincipalSum_monomial (k : Type u) [Field k] {n : ℕ} (N : ℕ) (z : WeylIteratedEquivalence.PresentedWeyl k n) : (orderPrincipalSum k) ((Polynomial.monomial N) z) = (WeylLeadingSymbol.presentedPrincipalComponent k WeylFiltration.orderWeight N) z

theorem Stafford38.CharacteristicOrderReesTwoJet.orderPrincipalSum_mul (k : Type u) [Field k] {n : ℕ} (f g : ↥(WeylOrderRees.OrderReesRing k)) : (orderPrincipalSum k) ↑(f * g) = (orderPrincipalSum k) ↑f * (orderPrincipalSum k) ↑g

On Rees polynomials, the degreewise principal-component sum preserves multiplication. In the double sum, coefficients occur as x * y, in the same order as in the input product.

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization (k : Type u) [Field k] {n : ℕ} : ↥(WeylOrderRees.OrderReesRing k) →+* Characteristic.SymbolRing k n

Global specialization of the order-Rees ring to its commutative symbol ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization_monomial (k : Type u) [Field k] {n : ℕ} (N : ℕ) (z : ↥(WeylFiltration.orderPiece k n N)) : (orderReesSpecialization k) (WeylOrderRees.orderReesMonomial k N z) = (WeylLeadingSymbol.presentedPrincipalComponent k WeylFiltration.orderWeight N) ↑z

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization_parameter (k : Type u) [Field k] {n : ℕ} : (orderReesSpecialization k) (WeylOrderRees.orderReesParameter k) = 0

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization_surjective (k : Type u) [Field k] {n : ℕ} : Function.Surjective ⇑(orderReesSpecialization k)

Every symbol has a Rees lift.

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization_scalar (k : Type u) [Field k] {n : ℕ} (a : k) : (orderReesSpecialization k) ((orderReesScalarHom k) a) = (algebraMap k (Characteristic.SymbolRing k n)) a

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecializationAlg (k : Type u) [Field k] {n : ℕ} : ↥(WeylOrderRees.OrderReesRing k) →ₐ[k] Characteristic.SymbolRing k n

The order-Rees specialization as a k-algebra homomorphism.

Equations

• Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecializationAlg k = AlgHom.mk' (Stafford38.CharacteristicOrderReesTwoJet.orderReesSpecialization k) ⋯

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetIdeal (k : Type u) [Field k] {n : ℕ} : TwoSidedIdeal ↥(WeylOrderRees.OrderReesRing k)

The two-sided ideal generated by the square of the Rees parameter.

Equations

• Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetIdeal k = TwoSidedIdeal.span {Stafford38.WeylOrderRees.orderReesParameter k ^ 2}

@[reducible, inline]

abbrev Stafford38.CharacteristicOrderReesTwoJet.OrderReesTwoJet (k : Type u) [Field k] {n : ℕ} : Type u

The order-Rees ring modulo T².

Equations

• Stafford38.CharacteristicOrderReesTwoJet.OrderReesTwoJet k = (Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetIdeal k).ringCon.Quotient

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetQuotient (k : Type u) [Field k] {n : ℕ} : ↥(WeylOrderRees.OrderReesRing k) →ₐ[k] OrderReesTwoJet k

The canonical algebra quotient map to the two-jet.

Equations

• Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetQuotient k = AlgHom.mk' (Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetIdeal k).ringCon.mk' ⋯

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetParameter (k : Type u) [Field k] {n : ℕ} : OrderReesTwoJet k

The image of the Rees parameter in the two-jet.

Equations

• Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetParameter k = (Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetQuotient k) (Stafford38.WeylOrderRees.orderReesParameter k)

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetParameter_mem_center (k : Type u) [Field k] {n : ℕ} : orderReesTwoJetParameter k ∈ Set.center (OrderReesTwoJet k)

The two-jet parameter is central.

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetParameter_sq (k : Type u) [Field k] {n : ℕ} : orderReesTwoJetParameter k ^ 2 = 0

The two-jet parameter is square-zero.

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetIdeal_le_specializationKer (k : Type u) [Field k] {n : ℕ} : orderReesTwoJetIdeal k ≤ TwoSidedIdeal.ker (orderReesSpecialization k)

noncomputable def Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetSpecialization (k : Type u) [Field k] {n : ℕ} : OrderReesTwoJet k →ₐ[k] Characteristic.SymbolRing k n

Specialization factors through the order-Rees two-jet.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetSpecialization_quotient (k : Type u) [Field k] {n : ℕ} (r : ↥(WeylOrderRees.OrderReesRing k)) : (orderReesTwoJetSpecialization k) ((orderReesTwoJetQuotient k) r) = (orderReesSpecialization k) r

@[simp]

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetSpecialization_parameter (k : Type u) [Field k] {n : ℕ} : (orderReesTwoJetSpecialization k) (orderReesTwoJetParameter k) = 0

theorem Stafford38.CharacteristicOrderReesTwoJet.orderReesTwoJetSpecialization_surjective (k : Type u) [Field k] {n : ℕ} : Function.Surjective ⇑(orderReesTwoJetSpecialization k)

The two-jet specialization remains surjective.