OAI/AlgebraicGeometry/StableCoordinate/MatrixChange.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The determinant-preserving change in §2

These identities are valid in every commutative ring. The parameter t gives (I - 2t n eᵀ) M, and composition adds parameters. No division by two is needed in the coordinate formulas.

  1. def OAI.StableCoordinate.MatrixChange.quad line 20

    Source documentation

    The negative determinant of the displayed two-by-two matrix.

    def quad (p s u F : K) : K := s ^ 2 - u ^ 2 + p * F
  2. def OAI.StableCoordinate.MatrixChange.pChange line 22
  3. def OAI.StableCoordinate.MatrixChange.sChange line 25
  4. def OAI.StableCoordinate.MatrixChange.uChange line 28
  5. def OAI.StableCoordinate.MatrixChange.FChange line 31
  6. def OAI.StableCoordinate.MatrixChange.relation line 35

    Source documentation

    The defining equation of the five-variable hypersurface.

    def relation (p s u F J : K) : K :=
…
  7. lemma OAI.StableCoordinate.MatrixChange.map_quad line 41
  8. lemma OAI.StableCoordinate.MatrixChange.map_pChange line 45
  9. lemma OAI.StableCoordinate.MatrixChange.map_sChange line 49
  10. lemma OAI.StableCoordinate.MatrixChange.map_uChange line 53
  11. lemma OAI.StableCoordinate.MatrixChange.map_FChange line 57
  12. lemma OAI.StableCoordinate.MatrixChange.map_relation line 61
  13. lemma OAI.StableCoordinate.MatrixChange.quad_change line 67
  14. lemma OAI.StableCoordinate.MatrixChange.pChange_add line 73
  15. lemma OAI.StableCoordinate.MatrixChange.sChange_add line 81
  16. lemma OAI.StableCoordinate.MatrixChange.uChange_add line 89
  17. lemma OAI.StableCoordinate.MatrixChange.FChange_add line 97
  18. lemma OAI.StableCoordinate.MatrixChange.pChange_zero line 105
  19. lemma OAI.StableCoordinate.MatrixChange.sChange_zero line 107
  20. lemma OAI.StableCoordinate.MatrixChange.uChange_zero line 109
  21. lemma OAI.StableCoordinate.MatrixChange.FChange_zero line 111
  22. lemma OAI.StableCoordinate.MatrixChange.uChange_one line 114
  23. lemma OAI.StableCoordinate.MatrixChange.relation_change_neg_one line 119