OAI/AlgebraicGeometry/StableCoordinate/DeterminantRing.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The determinant ring used in the coordinate obstruction

The independent variables are ordered a,d,b,c,u. The only relation is a*c-b*d=1. This module records the quotient and its elementary universal property; it makes no domain, localization, or rigidity assertion by assumption.

  1. abbrev OAI.StableCoordinate.DeterminantRing.P line 23
  2. def OAI.StableCoordinate.DeterminantRing.relation line 25
  3. def OAI.StableCoordinate.DeterminantRing.relationIdeal line 26
  4. abbrev OAI.StableCoordinate.DeterminantRing.C line 27
  5. def OAI.StableCoordinate.DeterminantRing.mk line 29
  6. def OAI.StableCoordinate.DeterminantRing.generator line 30
  7. abbrev OAI.StableCoordinate.DeterminantRing.a line 31
  8. abbrev OAI.StableCoordinate.DeterminantRing.d line 32
  9. abbrev OAI.StableCoordinate.DeterminantRing.b line 33
  10. abbrev OAI.StableCoordinate.DeterminantRing.c line 34
  11. abbrev OAI.StableCoordinate.DeterminantRing.u line 35
  12. theorem OAI.StableCoordinate.DeterminantRing.mk_relation line 37
  13. theorem OAI.StableCoordinate.DeterminantRing.determinant_relation line 40
  14. def OAI.StableCoordinate.DeterminantRing.lift line 49

    Source documentation

    The universal homomorphism out of the determinant quotient.

    noncomputable def lift (A D B C U : S) (h : A * C - B * D = 1) :
    DeterminantRing.C k →ₐ[k] S :=
…

    Mentions: OAI.StableCoordinate.DeterminantRing.C

  15. theorem OAI.StableCoordinate.DeterminantRing.lift_mk line 58
  16. theorem OAI.StableCoordinate.DeterminantRing.lift_a line 61
  17. theorem OAI.StableCoordinate.DeterminantRing.lift_d line 63
  18. theorem OAI.StableCoordinate.DeterminantRing.lift_b line 65
  19. theorem OAI.StableCoordinate.DeterminantRing.lift_c line 67
  20. theorem OAI.StableCoordinate.DeterminantRing.lift_u line 69
  21. theorem OAI.StableCoordinate.DeterminantRing.hom_ext line 72
  22. abbrev OAI.StableCoordinate.DeterminantRing.Base line 87

    Source documentation

    The three-variable polynomial subalgebra appearing in the rigidity proof.

    abbrev Base (k : Type*) [CommRing k] := MvPolynomial (Fin 3) k
  23. def OAI.StableCoordinate.DeterminantRing.baseMap line 90

    Source documentation

    The base variables have order a,d,u.

    noncomputable def baseMap : Base k →ₐ[k] DeterminantRing.C k :=
…

    Mentions: OAI.StableCoordinate.DeterminantRing.Base, OAI.StableCoordinate.DeterminantRing.C

  24. instance OAI.StableCoordinate.DeterminantRing.baseAlgebra line 94

    Source documentation

    The canonical polynomial coefficient-algebra structure, induced by baseMap.

    noncomputable instance baseAlgebra : Algebra (Base k) (DeterminantRing.C k) :=
…

    Mentions: OAI.StableCoordinate.DeterminantRing.Base, OAI.StableCoordinate.DeterminantRing.C

  25. instance OAI.StableCoordinate.DeterminantRing.baseScalarTower line 97
  26. theorem OAI.StableCoordinate.DeterminantRing.base_algebraMap line 100
  27. theorem OAI.StableCoordinate.DeterminantRing.baseMap_X0 line 103
  28. theorem OAI.StableCoordinate.DeterminantRing.baseMap_X1 line 104
  29. theorem OAI.StableCoordinate.DeterminantRing.baseMap_X2 line 105