OAI/AlgebraicGeometry/StableCoordinate/ZeroFiberExact.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact polynomial has affine-three-space zero fiber

The proved matrix presentation sends its distinguished parameter to the exact polynomial f. Transporting the explicit zero-fiber coordinate algebra isomorphism therefore completes the zero case of Proposition 2.3 without adding any assumptions to its headline statement.

  1. def OAI.StableCoordinate.zeroFiberEquiv line 20

    Source documentation

    The fiber at zero of the exact degree-five polynomial is affine three-space, expressed as an isomorphism of complex coordinate algebras.

    def zeroFiberEquiv : FiberRing 0 ≃ₐ[ℂ] R 3 :=
…

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

  2. theorem OAI.StableCoordinate.zeroFiber_isAffineThreeSpace line 24