AllFibers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Every complex fiber of the exact polynomial

The two explicit quotient-algebra calculations cover every parameter, including zero. Together with the noncoordinate theorem, these equivalences show that every fiber is affine three-space and its embedding is nonrectifiable.

theorem OAI.StableCoordinate.all_fibers_isAffineThreeSpace line 19
Source documentation
Every complex fiber of the specified polynomial has the coordinate algebra of affine three-space, with no exceptional parameters.
```
theorem all_fibers_isAffineThreeSpace :
    ∀ t : ℂ, IsAffineThreeSpaceFiber t := by
…
```
Mentions: OAI.StableCoordinate.IsAffineThreeSpaceFiber
def OAI.StableCoordinate.exactFiberEquiv line 28
Source documentation
An actual complex algebra equivalence for each fiber.
```
noncomputable def exactFiberEquiv (t : ℂ) : FiberRing t ≃ₐ[ℂ] R 3 :=
…
```
Mentions: OAI.StableCoordinate.FiberRing, OAI.StableCoordinate.R
theorem OAI.StableCoordinate.fiberPackage_of_noncoordinate line 33
Source documentation
With the unrestricted four-variable coordinate obstruction, the already proved all-fiber calculation supplies the entire geometric principal group.
```
theorem fiberPackage_of_noncoordinate
    (h : ¬ IsCoordinate (by decide : 0 < 4) f) : FiberPackage :=
…
```
Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.FiberPackage