OAI/AlgebraicGeometry/StableCoordinate/NonzeroFiberAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nonzero fibers of the four-variable polynomial

The matrix presentation identifies its distinguished element with exactly StableCoordinate.f. Composing that presentation with the nonzero-fiber calculation gives an affine coordinate-algebra isomorphism for every nonzero complex parameter.

  1. def OAI.StableCoordinate.exactNonzeroFiberEquiv line 20

    Source documentation

    Every nonzero complex fiber of the exact polynomial has affine-three-space coordinate algebra. The zero fiber is treated in ZeroFiberExact.

    def exactNonzeroFiberEquiv (l : ℂ) (hl : l≠0) : FiberRing l ≃ₐ[ℂ] R 3 :=
…

    Mentions: OAI.StableCoordinate.FiberRing, OAI.StableCoordinate.R

  2. theorem OAI.StableCoordinate.isAffineThreeSpaceFiber_of_ne_zero line 24