Documentation

LeanPool.Stafford38.Stafford38.Geometry.PowerSeriesArcTangency

Tangency of the formal-arc velocity #

If a power-series arc annihilates an affine ideal coefficientwise, its formal derivative and the residues of arbitrary derivation directions are Zariski tangent vectors at the constant point. The result is deliberately independent of any projective closure or normalization: it consumes an actual power-series arc and produces actual tangent data for the scalar-extended base ideal.

The file does not construct the arc or identify its tangent data with a projective component. Those chart, normalization, frame-independence, and dimension arguments remain separate geometric obligations.

The formal chain rule #

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.derivation_eval₂ {k : Type u} [Field k] {S : Type u_1} [CommSemiring S] [Algebra k S] (D : Derivation k S S) {m : ℕ} (f : MvPolynomial (Fin m) k) (q : Fin m → S) :
D (MvPolynomial.eval₂ (algebraMap k S) q f) = ∑ i : Fin m, MvPolynomial.eval₂ (algebraMap k S) q ((MvPolynomial.pderiv i) f) * D (q i)

Chain rule for a derivation of a field-valued polynomial evaluation.

Derivation directions of extended ideal loci #

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.derivationVector_mem_zariskiTangentSpace_of_eval₂_eq_zero {k : Type u} [Field k] {S : Type u_1} [Field S] [Algebra k S] (D : Derivation k S S) {m : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → S) (hq : ∀ f ∈ I, MvPolynomial.eval₂ (algebraMap k S) q f = 0) :
(fun (i : Fin m) => D (q i)) ∈ AffineConormalSpan.zariskiTangentSpace q (Ideal.map (MvPolynomial.map (algebraMap k S)) I)

A derivation of an evaluation point is tangent to the scalar extension of an ideal that vanishes at that point. This is the coefficient-direction analogue of the power-series arc theorem below; it is stated for an arbitrary field extension and an arbitrary derivation, so no chart or completeness hypothesis is hidden in the result.

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.constantCoeff_eval₂ {k : Type u} [Field k] {K : Type u} [Field K] [Algebra k K] {m : ℕ} (f : MvPolynomial (Fin m) k) (q : Fin m → PowerSeries K) :
PowerSeries.constantCoeff (MvPolynomial.eval₂ (algebraMap k (PowerSeries K)) q f) = MvPolynomial.eval₂ (algebraMap k K) (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) f

Constant-term evaluation commutes with evaluating a base-field polynomial in a power-series point.

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.residueDerivationVector_mem_zariskiTangentSpace_of_eval₂_eq_zero {k : Type u} [Field k] {K : Type u} [Field K] [Algebra k K] {m : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries K) (D : Derivation k (PowerSeries K) (PowerSeries K)) (hq : ∀ f ∈ I, MvPolynomial.eval₂ (algebraMap k (PowerSeries K)) q f = 0) :
(fun (i : Fin m) => PowerSeries.constantCoeff (D (q i))) ∈ AffineConormalSpan.zariskiTangentSpace (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) (Ideal.map (MvPolynomial.map (algebraMap k K)) I)

The residue of an arbitrary derivation direction on an annihilating power-series arc is tangent to the scalar-extended base ideal. The derivation need not preserve the coefficient field: the ideal-span argument handles the coefficient terms because every base equation already vanishes along the arc.

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.residueFrameVector_uniformizer_mem_zariskiTangentSpace_of_eval₂_eq_zero {k : Type u} [Field k] {K : Type u} [Field K] [Algebra k K] {m κ : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries K) (D : Fin κ → Derivation k K K) (hq : ∀ f ∈ I, MvPolynomial.eval₂ (algebraMap k (PowerSeries K)) q f = 0) :
ContinuousPowerSeriesTangentFrame.residueFrameVector q D none ∈ AffineConormalSpan.zariskiTangentSpace (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) (Ideal.map (MvPolynomial.map (algebraMap k K)) I)

The uniformizer member of the power-series frame is tangent after residue specialization whenever the arc annihilates the base ideal.

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.residueFrameVector_coefficient_mem_zariskiTangentSpace_of_eval₂_eq_zero {k : Type u} [Field k] {K : Type u} [Field K] [Algebra k K] {m κ : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries K) (D : Fin κ → Derivation k K K) (hq : ∀ f ∈ I, MvPolynomial.eval₂ (algebraMap k (PowerSeries K)) q f = 0) (j : Fin κ) :
ContinuousPowerSeriesTangentFrame.residueFrameVector q D (some j) ∈ AffineConormalSpan.zariskiTangentSpace (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) (Ideal.map (MvPolynomial.map (algebraMap k K)) I)

Every coefficient-field derivation direction of an annihilating power-series arc is tangent at its constant point to the scalar-extended base ideal.

source
theorem Stafford38.Geometry.PowerSeriesArcTangency.derivative_eval_map {k : Type u} [Field k] {m : ℕ} (f : MvPolynomial (Fin m) k) (q : Fin m → PowerSeries k) :
PowerSeries.derivative ((MvPolynomial.eval q) ((MvPolynomial.map PowerSeries.C) f)) = ∑ i : Fin m, (MvPolynomial.eval q) ((MvPolynomial.map PowerSeries.C) ((MvPolynomial.pderiv i) f)) * PowerSeries.derivative (q i)

Formal chain rule for evaluating a polynomial along a power-series arc.

Tangency at the closed point #

source
noncomputable def Stafford38.Geometry.PowerSeriesArcTangency.arcVelocity {k : Type u} [Field k] {m : ℕ} (q : Fin m → PowerSeries k) :
Fin m → k

The velocity of a power-series arc at its constant term.

Equations
Instances For
    source
    @[simp]
    theorem Stafford38.Geometry.PowerSeriesArcTangency.arcVelocity_eq_residueFrameVector {k : Type u} [Field k] {m κ : ℕ} (q : Fin m → PowerSeries k) (D : Fin κ → Derivation k k k) :
    arcVelocity q = ContinuousPowerSeriesTangentFrame.residueFrameVector q D none
    source
    theorem Stafford38.Geometry.PowerSeriesArcTangency.differentialCovector_arcVelocity_eq_zero_of_eval_eq_zero {k : Type u} [Field k] {m : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries k) (hq : ∀ f ∈ I, (MvPolynomial.eval q) ((MvPolynomial.map PowerSeries.C) f) = 0) (f : MvPolynomial (Fin m) k) :
    f ∈ I → (AffineConormalSpan.differentialCovector (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) f) (arcVelocity q) = 0

    The formal-arc velocity annihilates the differential of every polynomial that vanishes identically along the arc.

    source
    theorem Stafford38.Geometry.PowerSeriesArcTangency.arcVelocity_mem_zariskiTangentSpace_of_eval_eq_zero {k : Type u} [Field k] {m : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries k) (hq : ∀ f ∈ I, (MvPolynomial.eval q) ((MvPolynomial.map PowerSeries.C) f) = 0) :
    arcVelocity q ∈ AffineConormalSpan.zariskiTangentSpace (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) I

    An actual power-series arc supplies the uniformizer tangent vector needed by the higher-dimensional conormal consumer.

    source
    @[simp]
    theorem Stafford38.Geometry.PowerSeriesArcTangency.residueFrameVector_none_mem_zariskiTangentSpace_of_eval_eq_zero {k : Type u} [Field k] {m κ : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (q : Fin m → PowerSeries k) (D : Fin κ → Derivation k k k) (hq : ∀ f ∈ I, (MvPolynomial.eval q) ((MvPolynomial.map PowerSeries.C) f) = 0) :
    ContinuousPowerSeriesTangentFrame.residueFrameVector q D none ∈ AffineConormalSpan.zariskiTangentSpace (fun (i : Fin m) => PowerSeries.constantCoeff (q i)) I