ParameterBridge.lean`

62 declarations, 0 contain sorry, 0 declared as axioms

Explicit relative polynomial coordinates with an invertible parameter.

The coefficient ring is arbitrary, including the zero ring. In the localization application it is the Laurent coefficient ring ℂ[c,c⁻¹]. The relative presentation is explicitly isomorphic to a polynomial algebra in three variables.

def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawH line 23
Source comment
Original independent variable order: h,u,v,w.
```
def rawH : MvPolynomial (Fin 4) K := X 0
```
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawU line 24
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawV line 25
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawW line 26
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawX line 27
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawY line 28
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.rawS line 29
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.relation line 30
abbrev OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.Q line 32
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qmap line 33
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.coeff line 35
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qH line 36
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qU line 37
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qV line 38
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qW line 39
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qX line 40
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qY line 41
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qS line 42
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qAlpha line 43
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qBeta line 45
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.qT line 47
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.quotient_relation line 50
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.quotient_cusp line 61
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.quotient_bezout line 66
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.quotient_recover_s line 73
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeS line 81
Source comment
Free independent variable order: X,Y,T.
```
def freeS (d : K) : MvPolynomial (Fin 3) K := C d*(X 0^2+X 1^3)
```
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeX line 82
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeY line 83
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeH line 84
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeAlpha line 86
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeBeta line 88
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeU line 90
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeG line 92
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeW line 94
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.freeV line 97
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.free_cusp line 100
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.free_bezout line 115
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.free_relations line 121
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.values line 128
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation line 130
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_h line 133
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_u line 135
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_v line 137
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_w line 139
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_x line 141
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_y line 144
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_s line 147
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.evaluation_relation line 151
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.forward line 157
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.forward_qmap line 166
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward line 169
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_X2 line 172
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeS line 175
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeX line 178
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeY line 182
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeH line 186
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeAlpha line 190
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_freeBeta line 194
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_free_original line 199
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.forward_backward line 216
theorem OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.backward_forward line 231
def OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.equivalence line 247
Source documentation
The complete explicit relative bridge. For a Laurent coefficient ring, c is its Laurent variable and d its inverse. Both composites are proved.
```
def equivalence (c d : K) (hunit : c*d=1) :
    Q K c ≃ₐ[K] MvPolynomial (Fin 3) K :=
…
```
Mentions: OAI.AbhyankarSathaye.CommutingDerivations.ParameterBridge.Q