Affine conormals are finite spans of equation differentials

For an ideal of equations in affine space and a rational point, define the embedded Zariski tangent space as the common kernel of the evaluated differentials. Its annihilator is exactly the span of those differentials. Because the ambient affine space is finite-dimensional, every conormal covector is therefore an explicit finite linear combination of equation differentials.

The final theorem feeds that finite representation into the pointwise Hamiltonian-translation theorem. No smoothness assumption is needed for this linear-algebraic bridge. What is not proved here is the scheme-geometric identification of this equation-defined tangent space with the tangent fibre of a smooth locus, or the passage from pointwise fibres to the closure of the smooth conormal bundle.

@[reducible, inline]

abbrev Stafford38.Geometry.AffineConormalSpan.AffineTangentVector (k : Type u_2) (n : ℕ) : Type u_2

The ambient tangent vector space of affine n-space.

Equations

• Stafford38.Geometry.AffineConormalSpan.AffineTangentVector k n = (Fin n → k)

noncomputable def Stafford38.Geometry.AffineConormalSpan.differentialCovector {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (f : MvPolynomial (Fin n) k) : Module.Dual k (AffineTangentVector k n)

The differential of f at y, viewed as a linear functional on the ambient affine tangent space.

Equations

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

@[simp]

theorem Stafford38.Geometry.AffineConormalSpan.differentialCovector_apply {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (f : MvPolynomial (Fin n) k) (v : AffineTangentVector k n) : (differentialCovector y f) v = ∑ i : Fin n, CoisotropicTranslation.differentialAt y f i * v i

def Stafford38.Geometry.AffineConormalSpan.equationCovectorSpan {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) : Submodule k (Module.Dual k (AffineTangentVector k n))

Covectors generated by the differentials of all equations in I.

Equations

• Stafford38.Geometry.AffineConormalSpan.equationCovectorSpan y I = Submodule.span k (Set.range fun (f : ↥I) => Stafford38.Geometry.AffineConormalSpan.differentialCovector y ↑f)

def Stafford38.Geometry.AffineConormalSpan.zariskiTangentSpace {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) : Submodule k (AffineTangentVector k n)

The embedded Zariski tangent space cut out by the first-order parts of all equations in I.

Equations

• Stafford38.Geometry.AffineConormalSpan.zariskiTangentSpace y I = (Stafford38.Geometry.AffineConormalSpan.equationCovectorSpan y I).dualCoannihilator

def Stafford38.Geometry.AffineConormalSpan.affineConormalSpace {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) : Submodule k (Module.Dual k (AffineTangentVector k n))

The embedded conormal space, defined as the annihilator of the embedded Zariski tangent space.

Equations

• Stafford38.Geometry.AffineConormalSpan.affineConormalSpace y I = (Stafford38.Geometry.AffineConormalSpan.zariskiTangentSpace y I).dualAnnihilator

theorem Stafford38.Geometry.AffineConormalSpan.affineConormalSpace_eq_equationCovectorSpan {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) : affineConormalSpace y I = equationCovectorSpan y I

The embedded conormal is exactly the span of evaluated differentials of the equation ideal. This is finite-dimensional double-annihilator duality.

theorem Stafford38.Geometry.AffineConormalSpan.mem_affineConormalSpace_iff_exists_finsupp {k : Type u_1} [Field k] {n : ℕ} (y : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) (phi : Module.Dual k (AffineTangentVector k n)) : phi ∈ affineConormalSpace y I ↔ ∃ (c : ↥I →₀ k), (Finsupp.linearCombination k fun (f : ↥I) => differentialCovector y ↑f) c = phi

Every embedded conormal covector has an explicit finite-support expansion in differentials of equations.

def Stafford38.Geometry.AffineConormalSpan.coordinateCovector {k : Type u_1} [Field k] {n : ℕ} (xi : Fin n → k) : Module.Dual k (AffineTangentVector k n)

The coordinate covector associated with a fibre coordinate xi.

Equations

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

@[simp]

theorem Stafford38.Geometry.AffineConormalSpan.coordinateCovector_apply {k : Type u_1} [Field k] {n : ℕ} (xi v : Fin n → k) : (coordinateCovector xi) v = ∑ i : Fin n, xi i * v i

theorem Stafford38.Geometry.AffineConormalSpan.coordinateCovector_injective {k : Type u_1} [Field k] {n : ℕ} : Function.Injective coordinateCovector

Equality of coordinate covectors recovers equality of their coordinates.

theorem Stafford38.Geometry.AffineConormalSpan.coordinate_mem_affineConormalSpace_exists_finsupp {k : Type u_1} [Field k] {n : ℕ} (y xi : Fin n → k) (I : Ideal (MvPolynomial (Fin n) k)) : coordinateCovector xi ∈ affineConormalSpace y I → ∃ (c : ↥I →₀ k), ∀ (i : Fin n), xi i = ∑ f ∈ c.support, c f * CoisotropicTranslation.differentialAt y (↑f) i

A conormal coordinate covector admits a finite-support expansion in gradients of equations.

theorem Stafford38.Geometry.AffineConormalSpan.affineConormal_coordinatePoint_isCommonZero {k : Type u_1} [Field k] {n : ℕ} [CharZero k] (J : Ideal (Characteristic.SymbolRing k n)) (hJ : Characteristic.BaseRelativePoisson.IsBaseRelativePoisson J) (y : Fin n → k) (hzero : ∀ g ∈ J, (MvPolynomial.eval (CoisotropicTranslation.zeroSectionPoint y)) g = 0) (I : Ideal (MvPolynomial (Fin n) k)) (hlift : ∀ (f : ↥I), CoisotropicTranslation.baseLift ↑f ∈ J) (xi : Fin n → k) (hxi : coordinateCovector xi ∈ affineConormalSpace y I) (g : Characteristic.SymbolRing k n) : g ∈ J → (MvPolynomial.eval (Sum.elim y xi)) g = 0

The genuine conormal consumer: under the existing base-relative Poisson hypothesis, every coordinate covector in the equation-defined affine conormal space gives a common zero in the corresponding support fibre.

theorem Stafford38.Geometry.AffineConormalSpan.reducedOrderSupport_affineConormal_coordinatePoint_isCommonZero {k : Type u_1} [Field k] {n : ℕ} [CharZero k] (W : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (hJ : Characteristic.BaseRelativePoisson.IsBaseRelativePoisson (Characteristic.ReducedSupportIdeal.reducedOrderSupportIdeal k W)) (y eta : Fin n → k) (hpoint : ∀ g ∈ Characteristic.ReducedSupportIdeal.reducedOrderSupportIdeal k W, (MvPolynomial.eval (Sum.elim y eta)) g = 0) (xi : Fin n → k) (hxi : coordinateCovector xi ∈ affineConormalSpace y (Characteristic.ReducedSupportIdeal.reducedOrderBaseIdeal k W)) (g : Characteristic.SymbolRing k n) : g ∈ Characteristic.ReducedSupportIdeal.reducedOrderSupportIdeal k W → (MvPolynomial.eval (Sum.elim y xi)) g = 0

Concrete characteristic-support form. If (y, eta) lies in the reduced order support and the required base-relative Gabber fragment holds, then the entire equation-defined conormal space of the contracted base ideal over y lies in the same reduced support fibre.

theorem Stafford38.Geometry.AffineConormalSpan.reducedOrderBaseZero_affineConormal_coordinatePoint_isCommonZero {k : Type u_1} [Field k] {n : ℕ} [CharZero k] (W : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (hJ : Characteristic.BaseRelativePoisson.IsBaseRelativePoisson (Characteristic.ReducedSupportIdeal.reducedOrderSupportIdeal k W)) (y : Fin n → k) (hy : ∀ f ∈ Characteristic.ReducedSupportIdeal.reducedOrderBaseIdeal k W, (MvPolynomial.eval y) f = 0) (xi : Fin n → k) (hxi : coordinateCovector xi ∈ affineConormalSpace y (Characteristic.ReducedSupportIdeal.reducedOrderBaseIdeal k W)) (g : Characteristic.SymbolRing k n) : g ∈ Characteristic.ReducedSupportIdeal.reducedOrderSupportIdeal k W → (MvPolynomial.eval (Sum.elim y xi)) g = 0

Stronger contracted-base form: every equation-defined conormal covector over a common zero of the contracted base ideal lies in the reduced support fibre. No auxiliary point of that fibre is required.