Coefficient extension for the presented Weyl algebra #
This file records the concrete map needed before any characteristic-support
descent can be attempted. The source is the quotient presentation over k
and the target is the same presentation over an extension field K. The map
is defined by the quotient universal property; in particular, no PBW
identification or base-change theorem is used in its definition.
The file also proves injectivity, PBW normal-form and filtration transport,
PBW monicity, canonical-right-ideal transport in the usable direction, and the
resulting source-to-target order-initial-ideal inclusion. The reverse filtered
comparison is recorded as an explicit contract below and proved in
FilteredScalarLifting.lean; no base-change equality is treated as
definitional.
@[simp]
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_generator
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(i : Fin n ⊕ Fin n)
:
(presentedWeylScalarExtension n) (Stafford.freeWeylGenerator (Matrix.J (Fin n) k) i) = Stafford.freeWeylGenerator (Matrix.J (Fin n) K) i
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_scalar
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(a : k)
:
(presentedWeylScalarExtension n) ((algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)) a) = (algebraMap k (WeylIteratedEquivalence.PresentedWeyl K n)) a
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_map_mul
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(a b : WeylIteratedEquivalence.PresentedWeyl k n)
:
(presentedWeylScalarExtension n) (a * b) = (presentedWeylScalarExtension n) a * (presentedWeylScalarExtension n) b
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_map_add
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(a b : WeylIteratedEquivalence.PresentedWeyl k n)
:
(presentedWeylScalarExtension n) (a + b) = (presentedWeylScalarExtension n) a + (presentedWeylScalarExtension n) b
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_commutes
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(a : k)
:
(presentedWeylScalarExtension n) ((algebraMap k (WeylIteratedEquivalence.PresentedWeyl k n)) a) = (algebraMap k (WeylIteratedEquivalence.PresentedWeyl K n)) a
Compatibility with the recursive presentation #
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_previous
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(z : WeylIteratedEquivalence.PresentedWeyl k n)
:
(presentedWeylScalarExtension (n + 1)) ((WeylIteratedEquivalence.previousWeylEmbedding k n) z) = (WeylIteratedEquivalence.previousWeylEmbedding K n) ((presentedWeylScalarExtension n) z)
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_orderedMonomial
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(a p : Fin n → ℕ)
:
(presentedWeylScalarExtension n) (WeylPBW.presentedOrderedMonomial k n a p) = WeylPBW.presentedOrderedMonomial K n a p
The PBW-linear extension of coefficients #
noncomputable def
Stafford38.Weyl.PresentedScalarExtension.symbolScalarExtension
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
:
Coefficient extension on the commutative symbol polynomial ring.
Equations
- Stafford38.Weyl.PresentedScalarExtension.symbolScalarExtension n = { toRingHom := MvPolynomial.map (algebraMap k K), commutes' := ⋯ }
Instances For
@[simp]
theorem
Stafford38.Weyl.PresentedScalarExtension.symbolScalarExtension_apply
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(p : Characteristic.SymbolRing k n)
:
theorem
Stafford38.Weyl.PresentedScalarExtension.symbolScalarExtension_monomial
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(m : Characteristic.PhaseVar n →₀ ℕ)
(a : k)
:
(symbolScalarExtension n) ((MvPolynomial.monomial m) a) = (MvPolynomial.monomial m) ((algebraMap k K) a)
noncomputable def
Stafford38.Weyl.PresentedScalarExtension.pbwScalarLinearMap
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
:
The k-linear map obtained by extending PBW coordinates and rebuilding in
the target presentation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Stafford38.Weyl.PresentedScalarExtension.pbwScalarLinearMap_basis
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(m : Characteristic.PhaseVar n →₀ ℕ)
:
@[simp]
theorem
Stafford38.Weyl.PresentedScalarExtension.pbwScalarLinearMap_orderedMonomial
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(m : Characteristic.PhaseVar n →₀ ℕ)
:
(pbwScalarLinearMap n)
(WeylPBW.presentedOrderedMonomial k n (fun (i : Fin n) => m (Sum.inl i)) fun (i : Fin n) => m (Sum.inr i)) = WeylPBW.presentedOrderedMonomial K n (fun (i : Fin n) => m (Sum.inl i)) fun (i : Fin n) => m (Sum.inr i)
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_basis
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(m : Characteristic.PhaseVar n →₀ ℕ)
:
(presentedWeylScalarExtension n) ((WeylPBW.presentedPBWBasis k n) m) = (WeylPBW.presentedPBWBasis K n) m
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedNormalFormLinearEquiv_scalarExtension
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(z : WeylIteratedEquivalence.PresentedWeyl k n)
:
(WeylPBW.presentedNormalFormLinearEquiv K n) ((presentedWeylScalarExtension n) z) = (symbolScalarExtension n) ((WeylPBW.presentedNormalFormLinearEquiv k n) z)
Injectivity and filtered transport #
theorem
Stafford38.Weyl.PresentedScalarExtension.symbolScalarExtension_weightedHomogeneousComponent
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(w : Characteristic.PhaseVar n → ℕ)
(N : ℕ)
(f : Characteristic.SymbolRing k n)
:
(symbolScalarExtension n) ((MvPolynomial.weightedHomogeneousComponent w N) f) = (MvPolynomial.weightedHomogeneousComponent w N) ((symbolScalarExtension n) f)
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_mem_weightPiece
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(w : Characteristic.PhaseVar n → ℕ)
(N : ℕ)
{z : WeylIteratedEquivalence.PresentedWeyl k n}
(hz : z ∈ WeylFiltration.presentedWeightPiece k w N)
:
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_mem_orderPiece
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
{z : WeylIteratedEquivalence.PresentedWeyl k n}
(hz : z ∈ WeylFiltration.orderPiece k n N)
:
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_mem_bernsteinPiece
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
{z : WeylIteratedEquivalence.PresentedWeyl k n}
(hz : z ∈ WeylFiltration.bernsteinPiece k n N)
:
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_principalComponent
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(w : Characteristic.PhaseVar n → ℕ)
(N : ℕ)
(z : WeylIteratedEquivalence.PresentedWeyl k n)
:
(symbolScalarExtension n) ((WeylLeadingSymbol.presentedPrincipalComponent k w N) z) = (WeylLeadingSymbol.presentedPrincipalComponent K w N) ((presentedWeylScalarExtension n) z)
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_isPBWMonicAt
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
{z : WeylIteratedEquivalence.PresentedWeyl k (n + 1)}
(hz : WeylPBWMonicBridge.IsPBWMonicAt k (Sum.inr 0) N z)
:
WeylPBWMonicBridge.IsPBWMonicAt K (Sum.inr 0) N ((presentedWeylScalarExtension (n + 1)) z)
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_mem_canonicalRightIdeal
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
{d z : WeylIteratedEquivalence.PresentedWeyl k (n + 1)}
(hz : z ∈ WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate k n) d N)
:
(presentedWeylScalarExtension (n + 1)) z ∈ WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate K n)
((presentedWeylScalarExtension (n + 1)) d) N
The safe initial-ideal comparison #
theorem
Stafford38.Weyl.PresentedScalarExtension.presentedWeylScalarExtension_map_orderInitialIdeal_le
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
(d : WeylIteratedEquivalence.PresentedWeyl k (n + 1))
:
Ideal.map (symbolScalarExtension (n + 1)).toRingHom
(CharacteristicInitialIdeal.orderInitialIdeal k
(WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate k n) d N)) ≤ CharacteristicInitialIdeal.orderInitialIdeal K
(WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate K n)
((presentedWeylScalarExtension (n + 1)) d) N)
Every source order-initial generator maps to a target order-initial generator. This is the comparison needed for descent; it is intentionally a one-way inclusion and makes no claim that the target initial ideal is the extension of the source initial ideal.
theorem
Stafford38.Weyl.PresentedScalarExtension.target_orderCharacteristicSupport_subset_scalarExtended_zeroLocus
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
(d : WeylIteratedEquivalence.PresentedWeyl k (n + 1))
:
CharacteristicInitialIdeal.orderCharacteristicSupport K
(WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate K n)
((presentedWeylScalarExtension (n + 1)) d) N) ⊆
PrimeSpectrum.zeroLocus
↑(Ideal.map (symbolScalarExtension (n + 1)).toRingHom
(CharacteristicInitialIdeal.orderInitialIdeal k
(WeylEulerResidue.canonicalRightIdeal (WeylIteratedEquivalence.presentedCoordinate k n) d N)))
PBW spanning after scalar extension #
theorem
Stafford38.Weyl.PresentedScalarExtension.target_mem_scalarImageSpan
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(z : WeylIteratedEquivalence.PresentedWeyl K n)
:
def
Stafford38.Weyl.PresentedScalarExtension.scalarImageRightIdealSpan
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n))
:
The K-linear span of the scalar extensions of a source right ideal.
Equations
Instances For
theorem
Stafford38.Weyl.PresentedScalarExtension.scalarImageRightIdealSpan_mul_right
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n : ℕ)
(I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n))
{a : WeylIteratedEquivalence.PresentedWeyl K n}
(ha : a ∈ scalarImageRightIdealSpan n I)
(b : WeylIteratedEquivalence.PresentedWeyl K n)
:
theorem
Stafford38.Weyl.PresentedScalarExtension.target_canonicalRightIdeal_le_scalarImageRightIdealSpan
{k : Type u}
{K : Type v}
[Field k]
[Field K]
[Algebra k K]
(n N : ℕ)
(d : WeylIteratedEquivalence.PresentedWeyl k (n + 1))
(z : WeylIteratedEquivalence.PresentedWeyl K (n + 1))
:
The filtered lifting contract #
The exact filtered statement for support descent. It asks that
every target order-initial generator be represented by the scalar extension
of source initial generators. It is stronger than the unfiltered PBW span
proved above and is deliberately not identified with a definitional
base-change equality. FilteredScalarLifting.lean proves this contract by
flat base change of the ideal/order-piece intersection.
Equations
- One or more equations did not get rendered due to their size.