OAI/Algebra/FiniteTensor/ChartPairings.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Chart-normal cycles, coordinate reindexing and oriented residue pairings.

  1. def OAI.PD4Tensor.FiniteCoordinates.chartDerivative line 17
  2. def OAI.PD4Tensor.FiniteCoordinates.normalCoordinates line 22
  3. def OAI.PD4Tensor.FiniteCoordinates.chartNormal line 26
  4. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_closed line 32
  5. theorem OAI.PD4Tensor.FiniteCoordinates.normalCoordinates_span line 40
  6. theorem OAI.PD4Tensor.FiniteCoordinates.normalCoordinates_pow line 48
  7. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_ann line 57
  8. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_koszul line 70
  9. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_boundary line 80
  10. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_pair_nonzero line 107
  11. theorem OAI.PD4Tensor.Forms.reindexForms_normalCycle line 155
  12. theorem OAI.PD4Tensor.FiniteCoordinates.renameHom_mk line 175
  13. theorem OAI.PD4Tensor.FiniteCoordinates.reindexEquiv_partial line 192
  14. def OAI.PD4Tensor.FiniteCoordinates.reindexChart line 210
  15. theorem OAI.PD4Tensor.FiniteCoordinates.chartNormal_reindex line 215
  16. theorem OAI.PD4Tensor.TruncatedForms.residueForm_topCoefficient line 246
  17. def OAI.PD4Tensor.FiniteCoordinates.orientedResidue line 266
  18. theorem OAI.PD4Tensor.FiniteCoordinates.orientedResidue_stokes line 271
  19. theorem OAI.PD4Tensor.FiniteCoordinates.orientedResidue_closed_exact line 283
  20. theorem OAI.PD4Tensor.FiniteCoordinates.orientedResidue_chartNormal_pair line 296