OAI/Algebra/FiniteTensor/DeformedCycles.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Liftable pure tensors, deformation cycles and the finite pairing obstruction.

  1. theorem OAI.PD4Tensor.exists_liftable_pure_tensor line 20
  2. def OAI.PD4Tensor.deformedTensor line 149
  3. def OAI.PD4Tensor.tensorLift line 156
  4. theorem OAI.PD4Tensor.sum_finsets_split line 160
  5. def OAI.PD4Tensor.deformedCoordinate line 183
  6. theorem OAI.PD4Tensor.deformedTensor_eq_sum line 189
  7. theorem OAI.PD4Tensor.tensorLift_cycle line 203
  8. def OAI.PD4Tensor.specializeTensor line 246
  9. theorem OAI.PD4Tensor.specializeTensor_tmul line 249
  10. theorem OAI.PD4Tensor.specialize_tensorLift line 254
  11. theorem OAI.PD4Tensor.selective_tensorLift_cycle line 284
  12. theorem OAI.PD4Tensor.exists_three_deformed_cycle line 319
  13. theorem OAI.PD4Tensor.finite_tensor_pairing_obstruction line 383