OAI/AlgebraicGeometry/StableCoordinate/ZeroFiber.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The zero-fiber elimination

The quotient by the specialized defining equation of Section 2 is a polynomial algebra in three independent variables. The construction is an algebra isomorphism, not merely a bijection on points, and works over any commutative coefficient ring.

  1. abbrev OAI.StableCoordinate.ZeroFiber.Four line 27
  2. abbrev OAI.StableCoordinate.ZeroFiber.Three line 28
  3. def OAI.StableCoordinate.ZeroFiber.squareDifference line 30
  4. def OAI.StableCoordinate.ZeroFiber.relation line 32
  5. def OAI.StableCoordinate.ZeroFiber.relationIdeal line 35
  6. abbrev OAI.StableCoordinate.ZeroFiber.Ring line 37
  7. def OAI.StableCoordinate.ZeroFiber.qmk line 39
  8. def OAI.StableCoordinate.ZeroFiber.forward line 41
  9. lemma OAI.StableCoordinate.ZeroFiber.forward_relation line 46
  10. lemma OAI.StableCoordinate.ZeroFiber.forward_vanishes line 52
  11. def OAI.StableCoordinate.ZeroFiber.toThree line 61
  12. lemma OAI.StableCoordinate.ZeroFiber.toThree_qmk line 64
  13. def OAI.StableCoordinate.ZeroFiber.backward line 66
  14. lemma OAI.StableCoordinate.ZeroFiber.forward_backward line 70
  15. lemma OAI.StableCoordinate.ZeroFiber.qmk_relation line 75
  16. lemma OAI.StableCoordinate.ZeroFiber.backward_forward line 79
  17. def OAI.StableCoordinate.ZeroFiber.presentationEquiv line 96

    Source documentation

    The zero fiber of the five-generator hypersurface presentation is affine three-space, expressed by an isomorphism of coordinate algebras.

    def presentationEquiv : Ring K ≃ₐ[K] Three K :=
…

    Mentions: OAI.StableCoordinate.ZeroFiber.Ring, OAI.StableCoordinate.ZeroFiber.Three