OAI/Algebra/FiniteTensor/KoszulForms.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

First-order Koszul equations and lifting of truncated differential-form cycles.

  1. def OAI.PD4Tensor.firstOrderKoszul line 22
  2. theorem OAI.PD4Tensor.firstOrder_lift line 29
  3. abbrev OAI.PD4Tensor.TruncatedForms.A line 56
  4. abbrev OAI.PD4Tensor.TruncatedForms.Space line 57
  5. def OAI.PD4Tensor.TruncatedForms.D line 59
  6. def OAI.PD4Tensor.TruncatedForms.koszul line 62
  7. def OAI.PD4Tensor.TruncatedForms.mulScalar line 65
  8. def OAI.PD4Tensor.TruncatedForms.residueForm line 68
  9. theorem OAI.PD4Tensor.TruncatedForms.residueForm_tmul line 73
  10. theorem OAI.PD4Tensor.TruncatedForms.stokes line 80
  11. theorem OAI.PD4Tensor.TruncatedForms.D_sq_zero line 87
  12. theorem OAI.PD4Tensor.TruncatedForms.D_mul line 91
  13. theorem OAI.PD4Tensor.TruncatedForms.closed_mul_exact_residue line 97
  14. theorem OAI.PD4Tensor.TruncatedForms.koszul_sq_zero line 106
  15. theorem OAI.PD4Tensor.TruncatedForms.D_koszul line 113
  16. theorem OAI.PD4Tensor.TruncatedForms.mulScalar_koszul line 122
  17. theorem OAI.PD4Tensor.TruncatedForms.D_mulScalar line 132
  18. theorem OAI.PD4Tensor.TruncatedForms.lift_cycle line 141