DenominatorDescent.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common exponent clears finitely many localized generator images. Leibniz and polynomial induction extend the generator bounds to the full ring and yield descended derivations.

theorem OAI.AbhyankarSathaye.CommutingDerivations.derivation_preserves_polynomial_image line 20
Source documentation
Leibniz extends a closure proof on the literal polynomial generators to the whole polynomial ring. No finite-variable or domain assumption is needed.
```
theorem derivation_preserves_polynomial_image [Algebra K L]
    (ι : MvPolynomial σ K →ₐ[K] L) (D : Derivation K L L)
    (hX : ∀ j : σ, ∃ q : MvPolynomial σ K, ι q = D (ι (X j))) :
    ∀ p : MvPolynomial σ K, ∃ q : MvPolynomial σ K, ι q = D (ι p) := by
…
```
Mentions: OAI.AbhyankarSathaye.p
theorem OAI.AbhyankarSathaye.CommutingDerivations.finite_localization_denominator_bound line 46
Source documentation
One exponent clears any finite collection of localization elements. The proof selects actual numerators and takes the finite maximum of exponents. It remains valid when the original coefficient ring has zero divisors.
```
theorem finite_localization_denominator_bound (c : MvPolynomial σ K)
    [IsLocalization.Away c L] (z : τ → σ → L) :
    ∃ N : ℕ, ∀ (i : τ) (j : σ), ∃ a : MvPolynomial σ K,
      algebraMap (MvPolynomial σ K) L a =
        (algebraMap (MvPolynomial σ K) L c)^N * z i j := by
…
```

theorem OAI.AbhyankarSathaye.CommutingDerivations.exists_common_denominator_descent line 72

Source documentation

Construct descended derivations with a common clearing exponent, assuming injectivity of the localization map.

theorem exists_common_denominator_descent (c : MvPolynomial σ K)
    [IsLocalization.Away c L]
    (hinj : Function.Injective (algebraMap (MvPolynomial σ K) L))
    (D : τ → Derivation K L L) :
    ∃ (N : ℕ) (d : τ → Derivation K (MvPolynomial σ K) (MvPolynomial σ K)),
      ∀ (i : τ) (p : MvPolynomial σ K),
        algebraMap (MvPolynomial σ K) L (d i p) =
          (algebraMap (MvPolynomial σ K) L c)^N *
            D i (algebraMap (MvPolynomial σ K) L p) := by
…

Mentions: OAI.AbhyankarSathaye.p