OAI/AlgebraicGeometry/StableCoordinate/DeterminantPrimeA.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The first determinant coordinate is prime

This file proves the exact residual presentation obtained by setting a=0, then its domain property. Consequently a is a prime element of the determinant ring. Combined with the explicit a-chart, this is the algebraic input to the prime-element localization criterion for unique factorization.

  1. def OAI.StableCoordinate.DeterminantPrimeA.residualRelation line 25

    Source documentation

    The residual relation after setting a=0; variables are d,b,c,u.

    def residualRelation : MvPolynomial (Fin 4) k := X 1 * X 0 + 1
  2. def OAI.StableCoordinate.DeterminantPrimeA.residualIdeal line 27
  3. abbrev OAI.StableCoordinate.DeterminantPrimeA.ResidualRing line 28
  4. def OAI.StableCoordinate.DeterminantPrimeA.residualMk line 30
  5. def OAI.StableCoordinate.DeterminantPrimeA.rX line 33
  6. theorem OAI.StableCoordinate.DeterminantPrimeA.residual_relation line 35
  7. def OAI.StableCoordinate.DeterminantPrimeA.aIdeal line 40
  8. abbrev OAI.StableCoordinate.DeterminantPrimeA.ModA line 41
  9. def OAI.StableCoordinate.DeterminantPrimeA.modAMk line 43
  10. theorem OAI.StableCoordinate.DeterminantPrimeA.modAMk_a line 45
  11. theorem OAI.StableCoordinate.DeterminantPrimeA.modA_relation line 48
  12. def OAI.StableCoordinate.DeterminantPrimeA.toResidual line 53
  13. theorem OAI.StableCoordinate.DeterminantPrimeA.toResidual_a line 58
  14. theorem OAI.StableCoordinate.DeterminantPrimeA.toResidual_d line 59
  15. theorem OAI.StableCoordinate.DeterminantPrimeA.toResidual_b line 60
  16. theorem OAI.StableCoordinate.DeterminantPrimeA.toResidual_c line 61
  17. theorem OAI.StableCoordinate.DeterminantPrimeA.toResidual_u line 62
  18. def OAI.StableCoordinate.DeterminantPrimeA.modAToResidual line 64
  19. theorem OAI.StableCoordinate.DeterminantPrimeA.modAToResidual_mk line 72
  20. def OAI.StableCoordinate.DeterminantPrimeA.residualToModA line 75
  21. theorem OAI.StableCoordinate.DeterminantPrimeA.residualToModA_rX line 85
  22. theorem OAI.StableCoordinate.DeterminantPrimeA.residualToModA_comp_modAToResidual line 91
  23. theorem OAI.StableCoordinate.DeterminantPrimeA.modAToResidual_comp_residualToModA line 99
  24. def OAI.StableCoordinate.DeterminantPrimeA.modAEquivResidual line 108

    Source documentation

    Setting a=0 gives the domain presentation k[d,b,c,u]/(bd+1).

    def modAEquivResidual : ModA k ≃ₐ[k] ResidualRing k :=
…

    Mentions: OAI.StableCoordinate.DeterminantPrimeA.ModA, OAI.StableCoordinate.DeterminantPrimeA.ResidualRing

  25. theorem OAI.StableCoordinate.DeterminantPrimeA.residualRelation_irreducible line 116
  26. instance OAI.StableCoordinate.DeterminantPrimeA.residualIdeal_isPrime line 121
  27. instance OAI.StableCoordinate.DeterminantPrimeA.residualRing_isDomain line 124
  28. instance OAI.StableCoordinate.DeterminantPrimeA.modA_isDomain line 126
  29. theorem OAI.StableCoordinate.DeterminantRing.a_prime line 140

    Source documentation

    The first coordinate of the determinant hypersurface is a prime element.

    theorem a_prime : Prime (a k) := by
…

    Mentions: OAI.StableCoordinate.DeterminantRing.a