Tangent spaces of algebraic sets

DefinitionTotal derivative at a point#✓fully proved

For a field \(k\), a polynomial \(f \in k[x_1, \dots, x_n]\) and \(P, v \in k^n\), the total derivative of \(f\) at \(P\) along the translated direction \(v\) is \(\sum_{i=1}^n \frac{\partial f}{\partial x_i}(P)\, v_i \in k\), where \(\frac{\partial f}{\partial x_i}\) is the formal partial derivative.

def totalDerivativeAt (f : MvPolynomial (Fin n) k) (P v : Fin n → k) : k :=
  ∑ i : Fin n, MvPolynomial.eval P (MvPolynomial.pderiv i f) * v i

Used by 4

Used byMembership in the tangent space of an ideal · Membership in the tangent space of a hypersurface · Total derivative as a linear map · Evaluating the total derivative linear map

DefinitionTotal derivative as a linear map#✓fully proved

For a field \(k\), a polynomial \(f \in k[x_1, \dots, x_n]\) and a point \(P \in k^n\), this is the \(k\)-linear map \(k^n \to k\) sending \(v\) to the total derivative of \(f\) at \(P\) along \(v\), namely \(\sum_{i=1}^n \frac{\partial f}{\partial x_i}(P)\, v_i\).

def totalDerivativeAtLin (f : MvPolynomial (Fin n) k) (P : Fin n → k) :
    (Fin n → k) →ₗ[k] k where
  toFun := totalDerivativeAt f P
  map_add' x y := by
    simp only [totalDerivativeAt, Pi.add_apply, mul_add, Finset.sum_add_distrib]
  map_smul' r x := by
    simp only [totalDerivativeAt, Pi.smul_apply, smul_eq_mul, mul_left_comm,
      ← Finset.mul_sum, RingHom.id_apply]

Uses 1 · Used by 3

Statement usesTotal derivative at a point

Used byMembership in the tangent space of a hypersurface · Tangent space of a hypersurface · Evaluating the total derivative linear map

DefinitionTangent space of a hypersurface#✓fully proved

For a field \(k\), a polynomial \(f \in k[x_1, \dots, x_n]\) and a point \(P \in k^n\), the tangent space of the hypersurface \(f = 0\) at \(P\) is the kernel of the total derivative of \(f\) at \(P\), viewed as a \(k\)-linear map \(k^n \to k\): the subspace of vectors \(v \in k^n\) with \(\sum_{i=1}^n \frac{\partial f}{\partial x_i}(P)\, v_i = 0\). The point \(P\) is not required to satisfy \(f(P) = 0\).

def tangentSpacePoly (f : MvPolynomial (Fin n) k) (P : Fin n → k) :
    Submodule k (Fin n → k) :=
  LinearMap.ker (totalDerivativeAtLin f P)

Uses 1 · Used by 3

Statement usesTotal derivative as a linear map

Used byMembership in the tangent space of an ideal · Membership in the tangent space of a hypersurface · Tangent space of an ideal

DefinitionTangent space of an ideal#✓fully proved

For a field \(k\), an ideal \(I\) of \(k[x_1, \dots, x_n]\) and a point \(P \in k^n\), the tangent space of \(I\) at \(P\) is the \(k\)-linear subspace of \(k^n\) obtained as the intersection, over all \(f \in I\), of the tangent spaces at \(P\) of the hypersurfaces \(f = 0\). The point \(P\) is not required to be a common zero of \(I\).

def tangentSpaceIdeal (I : Ideal (MvPolynomial (Fin n) k)) (P : Fin n → k) :
    Submodule k (Fin n → k) :=
  ⨅ f ∈ I, tangentSpacePoly f P

Uses 1 · Used by 1

Statement usesTangent space of a hypersurface

Used byMembership in the tangent space of an ideal

TheoremEvaluating the total derivative linear map#✓fully proved

For a field \(k\), a polynomial \(f \in k[x_1, \dots, x_n]\) and \(P, v \in k^n\), the total derivative of \(f\) at \(P\), viewed as a \(k\)-linear map \(k^n \to k\), sends \(v\) to the total derivative of \(f\) at \(P\) along \(v\).

@[simp]
theorem totalDerivativeAtLin_apply (f : MvPolynomial (Fin n) k) (P : Fin n → k)
    (v : Fin n → k) :
    totalDerivativeAtLin f P v = totalDerivativeAt f P v

Uses 2

Statement usesTotal derivative at a point · Total derivative as a linear map

TheoremMembership in the tangent space of a hypersurface#✓fully proved

Let \(k\) be a field, \(f \in k[x_1, \dots, x_n]\), and \(P, v \in k^n\). Then \(v\) lies in the tangent space of the hypersurface \(f = 0\) at \(P\) if and only if the total derivative of \(f\) at \(P\) along \(v\) is zero.

@[simp]
theorem mem_tangentSpacePoly (f : MvPolynomial (Fin n) k) (P : Fin n → k)
    (v : Fin n → k) :
    v ∈ tangentSpacePoly f P ↔ totalDerivativeAt f P v = 0

Uses 3 · Used by 1

Statement usesTangent space of a hypersurface · Total derivative at a point

Proof usesTotal derivative as a linear map

Used byMembership in the tangent space of an ideal

TheoremMembership in the tangent space of an ideal#✓fully proved

Let \(k\) be a field, \(I\) an ideal of \(k[x_1, \dots, x_n]\), and \(P, v \in k^n\). Then \(v\) lies in the tangent space of \(I\) at \(P\) if and only if, for every \(f \in I\), the total derivative of \(f\) at \(P\) along \(v\) is zero.

theorem mem_tangentSpaceIdeal (I : Ideal (MvPolynomial (Fin n) k)) (P : Fin n → k)
    (v : Fin n → k) :
    v ∈ tangentSpaceIdeal I P ↔ ∀ f ∈ I, totalDerivativeAt f P v = 0

Uses 4

Statement usesTangent space of an ideal · Total derivative at a point

Proof usesMembership in the tangent space of a hypersurface · Tangent space of a hypersurface

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.