OAI/AlgebraicGeometry/StableCoordinate/StabilizedQuotient.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Eliminating the last linear relation in the stabilization

The variables of the six-variable ring are ordered p,s,u,L,N,w. The quotient by L-u+p*w is the polynomial algebra on p,s,u,N,w. This file gives an actual algebra equivalence, including its effect on p.

  1. abbrev OAI.StableCoordinate.StabilizedQuotient.P line 19
  2. abbrev OAI.StableCoordinate.StabilizedQuotient.S line 20
  3. def OAI.StableCoordinate.StabilizedQuotient.equation line 22
  4. def OAI.StableCoordinate.StabilizedQuotient.equationIdeal line 24
  5. abbrev OAI.StableCoordinate.StabilizedQuotient.A line 26
  6. def OAI.StableCoordinate.StabilizedQuotient.evaluate line 28
  7. theorem OAI.StableCoordinate.StabilizedQuotient.evaluate_equation line 31
  8. def OAI.StableCoordinate.StabilizedQuotient.out line 34
  9. def OAI.StableCoordinate.StabilizedQuotient.into line 44
  10. theorem OAI.StableCoordinate.StabilizedQuotient.out_mk line 51
  11. theorem OAI.StableCoordinate.StabilizedQuotient.quotient_equation line 53
  12. theorem OAI.StableCoordinate.StabilizedQuotient.out_comp_into line 56
  13. theorem OAI.StableCoordinate.StabilizedQuotient.into_comp_out line 61
  14. def OAI.StableCoordinate.StabilizedQuotient.equiv line 74

    Source documentation

    The quotient by L-u+p*w is the five-variable polynomial algebra.

    def equiv : A ≃ₐ[ℂ] S :=
…

    Mentions: OAI.StableCoordinate.StabilizedQuotient.A, OAI.StableCoordinate.StabilizedQuotient.S

  15. theorem OAI.StableCoordinate.StabilizedQuotient.equiv_mk line 77
  16. theorem OAI.StableCoordinate.StabilizedQuotient.equiv_p line 79