ZeroFiberTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting the zero-fiber calculation through a polynomial presentation

The hypothesis of the helper below is a proved algebra equivalence to be supplied by the matrix-change construction. It does not assert or assume any of the requested headline claims.

def OAI.StableCoordinate.ZeroFiber.zeroFiberEquivOfPresentation line 21
Source documentation
Transport the already calculated zero fiber through a polynomial presentation that takes the distinguished parameter to the exact polynomial. This helper is instantiated by the explicit presentation construction.
```
def zeroFiberEquivOfPresentation
    (e : Hypersurface ℂ ≃ₐ[ℂ] R 4)
    (he : e (hypersurfaceMk ℂ (X 0)) = f) : FiberRing 0 ≃ₐ[ℂ] R 3 :=
…
```
Mentions: OAI.StableCoordinate.ZeroFiber.Hypersurface, OAI.StableCoordinate.R, OAI.StableCoordinate.ZeroFiber.hypersurfaceMk, OAI.StableCoordinate.f, OAI.StableCoordinate.FiberRing