Rectifiability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The coordinate obstruction and rectifiability of every fiber

The ambient algebra automorphisms in this file are arbitrary complex algebra automorphisms. In particular, there is no restriction to a chosen subgroup or triangular form. The scalar-image characterization keeps the nonzero scalar which occurs when generators of two equal principal ideals are compared.

theorem OAI.StableCoordinate.rectifiableFiber_iff_affine_image line 22
Source documentation
Rectifiability is equivalent to sending f to an affine-linear polynomial in the first coordinate, with nonzero linear coefficient.
```
theorem rectifiableFiber_iff_affine_image (t : ℂ) :
    IsRectifiableFiber t ↔
      ∃ (φ : R 4 ≃ₐ[ℂ] R 4) (c : ℂ), c ≠ 0 ∧
        φ f = C c * X 0 + C t := by
…
```
Mentions: OAI.StableCoordinate.IsRectifiableFiber, OAI.StableCoordinate.R, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.rectifiableFiber_iff_coordinate line 47
Source documentation
For every complex level, rectifiability of the defining hypersurface ideal is equivalent to the coordinate property of the original polynomial.
```
theorem rectifiableFiber_iff_coordinate (t : ℂ) :
    IsRectifiableFiber t ↔ IsCoordinate (by decide : 0 < 4) f := by
…
```
Mentions: OAI.StableCoordinate.IsRectifiableFiber, OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.noncoordinate_implies_all_fibers_nonrectifiable line 61
Source documentation
The four-variable coordinate obstruction forbids rectification at every complex level, with no exclusion of zero or exceptional fibers.
```
theorem noncoordinate_implies_all_fibers_nonrectifiable
    (h : ¬ IsCoordinate (by decide : 0 < 4) f) :
    ∀ t : ℂ, ¬ IsRectifiableFiber t := by
…
```
Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.IsRectifiableFiber
theorem OAI.StableCoordinate.fiberPackage_of_noncoordinate_of_affine line 69
Source documentation
The all-fiber geometric package follows from actual coordinate-algebra isomorphisms and the four-variable coordinate obstruction.
```
theorem fiberPackage_of_noncoordinate_of_affine
    (h : ¬ IsCoordinate (by decide : 0 < 4) f)
    (hFibers : ∀ t : ℂ, IsAffineThreeSpaceFiber t) : FiberPackage := by
…
```
Mentions: OAI.StableCoordinate.IsCoordinate, OAI.StableCoordinate.f, OAI.StableCoordinate.IsAffineThreeSpaceFiber, OAI.StableCoordinate.FiberPackage