OAI/CategoryTheory/ThickClosure/LaurentAction.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HahnWilson.LaurentDg.familyTotal line 15
  2. abbrev OAI.HahnWilson.LaurentDg.familyInc line 16
  3. def OAI.HahnWilson.LaurentDg.familyDifferential line 19
  4. structure OAI.HahnWilson.LaurentDg.ActionModule line 24
  5. structure OAI.HahnWilson.LaurentDg.PowerData line 35
  6. def OAI.HahnWilson.LaurentDg.ActionModule.presentation line 45
  7. def OAI.HahnWilson.LaurentDg.totalMap line 48
  8. lemma OAI.HahnWilson.LaurentDg.familyInc_injective line 52
  9. lemma OAI.HahnWilson.LaurentDg.familyDifferential_inc_succ line 55
  10. def OAI.HahnWilson.LaurentDg.ActionModule.asModule line 69
  11. lemma OAI.HahnWilson.LaurentDg.ActionModule.monomial_add line 72
  12. lemma OAI.HahnWilson.LaurentDg.ActionModule.monomial_zero line 79
  13. lemma OAI.HahnWilson.LaurentDg.ActionModule.monomial_smul line 83
  14. lemma OAI.HahnWilson.LaurentDg.ActionModule.exists_powerValue line 92
  15. def OAI.HahnWilson.LaurentDg.ActionModule.powerValue line 98
  16. lemma OAI.HahnWilson.LaurentDg.ActionModule.powerValue_spec line 102
  17. def OAI.HahnWilson.LaurentDg.ActionModule.powerLinear line 108
  18. lemma OAI.HahnWilson.LaurentDg.ActionModule.powerLinear_spec line 118
  19. def OAI.HahnWilson.LaurentDg.ActionModule.exponent line 123
  20. lemma OAI.HahnWilson.LaurentDg.ActionModule.exponent_spec line 126
  21. lemma OAI.HahnWilson.LaurentDg.ActionModule.exponent_eq line 130
  22. def OAI.HahnWilson.LaurentDg.ActionModule.directMap line 134
  23. lemma OAI.HahnWilson.LaurentDg.ActionModule.directMap_spec line 138
  24. lemma OAI.HahnWilson.LaurentDg.ActionModule.directMap_refl line 145
  25. lemma OAI.HahnWilson.LaurentDg.ActionModule.directMap_trans line 152
  26. def OAI.HahnWilson.LaurentDg.ActionModule.directIso line 166
  27. lemma OAI.HahnWilson.LaurentDg.ActionModule.directMap_d line 173
  28. def OAI.HahnWilson.LaurentDg.ActionModule.reconstructed line 187
  29. lemma OAI.HahnWilson.LaurentDg.representation_single_total line 196
  30. lemma OAI.HahnWilson.LaurentDg.totalMap_inc line 202
  31. theorem OAI.HahnWilson.LaurentDg.action_reconstructs line 207
  32. theorem OAI.HahnWilson.LaurentDg.morphism_action_iff line 225
  33. lemma OAI.HahnWilson.LaurentDg.totalMap_id line 262
  34. lemma OAI.HahnWilson.LaurentDg.totalMap_comp line 269
  35. structure OAI.HahnWilson.LaurentDg.ActionModule.Hom line 279
  36. instance OAI.HahnWilson.LaurentDg.ActionModule.(instance at line 285) line 285
  37. lemma OAI.HahnWilson.LaurentDg.ActionModule.id_f line 295
  38. lemma OAI.HahnWilson.LaurentDg.ActionModule.comp_f line 296
  39. lemma OAI.HahnWilson.LaurentDg.familyDifferential_eq line 299
  40. def OAI.HahnWilson.LaurentDg.asAction line 307
  41. def OAI.HahnWilson.LaurentDg.actionFunctor line 320
  42. instance OAI.HahnWilson.LaurentDg.actionFunctor_faithful line 326
  43. instance OAI.HahnWilson.LaurentDg.actionFunctor_full line 332
  44. def OAI.HahnWilson.LaurentDg.presentationActionIso line 339
  45. lemma OAI.HahnWilson.LaurentDg.actionFunctor_essSurj line 363
  46. theorem OAI.HahnWilson.LaurentDg.actual_action_equivalence line 368