Main.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Commuting locally nilpotent derivations for the explicit Abhyankar polynomial in every dimension n ≥ 4, with common kernel ℂ[Fₙ].

theorem OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_all_dimensions line 17
theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedF_four line 51

theorem OAI.AbhyankarSathaye.CommutingDerivations.commuting_derivations_dimension_four line 63

Source documentation

Three commuting, R-linearly independent locally nilpotent derivations of the original four-variable ring, with exact common kernel C[F]. Every element of this kernel, in particular any generator of it, fails to be a coordinate.

theorem commuting_derivations_dimension_four :
    ∃ d : Fin 3 → Derivation ℂ R R,
      (∀ i, d i (F + 1) = 0) ∧
      (∀ i j p, d i (d j p) = d j (d i p)) ∧
      (∀ i, LocallyNilpotent (d i)) ∧
      LinearIndependent R d ∧
      (∀ p, (∀ i, d i p = 0) ↔ p ∈ Algebra.adjoin ℂ ({F} : Set R)) ∧
      (∀ g, (∀ i, d i g = 0) → ¬ ∃ (e : R ≃ₐ[ℂ] R) (j : Fin 4), e (X j) = g) := by
…

Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.F, OAI.AbhyankarSathaye.p