OAI/AlgebraicGeometry/CommutingDerivations/KernelObstruction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Every element of the proposed common kernel has a critical point. This proves the coordinate obstruction for all such elements, independently of whether they generate that subalgebra. It does not assert kernel equality.

  1. theorem OAI.AbhyankarSathaye.CommutingDerivations.critical_aeval line 13
  2. theorem OAI.AbhyankarSathaye.CommutingDerivations.no_coordinate_aeval_of_critical line 23
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.polynomial_in_extendedF_not_coordinate line 30
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.element_of_extendedF_subring_not_coordinate line 39

    Source documentation

    In particular, no generator of a common kernel equal to C[F_n] can be a coordinate. The explicit polynomial-expression hypothesis suffices.

    theorem element_of_extendedF_subring_not_coordinate {n : ℕ} (hn : 4 ≤ n)
    (g : MvPolynomial (Fin n) ℂ)
    (hg : ∃ q : Polynomial ℂ, g = Polynomial.aeval (extendedF hn) q) :
    ¬ ∃ (e : MvPolynomial (Fin n) ℂ ≃ₐ[ℂ] MvPolynomial (Fin n) ℂ) (i : Fin n),
      e (X i) = g := by
…

    Mentions: OAI.AbhyankarSathaye.extendedF