OAI/Analysis/BoundedHochschild/PathWords.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Formal path words, free-group retractions and simultaneous path moments.

  1. def OAI.HochschildPaths.signed line 27
  2. lemma OAI.HochschildPaths.signed_signed line 29
  3. lemma OAI.HochschildPaths.signed_one line 32
  4. lemma OAI.HochschildPaths.map_signed line 35
  5. lemma OAI.HochschildPaths.prod_ofFn_single line 38
  6. lemma OAI.HochschildPaths.distinguished_injective line 64
  7. def OAI.HochschildPaths.retractLetter line 71
  8. lemma OAI.HochschildPaths.retractLetter_distinguished line 78
  9. lemma OAI.HochschildPaths.retractLetter_away line 89
  10. def OAI.HochschildPaths.formalPath line 100
  11. def OAI.HochschildPaths.pathHom line 103
  12. def OAI.HochschildPaths.retractHom line 106
  13. lemma OAI.HochschildPaths.retract_formalPath line 110
  14. theorem OAI.HochschildPaths.retract_pathHom line 124
  15. theorem OAI.HochschildPaths.pathHom_injective line 134
  16. theorem OAI.HochschildPaths.pathHom_ne_one line 140
  17. def OAI.HochschildPaths.freshProjection line 147
  18. lemma OAI.HochschildPaths.retract_factors line 150
  19. theorem OAI.HochschildPaths.freshProjection_pathHom_ne_one line 166
  20. def OAI.HochschildPaths.unitaryEvaluation line 184
  21. def OAI.HochschildPaths.freshEvaluation line 187
  22. def OAI.HochschildPaths.encodeLetter line 190
  23. lemma OAI.HochschildPaths.value_encode line 194
  24. lemma OAI.HochschildPaths.degree_encode line 200
  25. lemma OAI.HochschildPaths.evaluate_encode line 206
  26. lemma OAI.HochschildPaths.degree_encode_list line 218
  27. theorem OAI.HochschildPaths.moment_eq_zero_of_fresh_ne_one line 230
  28. theorem OAI.HochschildPaths.distinguished_paths_moment line 244
  29. lemma OAI.HochschildPaths.lift_pathValue_formal line 269
  30. def OAI.HochschildPaths.mixedFamily line 286
  31. def OAI.HochschildPaths.freshUnits line 290
  32. lemma OAI.HochschildPaths.mixedFamily_of_inl line 293
  33. lemma OAI.HochschildPaths.mixedFamily_of_inr line 301
  34. lemma OAI.HochschildPaths.mixedFamily_eq_eval line 308
  35. theorem OAI.HochschildPaths.simultaneous_paths_of_free_lifts line 329