OAI/AlgebraicGeometry/Seshadri/Nodal/NodalIntersection.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.NodalLocal.multiples line 20
  2. theorem OAI.MaximalSeshadri.NodalLocal.mem_multiples line 23
  3. def OAI.MaximalSeshadri.NodalLocal.nodeAlgebra line 28
  4. abbrev OAI.MaximalSeshadri.NodalLocal.Node line 42
  5. def OAI.MaximalSeshadri.NodalLocal.branchX line 44
  6. def OAI.MaximalSeshadri.NodalLocal.branchZ line 52
  7. theorem OAI.MaximalSeshadri.NodalLocal.node_ext line 60
  8. lemma OAI.MaximalSeshadri.NodalLocal.branch_constant line 64
  9. def OAI.MaximalSeshadri.NodalLocal.includeX line 67
  10. theorem OAI.MaximalSeshadri.NodalLocal.branchX_includeX line 72
  11. theorem OAI.MaximalSeshadri.NodalLocal.branchZ_includeX line 74
  12. def OAI.MaximalSeshadri.NodalLocal.liftZ line 77
  13. theorem OAI.MaximalSeshadri.NodalLocal.branchX_liftZ line 90
  14. theorem OAI.MaximalSeshadri.NodalLocal.branchZ_liftZ line 92
  15. theorem OAI.MaximalSeshadri.NodalLocal.range_includeX_eq_ker_branchZ line 95
  16. lemma OAI.MaximalSeshadri.NodalLocal.includeX_mul line 108
  17. def OAI.MaximalSeshadri.NodalLocal.coefficientJet line 112
  18. lemma OAI.MaximalSeshadri.NodalLocal.coefficientJet_apply line 115
  19. lemma OAI.MaximalSeshadri.NodalLocal.coefficientJet_surjective line 118
  20. lemma OAI.MaximalSeshadri.NodalLocal.ker_coefficientJet line 124
  21. lemma OAI.MaximalSeshadri.NodalLocal.multiples_eq_order line 135
  22. def OAI.MaximalSeshadri.NodalLocal.branchQuotientEquiv line 150
  23. lemma OAI.MaximalSeshadri.NodalLocal.finite_branch_quotient line 157
  24. lemma OAI.MaximalSeshadri.NodalLocal.finrank_branch_quotient line 162
  25. def OAI.MaximalSeshadri.NodalLocal.quotientZ line 167
  26. lemma OAI.MaximalSeshadri.NodalLocal.quotientZ_mk line 178
  27. def OAI.MaximalSeshadri.NodalLocal.quotientX line 181
  28. lemma OAI.MaximalSeshadri.NodalLocal.quotientX_mk line 192
  29. lemma OAI.MaximalSeshadri.NodalLocal.quotientZ_surjective line 195
  30. lemma OAI.MaximalSeshadri.NodalLocal.quotientX_injective line 201
  31. lemma OAI.MaximalSeshadri.NodalLocal.branch_quotient_exact line 229
  32. lemma OAI.MaximalSeshadri.NodalLocal.finite_node_quotient line 259
  33. theorem OAI.MaximalSeshadri.NodalLocal.finrank_node_quotient line 266
  34. abbrev OAI.MaximalSeshadri.NodalLocal.Bivariate line 280
  35. def OAI.MaximalSeshadri.NodalLocal.constAlg line 282
  36. def OAI.MaximalSeshadri.NodalLocal.restrictX line 286
  37. def OAI.MaximalSeshadri.NodalLocal.restrictZ line 290
  38. lemma OAI.MaximalSeshadri.NodalLocal.restrictX_apply line 293
  39. lemma OAI.MaximalSeshadri.NodalLocal.restrictZ_apply line 294
  40. lemma OAI.MaximalSeshadri.NodalLocal.restrict_constants line 297
  41. def OAI.MaximalSeshadri.NodalLocal.toNode line 302
  42. lemma OAI.MaximalSeshadri.NodalLocal.branchX_toNode line 317
  43. lemma OAI.MaximalSeshadri.NodalLocal.branchZ_toNode line 319
  44. lemma OAI.MaximalSeshadri.NodalLocal.toNode_surjective line 322
  45. def OAI.MaximalSeshadri.NodalLocal.nodeEquation line 339
  46. lemma OAI.MaximalSeshadri.NodalLocal.toNode_nodeEquation line 341
  47. theorem OAI.MaximalSeshadri.NodalLocal.toNode_eq_zero_iff line 344
  48. lemma OAI.MaximalSeshadri.NodalLocal.ker_toNode line 371
  49. def OAI.MaximalSeshadri.NodalLocal.nodePresentation line 377
  50. def OAI.MaximalSeshadri.NodalLocal.intersectionIdeal line 382
  51. def OAI.MaximalSeshadri.NodalLocal.intersectionRestriction line 385
  52. lemma OAI.MaximalSeshadri.NodalLocal.intersectionRestriction_surjective line 389
  53. lemma OAI.MaximalSeshadri.NodalLocal.ker_intersectionRestriction line 393
  54. def OAI.MaximalSeshadri.NodalLocal.intersectionQuotientEquiv line 413
  55. lemma OAI.MaximalSeshadri.NodalLocal.finite_intersection_quotient line 422
  56. theorem OAI.MaximalSeshadri.NodalLocal.nodal_intersection_colength line 429
  57. lemma OAI.MaximalSeshadri.LocalComparison.map_nodal_intersection_ideal line 450
  58. theorem OAI.MaximalSeshadri.LocalComparison.actual_nodal_intersection_colength line 458
  59. theorem OAI.MaximalSeshadri.LocalComparison.actual_nodal_intersection_finite line 479