OAI/Algebra/FiniteTensor/CompatibleCharts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Formal graph charts, compatible moving coordinates and actual gradient ideals.

  1. theorem OAI.PD4Tensor.FiniteCoordinates.exists_formal_left_chart line 21
  2. theorem OAI.PD4Tensor.FiniteCoordinates.substitution_specialization line 53
  3. def OAI.PD4Tensor.FiniteCoordinates.movingChart line 87
  4. def OAI.PD4Tensor.FiniteCoordinates.centralChart line 92
  5. theorem OAI.PD4Tensor.FiniteCoordinates.movingChart_specialization line 98
  6. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientRingCharP line 116
  7. theorem OAI.PD4Tensor.FiniteCoordinates.movingChart_normal_specialization line 124
  8. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_map line 140
  9. theorem OAI.PD4Tensor.FiniteCoordinates.combinedGraph_swap line 147
  10. def OAI.PD4Tensor.FiniteCoordinates.fixedChart line 164
  11. theorem OAI.PD4Tensor.FiniteCoordinates.fixedChart_coord line 171
  12. theorem OAI.PD4Tensor.FiniteCoordinates.compatible_moving_chart line 184
  13. theorem OAI.PD4Tensor.FiniteCoordinates.compatible_graph_charts line 236
  14. theorem OAI.PD4Tensor.FiniteCoordinates.constantMap_parameters line 314
  15. theorem OAI.PD4Tensor.parameter_hasSubst line 331
  16. theorem OAI.PD4Tensor.FiniteCoordinates.graph_zero line 350
  17. theorem OAI.PD4Tensor.FiniteCoordinates.graph_gradient line 362