OAI/Algebra/FiniteTensor/FiniteCharts.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Finite coordinate charts, coefficient extensions and nilpotent deformation equivalences.

  1. def OAI.PD4Tensor.FiniteCoordinates.leftInclusion line 15
  2. def OAI.PD4Tensor.FiniteCoordinates.leftRestriction line 19
  3. theorem OAI.PD4Tensor.FiniteCoordinates.leftInclusion_coord line 27
  4. theorem OAI.PD4Tensor.FiniteCoordinates.leftRestriction_coord line 33
  5. def OAI.PD4Tensor.FiniteCoordinates.rightIdeal line 38
  6. theorem OAI.PD4Tensor.FiniteCoordinates.leftRestriction_leftInclusion line 41
  7. theorem OAI.PD4Tensor.FiniteCoordinates.leftRestriction_surjective line 50
  8. theorem OAI.PD4Tensor.FiniteCoordinates.leftRestriction_ker line 56
  9. theorem OAI.PD4Tensor.FiniteCoordinates.graphRestriction_ker line 79
  10. def OAI.PD4Tensor.FiniteCoordinates.rightInclusion line 112
  11. theorem OAI.PD4Tensor.FiniteCoordinates.rightInclusion_coord line 116
  12. def OAI.PD4Tensor.FiniteCoordinates.toTensor line 121
  13. def OAI.PD4Tensor.FiniteCoordinates.fromTensor line 132
  14. theorem OAI.PD4Tensor.FiniteCoordinates.toTensor_inl line 136
  15. theorem OAI.PD4Tensor.FiniteCoordinates.toTensor_inr line 139
  16. theorem OAI.PD4Tensor.FiniteCoordinates.fromTensor_tmul line 142
  17. theorem OAI.PD4Tensor.FiniteCoordinates.from_toTensor line 146
  18. theorem OAI.PD4Tensor.FiniteCoordinates.to_fromTensor line 151
  19. def OAI.PD4Tensor.FiniteCoordinates.sumTensorEquiv line 166
  20. def OAI.PD4Tensor.FiniteCoordinates.coefficientMap line 180
  21. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientMap_coord line 183
  22. def OAI.PD4Tensor.FiniteCoordinates.baseToTensor line 186
  23. def OAI.PD4Tensor.FiniteCoordinates.baseFromTensor line 191
  24. theorem OAI.PD4Tensor.FiniteCoordinates.baseToTensor_coord line 195
  25. theorem OAI.PD4Tensor.FiniteCoordinates.baseFromTensor_tmul line 198
  26. theorem OAI.PD4Tensor.FiniteCoordinates.baseFrom_toTensor line 203
  27. theorem OAI.PD4Tensor.FiniteCoordinates.baseTo_fromTensor line 209
  28. def OAI.PD4Tensor.FiniteCoordinates.baseChangeEquiv line 229
  29. def OAI.PD4Tensor.FiniteCoordinates.extendEquiv line 237
  30. theorem OAI.PD4Tensor.FiniteCoordinates.extendEquiv_coord line 241
  31. def OAI.PD4Tensor.FiniteCoordinates.rightRestriction line 255
  32. theorem OAI.PD4Tensor.FiniteCoordinates.rightRestriction_coord line 263
  33. def OAI.PD4Tensor.FiniteCoordinates.leftIdeal line 267
  34. theorem OAI.PD4Tensor.FiniteCoordinates.rightRestriction_ker line 270
  35. def OAI.PD4Tensor.FiniteCoordinates.mixedEquiv line 293
  36. theorem OAI.PD4Tensor.FiniteCoordinates.mixedEquiv_inl line 297
  37. theorem OAI.PD4Tensor.FiniteCoordinates.mixedEquiv_inr line 305
  38. def OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization line 311
  39. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization_coord line 314
  40. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization_coefficientMap line 322
  41. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization_parameter line 334
  42. def OAI.PD4Tensor.FiniteCoordinates.coefficientIdeal line 343
  43. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientSpecialization_ker line 349
  44. theorem OAI.PD4Tensor.FiniteCoordinates.coefficientIdeal_nilpotent line 377
  45. theorem OAI.PD4Tensor.bijective_of_nilpotent_deformation line 393
  46. theorem OAI.PD4Tensor.FiniteCoordinates.difference_mem line 422
  47. theorem OAI.PD4Tensor.FiniteCoordinates.bijective_of_central_equiv line 452