ExtendedKernelIntersection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The coefficient algebra of the localization intersects the full ambient ring in exactly ℂ[Fₙ] in every dimension n ≥ 4.

theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedCoefficientMap_complex line 14
theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedCoefficientMap_polynomial line 21
theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedCoefficientMap_parameter line 37
theorem OAI.AbhyankarSathaye.CommutingDerivations.extended_localization_kernel_intersection line 44
Source documentation
Exact input to the generic commuting-family construction, specialized to the actual all-dimensional localization and coordinate equivalence.
```
theorem extended_localization_kernel_intersection {n : ℕ} (hn : 4 ≤ n)
    (r : MvPolynomial (Fin n) ℂ) :
    (∃ b : LaurentCoefficients,
      extendedLocalizationEquiv hn (extendedLocMap hn r) = C b) ↔
    r ∈ Algebra.adjoin ℂ ({extendedF hn} : Set (MvPolynomial (Fin n) ℂ)) := by
…
```
Mentions: OAI.AbhyankarSathaye.CommutingDerivations.LaurentCoefficients, OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv, OAI.AbhyankarSathaye.CommutingDerivations.extendedLocMap, OAI.AbhyankarSathaye.extendedF