OAI/AlgebraicGeometry/StableCoordinate/ObstructionDefinitions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Exact rings in the noncoordinate obstruction

These transparent definitions fix the independent variables and relations in Sections 2–5 of the paper. The relations define the quadric and determinant rings used to obstruct polynomial coordinateness.

  1. abbrev OAI.StableCoordinate.Obstruction.P line 19
  2. def OAI.StableCoordinate.Obstruction.xP line 24

    Source documentation

    The source's determinant invariant in k[p,s,u,F,J].

    noncomputable def xP : P k 5 := X 1 ^ 2 - X 2 ^ 2 + X 0 * X 3

    Mentions: OAI.StableCoordinate.Obstruction.P

  3. def OAI.StableCoordinate.Obstruction.Hstar line 27

    Source documentation

    Highest weighted part of the source hypersurface equation.

    noncomputable def Hstar : P k 5 :=
…

    Mentions: OAI.StableCoordinate.Obstruction.P

  4. def OAI.StableCoordinate.Obstruction.H line 30
  5. def OAI.StableCoordinate.Obstruction.idealA line 31
  6. def OAI.StableCoordinate.Obstruction.idealG line 32
  7. abbrev OAI.StableCoordinate.Obstruction.A line 33
  8. abbrev OAI.StableCoordinate.Obstruction.G line 34
  9. def OAI.StableCoordinate.Obstruction.aX line 37

    Source documentation

    Generator images of the original polynomial presentation.

    noncomputable def aX (i : Fin 5) : A k := Ideal.Quotient.mk (idealA k) (X i)

    Mentions: OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.Obstruction.idealA

  10. def OAI.StableCoordinate.Obstruction.gX line 39

    Source documentation

    Generator images of the weighted degeneration presentation.

    noncomputable def gX (i : Fin 5) : G k := Ideal.Quotient.mk (idealG k) (X i)

    Mentions: OAI.StableCoordinate.Obstruction.G, OAI.StableCoordinate.Obstruction.idealG

  11. def OAI.StableCoordinate.Obstruction.quadricRelation line 41
  12. def OAI.StableCoordinate.Obstruction.idealB line 42
  13. abbrev OAI.StableCoordinate.Obstruction.B line 43
  14. def OAI.StableCoordinate.Obstruction.bX line 45

    Source documentation

    Quadric variables x,y,z,u, in this order.

    noncomputable def bX (i : Fin 4) : B k := Ideal.Quotient.mk (idealB k) (X i)

    Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.idealB

  15. def OAI.StableCoordinate.Obstruction.determinantRelation line 47
  16. def OAI.StableCoordinate.Obstruction.idealC line 48
  17. abbrev OAI.StableCoordinate.Obstruction.C line 49
  18. def OAI.StableCoordinate.Obstruction.cX line 51

    Source documentation

    Determinant-ring variables a,d,b,c,u, in this order.

    noncomputable def cX (i : Fin 5) : C k := Ideal.Quotient.mk (idealC k) (X i)

    Mentions: OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.idealC

  19. def OAI.StableCoordinate.Obstruction.sB line 53
  20. def OAI.StableCoordinate.Obstruction.f0 line 54
  21. def OAI.StableCoordinate.Obstruction.g0 line 55
  22. def OAI.StableCoordinate.Obstruction.I line 56
  23. def OAI.StableCoordinate.Obstruction.v line 57
  24. def OAI.StableCoordinate.Obstruction.presentationWeight line 60

    Source documentation

    The exact negative integer weights on the presentation variables.

    def presentationWeight : Fin 5 → ℤ := ![-1, 0, 0, 1, 1]
  25. def OAI.StableCoordinate.Obstruction.fiberWeight line 62

    Source documentation

    Fiber weights on a,d,b,c,u; these encode fiber scaling.

    def fiberWeight : Fin 5 → ℤ := ![1, 1, -1, -1, 0]
  26. def OAI.StableCoordinate.Obstruction.auxiliaryWeight line 64

    Source documentation

    The second, auxiliary grading used only in the rigidity argument.

    def auxiliaryWeight : Fin 5 → ℤ := ![0, 1, -1, 0, 1]
  27. theorem OAI.StableCoordinate.Obstruction.mk_H line 66
  28. theorem OAI.StableCoordinate.Obstruction.mk_Hstar line 70
  29. theorem OAI.StableCoordinate.Obstruction.b_relation line 74
  30. theorem OAI.StableCoordinate.Obstruction.c_relation line 80