Tangentially linear equivalences between canonical total pages and graded modules.

@[reducible, inline]

abbrev Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.Graded (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : Type u_1

The order-associated graded module of the canonical right-ideal quotient.

Equations

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

@[reducible, inline]

abbrev Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.T (k : Type u_1) [Field k] (n : ℕ) : Type u_1

The polynomial ring in the tangential coordinate and momentum variables.

Equations

• Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.T k n = MvPolynomial (Fin n ⊕ Fin n) k

@[instance_reducible]

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.gradedModule (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : Module (T k n) (Graded k n N d)

The tangential polynomial action on the order-associated graded module.

Equations

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

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.graded_C_smul (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (c : k) (z : Graded k n N d) : MvPolynomial.C c • z = c • z

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.sourceEquiv_map_smul (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (P : T k n) (z : (CanonicalTangentialTotalAction.complex k n N d).SourceTotal 0) : (CanonicalTotalGradedBridge.sourceTotal0LinearEquivOrderAssociatedGraded k n N d) (P • z) = P • (CanonicalTotalGradedBridge.sourceTotal0LinearEquivOrderAssociatedGraded k n N d) z

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.targetEquiv_map_smul (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (P : T k n) (z : (CanonicalTangentialTotalAction.complex k n N d).TargetTotal 0) : (CanonicalTotalGradedBridge.targetTotal0LinearEquivOrderAssociatedGraded k n N d) (P • z) = P • (CanonicalTotalGradedBridge.targetTotal0LinearEquivOrderAssociatedGraded k n N d) z

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.sourceGradedEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (CanonicalTangentialTotalAction.complex k n N d).SourceTotal 0 ≃ₗ[T k n] Graded k n N d

The tangential-linear identification of the degree-zero source total with the associated graded module.

Equations

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

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.targetGradedEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (CanonicalTangentialTotalAction.complex k n N d).TargetTotal 0 ≃ₗ[T k n] Graded k n N d

The tangential-linear identification of the degree-zero target total with the associated graded module.

Equations

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

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.gradedEquiv_drop (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (z : (CanonicalTangentialTotalAction.complex k n N d).SourceTotal 0) : (targetGradedEquiv k n N d) ((CanonicalTangentialTotalAction.tangentialDrop k n N d 0) z) = (CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)) ((sourceGradedEquiv k n N d) z)

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.zeroDropKernelEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : ↥(CanonicalTangentialTotalAction.tangentialDrop k n N d 0).ker ≃ₗ[T k n] ↥(CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)).ker

The identification of the degree-zero drop kernel with the kernel of the tangential coordinate action.

Equations

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

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.targetGradedEquiv_range (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : Submodule.map (↑(targetGradedEquiv k n N d)) (CanonicalTangentialTotalAction.tangentialDrop k n N d 0).range = (CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)).range

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.zeroDropCokernelEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : ((CanonicalTangentialTotalAction.complex k n N d).TargetTotal 0 ⧸ (CanonicalTangentialTotalAction.tangentialDrop k n N d 0).range) ≃ₗ[T k n] Graded k n N d ⧸ (CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)).range

The identification of the degree-zero drop cokernel with the cokernel of the tangential coordinate action.

Equations

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

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.firstSourceGradedKernelEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (CanonicalTangentialTotalAction.complex k n N d).SourceTotal 1 ≃ₗ[T k n] ↥(CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)).ker

The first source total identified with the kernel of the tangential coordinate action.

Equations

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

noncomputable def Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.firstTargetGradedCokernelEquiv (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) : (CanonicalTangentialTotalAction.complex k n N d).TargetTotal 1 ≃ₗ[T k n] Graded k n N d ⧸ (CanonicalOldTangentialFiniteness.oldCoordinateMap n (Graded k n N d)).range

The first target total identified with the cokernel of the tangential coordinate action.

Equations

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

theorem Stafford38.Characteristic.CanonicalGradedTangentialEquivalences.first_pages_finite (k : Type u_1) [Field k] (n N : ℕ) (d : WeylIteratedEquivalence.PresentedWeyl k (n + 1)) (hd : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N d) : Module.Finite (T k n) ((CanonicalTangentialTotalAction.complex k n N d).SourceTotal 1) ∧ Module.Finite (T k n) ((CanonicalTangentialTotalAction.complex k n N d).TargetTotal 1)