OAI/AlgebraicGeometry/StableCoordinate/Presentation.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Polynomial presentation, with arbitrary additional independent variables

The source variables in P n are p,s,u,F,J, in that order, followed by n independent variables. The matrix transformation leaves those extra variables fixed. In particular n=0 gives the unstabilized presentation and n=1 supplies the presentation needed in the one-variable stabilization.

  1. abbrev OAI.StableCoordinate.Presentation.P line 23
  2. def OAI.StableCoordinate.Presentation.p line 25
  3. def OAI.StableCoordinate.Presentation.s line 26
  4. def OAI.StableCoordinate.Presentation.u line 27
  5. def OAI.StableCoordinate.Presentation.F line 28
  6. def OAI.StableCoordinate.Presentation.J line 29
  7. def OAI.StableCoordinate.Presentation.x line 30
  8. def OAI.StableCoordinate.Presentation.H line 31
  9. def OAI.StableCoordinate.Presentation.relationIdeal line 32
  10. abbrev OAI.StableCoordinate.Presentation.A line 33
  11. def OAI.StableCoordinate.Presentation.changeCoords line 35
  12. def OAI.StableCoordinate.Presentation.changeHom line 41
  13. lemma OAI.StableCoordinate.Presentation.changeHom_C line 44
  14. lemma OAI.StableCoordinate.Presentation.changeHom_X_left line 47
  15. lemma OAI.StableCoordinate.Presentation.changeHom_X_right line 51
  16. lemma OAI.StableCoordinate.Presentation.changeHom_p line 55
  17. lemma OAI.StableCoordinate.Presentation.changeHom_s line 58
  18. lemma OAI.StableCoordinate.Presentation.changeHom_u line 61
  19. lemma OAI.StableCoordinate.Presentation.changeHom_F line 64
  20. lemma OAI.StableCoordinate.Presentation.changeHom_J line 67
  21. lemma OAI.StableCoordinate.Presentation.changeHom_comp line 70
  22. lemma OAI.StableCoordinate.Presentation.changeHom_zero line 80
  23. def OAI.StableCoordinate.Presentation.matrixEquiv line 89

    Source documentation

    The source's inverse matrix substitution, regarded as an algebra automorphism. It carries the original hypersurface equation to -J-u.

    def matrixEquiv (n : ℕ) : P n ≃ₐ[ℂ] P n :=
…

    Mentions: OAI.StableCoordinate.Presentation.P

  24. lemma OAI.StableCoordinate.Presentation.matrixEquiv_apply line 94
  25. lemma OAI.StableCoordinate.Presentation.matrixEquiv_symm_apply line 97
  26. lemma OAI.StableCoordinate.Presentation.matrixEquiv_H line 100
  27. lemma OAI.StableCoordinate.Presentation.matrixEquiv_x line 103
  28. def OAI.StableCoordinate.Presentation.eliminateHom line 108

    Source documentation

    Set the transformed variable u equal to -J and retain all other variables.

    def eliminateHom (n : ℕ) : P n →ₐ[ℂ] R (4 + n) :=
…

    Mentions: OAI.StableCoordinate.Presentation.P, OAI.StableCoordinate.R

  29. def OAI.StableCoordinate.Presentation.includeHom line 115

    Source documentation

    Include the four retained variables and all the extra variables.

    def includeHom (n : ℕ) : R (4 + n) →ₐ[ℂ] P n :=
…

    Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Presentation.P

  30. lemma OAI.StableCoordinate.Presentation.eliminateHom_p line 118
  31. lemma OAI.StableCoordinate.Presentation.eliminateHom_s line 120
  32. lemma OAI.StableCoordinate.Presentation.eliminateHom_u line 122
  33. lemma OAI.StableCoordinate.Presentation.eliminateHom_F line 124
  34. lemma OAI.StableCoordinate.Presentation.eliminateHom_J line 126
  35. lemma OAI.StableCoordinate.Presentation.eliminateHom_X_right line 129
  36. lemma OAI.StableCoordinate.Presentation.includeHom_X_right line 132
  37. lemma OAI.StableCoordinate.Presentation.eliminateHom_includeHom line 136
  38. def OAI.StableCoordinate.Presentation.mk line 145

    Source documentation

    Quotient projection for the source hypersurface.

    def mk (n : ℕ) : P n →ₐ[ℂ] A n := Ideal.Quotient.mkₐ ℂ (relationIdeal n)

    Mentions: OAI.StableCoordinate.Presentation.P, OAI.StableCoordinate.Presentation.A, OAI.StableCoordinate.Presentation.relationIdeal

  39. lemma OAI.StableCoordinate.Presentation.mk_H line 147
  40. def OAI.StableCoordinate.Presentation.polynomialMap line 152

    Source documentation

    Evaluation in the explicit four-variable polynomial presentation.

    def polynomialMap (n : ℕ) : P n →ₐ[ℂ] R (4+n) :=
…

    Mentions: OAI.StableCoordinate.Presentation.P, OAI.StableCoordinate.R

  41. lemma OAI.StableCoordinate.Presentation.polynomialMap_H line 155
  42. def OAI.StableCoordinate.Presentation.toPolynomial line 161

    Source documentation

    The source quotient maps to the four-variable polynomial presentation.

    def toPolynomial (n : ℕ) : A n →ₐ[ℂ] R (4+n) :=
…

    Mentions: OAI.StableCoordinate.Presentation.A, OAI.StableCoordinate.R

  43. lemma OAI.StableCoordinate.Presentation.toPolynomial_mk line 166
  44. def OAI.StableCoordinate.Presentation.fromPolynomial line 170

    Source documentation

    The inverse polynomial presentation uses the forward matrix coordinates upstairs.

    def fromPolynomial (n : ℕ) : R (4+n) →ₐ[ℂ] A n :=
…

    Mentions: OAI.StableCoordinate.R, OAI.StableCoordinate.Presentation.A

  45. lemma OAI.StableCoordinate.Presentation.toPolynomial_fromPolynomial line 173
  46. lemma OAI.StableCoordinate.Presentation.mk_matrix_symm_include_eliminate line 182
  47. lemma OAI.StableCoordinate.Presentation.fromPolynomial_toPolynomial line 204
  48. def OAI.StableCoordinate.Presentation.polynomialPresentation line 217

    Source documentation

    Proposition 2.1, stable under adjoining any number of independent variables.

    def polynomialPresentation (n : ℕ) : A n ≃ₐ[ℂ] R (4+n) :=
…

    Mentions: OAI.StableCoordinate.Presentation.A, OAI.StableCoordinate.R

  49. lemma OAI.StableCoordinate.Presentation.polynomialPresentation_mk line 221
  50. lemma OAI.StableCoordinate.Presentation.polynomialPresentation_p line 227

    Source documentation

    The distinguished source variable is exactly the polynomial in the question, renamed into the first four variables; the extra variables are not involved.

    lemma polynomialPresentation_p (n : ℕ) :
    polynomialPresentation n (mk n (p n)) =
      MvPolynomial.rename (Fin.castAdd n : Fin 4 → Fin (4+n)) StableCoordinate.f := by
…

    Mentions: OAI.StableCoordinate.Presentation.polynomialPresentation, OAI.StableCoordinate.Presentation.mk, OAI.StableCoordinate.Presentation.p, OAI.StableCoordinate.f

  51. lemma OAI.StableCoordinate.Presentation.polynomialPresentation_extra line 234
  52. abbrev OAI.StableCoordinate.Presentation.originalPresentation line 239

    Source documentation

    The unstabilized polynomial presentation.

    abbrev originalPresentation : A 0 ≃ₐ[ℂ] R 4 := polynomialPresentation 0

    Mentions: OAI.StableCoordinate.Presentation.A, OAI.StableCoordinate.R, OAI.StableCoordinate.Presentation.polynomialPresentation

  53. lemma OAI.StableCoordinate.Presentation.originalPresentation_p line 241
  54. abbrev OAI.StableCoordinate.Presentation.stabilizedPresentation line 245

    Source documentation

    The same presentation after adjoining one independent variable.

    abbrev stabilizedPresentation : A 1 ≃ₐ[ℂ] R 5 := polynomialPresentation 1

    Mentions: OAI.StableCoordinate.Presentation.A, OAI.StableCoordinate.R, OAI.StableCoordinate.Presentation.polynomialPresentation

  55. lemma OAI.StableCoordinate.Presentation.stabilizedPresentation_p line 247