OAI/Geometry/Anticanonical/DeletedFaces.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Deleted-face retractions and preliminaries for anticanonical indices

The coordinate invariant Dolbeault index is defined, with high-degree vanishing proved. The deleted-face deformation retraction and contractibility are supporting results, alongside positive-weight lattice fibers, compactness, polarization and polynomial continuation. No theorem identifies this geometric index with a polynomial: Euler-characteristic cancellation, equivariant Dolbeault localization and the weighted Ehrhart step remain unproved. The metric and direct-image arguments for pseudoeffective-error conversion are also absent.

  1. abbrev OAI.AnticanonicalIndex.Geometry.Space line 23
  2. structure OAI.AnticanonicalIndex.Geometry.Atlas line 25
  3. def OAI.AnticanonicalIndex.Geometry.Atlas.transition line 34
  4. def OAI.AnticanonicalIndex.Geometry.Atlas.overlap line 37
  5. def OAI.AnticanonicalIndex.Geometry.jacobian line 40
  6. def OAI.AnticanonicalIndex.Geometry.antiDir line 43
  7. abbrev OAI.AnticanonicalIndex.Geometry.Coefficients line 46
  8. def OAI.AnticanonicalIndex.Geometry.pullCoefficient line 48
  9. def OAI.AnticanonicalIndex.Geometry.AlternatingCoefficients line 53
  10. def OAI.AnticanonicalIndex.Geometry.IsForm line 58
  11. def OAI.AnticanonicalIndex.Geometry.dbar line 66
  12. def OAI.AnticanonicalIndex.Geometry.IsClosedForm line 71
  13. def OAI.AnticanonicalIndex.Geometry.IsExact line 74
  14. structure OAI.AnticanonicalIndex.Geometry.Torus line 80
  15. def OAI.AnticanonicalIndex.Geometry.Torus.exp line 83
  16. structure OAI.AnticanonicalIndex.Geometry.HolomorphicAction line 87
  17. def OAI.AnticanonicalIndex.Geometry.HolomorphicAction.coordinateMap line 104
  18. def OAI.AnticanonicalIndex.Geometry.HolomorphicAction.coordinateDomain line 108
  19. def OAI.AnticanonicalIndex.Geometry.IsInvariantClass line 112
  20. def OAI.AnticanonicalIndex.Geometry.invariantCycles line 119
  21. def OAI.AnticanonicalIndex.Geometry.exactForms line 123
  22. abbrev OAI.AnticanonicalIndex.Geometry.InvariantDolbeault line 126
  23. def OAI.AnticanonicalIndex.Geometry.invariantIndex line 130
  24. lemma OAI.AnticanonicalIndex.Geometry.form_eq_zero_of_dimension_lt line 134
  25. lemma OAI.AnticanonicalIndex.Geometry.invariantCycles_eq_bot_of_dimension_lt line 143
  26. theorem OAI.AnticanonicalIndex.Geometry.invariantDolbeault_finrank_eq_zero_of_dimension_lt line 150
  27. def OAI.AnticanonicalIndex.DeletedFaces.vertex line 175
  28. def OAI.AnticanonicalIndex.DeletedFaces.domain line 177
  29. def OAI.AnticanonicalIndex.DeletedFaces.boundary line 180
  30. lemma OAI.AnticanonicalIndex.DeletedFaces.boundary_subset_domain line 183
  31. lemma OAI.AnticanonicalIndex.DeletedFaces.convex_domain line 186
  32. def OAI.AnticanonicalIndex.DeletedFaces.inclusion line 193
  33. def OAI.AnticanonicalIndex.DeletedFaces.entryTime line 197
  34. lemma OAI.AnticanonicalIndex.DeletedFaces.inv_le_entryTime line 201
  35. lemma OAI.AnticanonicalIndex.DeletedFaces.entryTime_pos line 206
  36. lemma OAI.AnticanonicalIndex.DeletedFaces.entryTime_le_one line 212
  37. lemma OAI.AnticanonicalIndex.DeletedFaces.continuous_entryTime line 218
  38. def OAI.AnticanonicalIndex.DeletedFaces.retractPoint line 227
  39. lemma OAI.AnticanonicalIndex.DeletedFaces.retractPoint_mem line 231
  40. lemma OAI.AnticanonicalIndex.DeletedFaces.entryTime_eq_one line 260
  41. lemma OAI.AnticanonicalIndex.DeletedFaces.retractPoint_fixed line 266
  42. lemma OAI.AnticanonicalIndex.DeletedFaces.continuous_retractPoint line 270
  43. def OAI.AnticanonicalIndex.DeletedFaces.retraction line 275
  44. lemma OAI.AnticanonicalIndex.DeletedFaces.retraction_inclusion line 280
  45. def OAI.AnticanonicalIndex.DeletedFaces.retractionHomotopy line 285
  46. theorem OAI.AnticanonicalIndex.DeletedFaces.deleted_faces_deformation_retract line 305
  47. def OAI.AnticanonicalIndex.DeletedFaces.homotopyEquiv line 313
  48. theorem OAI.AnticanonicalIndex.DeletedFaces.deleted_faces_contractible line 324
  49. def OAI.AnticanonicalIndex.PositiveWeights.equation line 335
  50. lemma OAI.AnticanonicalIndex.PositiveWeights.pair_equation line 340
  51. lemma OAI.AnticanonicalIndex.PositiveWeights.coordinate_bound line 344
  52. theorem OAI.AnticanonicalIndex.PositiveWeights.zero_fiber line 351
  53. theorem OAI.AnticanonicalIndex.PositiveWeights.zero_fiber_with_deleted_faces line 359
  54. theorem OAI.AnticanonicalIndex.PositiveWeights.nonnegative_integral_fiber_finite line 372
  55. def OAI.AnticanonicalIndex.PositiveWeights.latticeFiber line 383
  56. lemma OAI.AnticanonicalIndex.PositiveWeights.latticeFiber_finite line 386
  57. lemma OAI.AnticanonicalIndex.PositiveWeights.mem_latticeFiber_zero line 391
  58. theorem OAI.AnticanonicalIndex.PositiveWeights.weighted_count_at_zero line 406
  59. theorem OAI.AnticanonicalIndex.DeletedFaces.domain_compact line 435
  60. theorem OAI.AnticanonicalIndex.DeletedFaces.boundary_compact line 452
  61. def OAI.AnticanonicalIndex.Polarization.weights line 471
  62. def OAI.AnticanonicalIndex.Polarization.character line 474
  63. lemma OAI.AnticanonicalIndex.Polarization.anticanonical_equation line 476
  64. lemma OAI.AnticanonicalIndex.Polarization.positive line 484
  65. lemma OAI.AnticanonicalIndex.Polarization.domain_nonempty_of_no_deletions line 491
  66. lemma OAI.AnticanonicalIndex.PolynomialContinuation.progression_injective line 502
  67. theorem OAI.AnticanonicalIndex.PolynomialContinuation.unique line 508
  68. theorem OAI.AnticanonicalIndex.PolynomialContinuation.rational_of_integral_values line 516