OAI/RingTheory/Multiplicity/RootCoactionT.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.RootCoaction.T line 35
  2. def OAI.Lech.RootCoaction.right line 37
  3. def OAI.Lech.RootCoaction.coord line 39
  4. def OAI.Lech.RootCoaction.unit line 40
  5. def OAI.Lech.RootCoaction.roots line 42
  6. lemma OAI.Lech.RootCoaction.coeff_poly line 44
  7. lemma OAI.Lech.RootCoaction.factorization line 53
  8. def OAI.Lech.RootCoaction.hom line 65
  9. lemma OAI.Lech.RootCoaction.hom_root line 69
  10. lemma OAI.Lech.RootCoaction.denominator_unit line 74
  11. def OAI.Lech.RootCoaction.weight line 79
  12. def OAI.Lech.RootCoaction.linear line 83
  13. lemma OAI.Lech.RootCoaction.linear_apply line 87
  14. def OAI.Lech.RootCoaction.counit line 91
  15. lemma OAI.Lech.RootCoaction.counit_right line 94
  16. lemma OAI.Lech.RootCoaction.counit_hom line 97
  17. abbrev OAI.Lech.RootCoaction.U line 120
  18. def OAI.Lech.RootCoaction.right₂ line 122
  19. def OAI.Lech.RootCoaction.delta line 124
  20. def OAI.Lech.RootCoaction.psi line 127
  21. lemma OAI.Lech.RootCoaction.delta_right line 130
  22. lemma OAI.Lech.RootCoaction.psi_right line 134
  23. lemma OAI.Lech.RootCoaction.psi_coord line 138
  24. lemma OAI.Lech.RootCoaction.psi_roots line 142
  25. lemma OAI.Lech.RootCoaction.delta_hom line 151
  26. lemma OAI.Lech.RootCoaction.unit_zpow_cancel line 182
  27. def OAI.Lech.RootCoaction.denominator line 196
  28. lemma OAI.Lech.RootCoaction.denominator_val line 200
  29. lemma OAI.Lech.RootCoaction.weight_eq line 204
  30. lemma OAI.Lech.RootCoaction.counit_denominator line 206
  31. lemma OAI.Lech.RootCoaction.counit_weight line 213
  32. lemma OAI.Lech.RootCoaction.counit_linear line 218
  33. lemma OAI.Lech.RootCoaction.psi_denominator line 228
  34. lemma OAI.Lech.RootCoaction.weight_coassoc line 249
  35. def OAI.Lech.RootCoaction.liftLinear line 272
  36. lemma OAI.Lech.RootCoaction.liftLinear_apply line 276
  37. lemma OAI.Lech.RootCoaction.linear_coassoc line 287
  38. def OAI.Lech.NativeDescent.inclusion line 312
  39. def OAI.Lech.NativeDescent.evaluation line 314
  40. def OAI.Lech.NativeDescent.invariants line 318
  41. lemma OAI.Lech.NativeDescent.invariant_eq line 320
  42. def OAI.Lech.NativeDescent.baseMap line 323
  43. def OAI.Lech.NativeDescent.baseInclusion line 325
  44. lemma OAI.Lech.NativeDescent.evaluation_baseInclusion line 328
  45. lemma OAI.Lech.NativeDescent.coaction_baseMap line 332
  46. def OAI.Lech.NativeDescent.coactionToEqualizer line 343
  47. def OAI.Lech.NativeDescent.inverse line 348
  48. lemma OAI.Lech.NativeDescent.baseInclusion_inverse line 352
  49. def OAI.Lech.NativeDescent.tensorEquiv line 361
  50. lemma OAI.Lech.ModuleDescent.finitePresentation line 383
  51. def OAI.Lech.RootInvariants.module line 414
  52. lemma OAI.Lech.RootInvariants.member_eq line 417
  53. lemma OAI.Lech.RootInvariants.evaluation_eq line 422
  54. lemma OAI.Lech.RootInvariants.delta_eq line 428
  55. def OAI.Lech.RootInvariants.tensorEquiv line 435
  56. lemma OAI.Lech.RootInvariants.finite line 441
  57. lemma OAI.Lech.RootInvariants.finitePresentation line 448
  58. lemma OAI.Lech.RootInvariants.flat line 457
  59. lemma OAI.Lech.RootInvariants.projective line 464
  60. lemma OAI.Lech.RootInvariants.rankAtStalk line 470