OAI/AlgebraicGeometry/StableCoordinate/NonzeroFiber.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Nonzero fibers of the polynomial hypersurface presentation

Source: sources/build/source/sections/02-construction.tex, especially con:quadric-identity, con:localized-inverse, and prop:fibers.

The variables of P5 K are ordered p,s,u,F,J. This file proves the explicit algebra equivalence

K[p,s,u,F,J] / (H, p-l) ≃ₐ[K] K[x,y,z] for every nonzero l : K.

It uses actual quotient algebras and mutually inverse algebra homomorphisms, not a pointwise bijection. The identities work over any commutative ring with an inverse to p; the quotient construction is stated over any field. The transport from the presentation to the exact four-variable polynomial is supplied separately by the polynomial-presentation equivalence.

  1. def OAI.StableCoordinate.NonzeroFiber.quadric line 33
  2. def OAI.StableCoordinate.NonzeroFiber.relation line 35
  3. def OAI.StableCoordinate.NonzeroFiber.xCoord line 38
  4. def OAI.StableCoordinate.NonzeroFiber.yCoord line 40
  5. def OAI.StableCoordinate.NonzeroFiber.zCoord line 42
  6. theorem OAI.StableCoordinate.NonzeroFiber.quadric_identity line 44
  7. def OAI.StableCoordinate.NonzeroFiber.inverseU line 56
  8. def OAI.StableCoordinate.NonzeroFiber.inverseS line 57
  9. def OAI.StableCoordinate.NonzeroFiber.inverseF line 58
  10. def OAI.StableCoordinate.NonzeroFiber.inverseJ line 59
  11. theorem OAI.StableCoordinate.NonzeroFiber.x_inverse line 61
  12. theorem OAI.StableCoordinate.NonzeroFiber.y_inverse line 67
  13. theorem OAI.StableCoordinate.NonzeroFiber.z_inverse line 76
  14. theorem OAI.StableCoordinate.NonzeroFiber.inverseU_forward line 86
  15. theorem OAI.StableCoordinate.NonzeroFiber.inverseS_forward line 92
  16. theorem OAI.StableCoordinate.NonzeroFiber.inverseF_forward line 100
  17. theorem OAI.StableCoordinate.NonzeroFiber.inverseJ_forward line 111
  18. theorem OAI.StableCoordinate.NonzeroFiber.relation_inverse line 128
  19. abbrev OAI.StableCoordinate.NonzeroFiber.P5 line 160
  20. abbrev OAI.StableCoordinate.NonzeroFiber.P3 line 161
  21. def OAI.StableCoordinate.NonzeroFiber.H line 163
  22. def OAI.StableCoordinate.NonzeroFiber.fiberIdeal line 165
  23. abbrev OAI.StableCoordinate.NonzeroFiber.Fiber line 167
  24. def OAI.StableCoordinate.NonzeroFiber.mk line 169
  25. def OAI.StableCoordinate.NonzeroFiber.decode line 171
  26. def OAI.StableCoordinate.NonzeroFiber.forward line 178
  27. theorem OAI.StableCoordinate.NonzeroFiber.forward_X line 180
  28. theorem OAI.StableCoordinate.NonzeroFiber.forward_C line 183
  29. theorem OAI.StableCoordinate.NonzeroFiber.constants_inv line 186
  30. theorem OAI.StableCoordinate.NonzeroFiber.forward_H line 189
  31. theorem OAI.StableCoordinate.NonzeroFiber.forward_relation line 199
  32. theorem OAI.StableCoordinate.NonzeroFiber.forward_kills line 202
  33. def OAI.StableCoordinate.NonzeroFiber.toPoly line 207
  34. theorem OAI.StableCoordinate.NonzeroFiber.toPoly_mk line 210
  35. def OAI.StableCoordinate.NonzeroFiber.encode line 214
  36. def OAI.StableCoordinate.NonzeroFiber.fromPoly line 219
  37. theorem OAI.StableCoordinate.NonzeroFiber.fromPoly_X line 221
  38. theorem OAI.StableCoordinate.NonzeroFiber.fromPoly_C line 224
  39. theorem OAI.StableCoordinate.NonzeroFiber.mk_H line 235
  40. theorem OAI.StableCoordinate.NonzeroFiber.mk_p line 239
  41. theorem OAI.StableCoordinate.NonzeroFiber.mk_relation line 245
  42. theorem OAI.StableCoordinate.NonzeroFiber.mk_unit line 250
  43. theorem OAI.StableCoordinate.NonzeroFiber.toPoly_fromPoly line 254
  44. theorem OAI.StableCoordinate.NonzeroFiber.fromPoly_toPoly line 273
  45. def OAI.StableCoordinate.NonzeroFiber.nonzeroFiberEquiv line 300

    Source documentation

    The explicit algebraic nonzero-fiber calculation, valid over any field.

    def nonzeroFiberEquiv (l : K) (hl : l≠0) : Fiber l ≃ₐ[K] P3 K :=
…

    Mentions: OAI.StableCoordinate.NonzeroFiber.Fiber, OAI.StableCoordinate.NonzeroFiber.P3