ParameterRetraction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

An explicit retraction proves saturation of the subring generated by F + 1.

theorem OAI.AbhyankarSathaye.CommutingDerivations.retract_power_saturated line 15

Source documentation

A retract of a domain is saturated by powers of any nonzero element of the retract. The maps and their left-inverse law are explicit hypotheses.

theorem retract_power_saturated {A B : Type*} [CommRing A] [IsDomain A]
    [CommRing B] (ι : B →+* A) (ρ : A →+* B)
    (hρι : ∀ b, ρ (ι b) = b) (b q : B) (a : A) (n : ℕ)
    (hb : ι b ≠ 0) (he : (ι b)^n * a = ι q) : a = ι (ρ a) := by
…

def OAI.AbhyankarSathaye.CommutingDerivations.ambientParameter line 27
Source documentation
The parameter inverted in the localization, F + 1.
```
def ambientParameter : R := F + 1
```
Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.F
def OAI.AbhyankarSathaye.CommutingDerivations.parameterSlice line 30
Source documentation
Restriction to the line (h,u,v,w)=(t,0,0,0).
```
def parameterSlice : R →ₐ[ℂ] Polynomial ℂ :=
…
```
Mentions: OAI.AbhyankarSathaye.R
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameterSlice_parameter line 33
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameterSlice_aeval line 36
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameterSlice_aeval_apply line 41
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_aeval_injective line 45
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_ne_zero line 51
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_power_saturated line 57
Source documentation
Exact polynomial witness for descent from a Laurent expression.
```
theorem parameter_power_saturated (a : R) (q : Polynomial ℂ) (n : ℕ)
    (he : ambientParameter^n * a = Polynomial.aeval ambientParameter q) :
    a = Polynomial.aeval ambientParameter (parameterSlice a) := by
…
```
Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.CommutingDerivations.ambientParameter, OAI.AbhyankarSathaye.CommutingDerivations.parameterSlice
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_localization_injective line 69
theorem OAI.AbhyankarSathaye.CommutingDerivations.parameter_laurent_intersection line 80
Source documentation
Exact intersection with the ambient ring, in denominator-cleared form. The left side says that the localized image has a Laurent expression in c. The right side supplies an ordinary polynomial expression in c. There is no fraction-field-intersection hypothesis.
```
theorem parameter_laurent_intersection (L : Type*) [CommRing L] [Algebra R L]
    [IsLocalization.Away ambientParameter L] (a : R) :
    (∃ (n : ℕ) (q : Polynomial ℂ),
      (algebraMap R L ambientParameter)^n * algebraMap R L a =
        algebraMap R L (Polynomial.aeval ambientParameter q)) ↔
    ∃ q : Polynomial ℂ, a = Polynomial.aeval ambientParameter q := by
…
```
Mentions: OAI.AbhyankarSathaye.R, OAI.AbhyankarSathaye.CommutingDerivations.ambientParameter