OAI/Algebra/Drinfeld/Transport.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DeligneDrinfeld.FiniteAlgebraNorm.normedRing line 14
  2. abbrev OAI.DeligneDrinfeld.FiniteAlgebraNorm.normedAlgebra line 19
  3. abbrev OAI.DeligneDrinfeld.FiniteAlgebraNorm.normedRingOver line 25
  4. abbrev OAI.DeligneDrinfeld.FiniteAlgebraNorm.normedAlgebraOver line 30
  5. def OAI.DeligneDrinfeld.FinitePicard.term line 42
  6. theorem OAI.DeligneDrinfeld.FinitePicard.term_zero line 46
  7. theorem OAI.DeligneDrinfeld.FinitePicard.term_succ line 47
  8. theorem OAI.DeligneDrinfeld.FinitePicard.term_base line 50
  9. theorem OAI.DeligneDrinfeld.FinitePicard.continuous_term line 55
  10. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_succ line 62
  11. def OAI.DeligneDrinfeld.FinitePicard.transport line 69
  12. theorem OAI.DeligneDrinfeld.FinitePicard.transport_base line 73
  13. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_transport line 79
  14. theorem OAI.DeligneDrinfeld.FinitePicard.continuousOn_term line 93
  15. theorem OAI.DeligneDrinfeld.FinitePicard.continuousOn_transport line 102
  16. theorem OAI.DeligneDrinfeld.FinitePicard.collar_limit line 108
  17. theorem OAI.DeligneDrinfeld.FinitePicard.integral_mem_submodule line 120
  18. structure OAI.DeligneDrinfeld.FinitePicard.NilpotentFiltration line 134
  19. theorem OAI.DeligneDrinfeld.FinitePicard.pow_mem line 145
  20. theorem OAI.DeligneDrinfeld.FinitePicard.pow_cutoff_eq_zero line 152
  21. theorem OAI.DeligneDrinfeld.FinitePicard.term_mem line 156
  22. theorem OAI.DeligneDrinfeld.FinitePicard.last_term_zero line 166
  23. theorem OAI.DeligneDrinfeld.FinitePicard.last_product_zero line 172
  24. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_succ_of_integrable line 178
  25. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_transport_of_integrable line 194
  26. theorem OAI.DeligneDrinfeld.FinitePicard.derivative_nilpotent_transport line 209
  27. abbrev OAI.DeligneDrinfeld.TruncatedWords.wt line 229
  28. def OAI.DeligneDrinfeld.TruncatedWords.relations line 231
  29. abbrev OAI.DeligneDrinfeld.TruncatedWords.Q line 234
  30. def OAI.DeligneDrinfeld.TruncatedWords.quotient line 236
  31. theorem OAI.DeligneDrinfeld.TruncatedWords.quotient_relation line 239
  32. theorem OAI.DeligneDrinfeld.TruncatedWords.quotient_above line 244
  33. def OAI.DeligneDrinfeld.TruncatedWords.filtration line 249
  34. theorem OAI.DeligneDrinfeld.TruncatedWords.filtration_antitone line 252
  35. theorem OAI.DeligneDrinfeld.TruncatedWords.filtration_one line 256
  36. theorem OAI.DeligneDrinfeld.TruncatedWords.filtration_mul line 260
  37. theorem OAI.DeligneDrinfeld.TruncatedWords.filtration_terminal line 266
  38. def OAI.DeligneDrinfeld.TruncatedWords.fromBelow line 271
  39. theorem OAI.DeligneDrinfeld.TruncatedWords.fromBelow_surjective line 274
  40. theorem OAI.DeligneDrinfeld.TruncatedWords.finite_words_below line 292
  41. instance OAI.DeligneDrinfeld.TruncatedWords.finite_below line 297
  42. instance OAI.DeligneDrinfeld.TruncatedWords.finite_quotient line 301
  43. instance OAI.DeligneDrinfeld.TruncatedWords.normedRing line 306
  44. instance OAI.DeligneDrinfeld.TruncatedWords.normedAlgebra line 307
  45. def OAI.DeligneDrinfeld.TruncatedWords.nilpotentFiltration line 309
  46. def OAI.DeligneDrinfeld.TensorFiltration.space line 325
  47. theorem OAI.DeligneDrinfeld.TensorFiltration.tmul_mem line 328
  48. theorem OAI.DeligneDrinfeld.TensorFiltration.antitone line 332
  49. theorem OAI.DeligneDrinfeld.TensorFiltration.one line 338
  50. theorem OAI.DeligneDrinfeld.TensorFiltration.mul line 342
  51. theorem OAI.DeligneDrinfeld.TensorFiltration.terminal line 362
  52. theorem OAI.DeligneDrinfeld.TensorFiltration.initial line 379
  53. def OAI.DeligneDrinfeld.TensorFiltration.cutoff line 394
  54. abbrev OAI.DeligneDrinfeld.TruncatedFree.wt line 407
  55. abbrev OAI.DeligneDrinfeld.TruncatedFree.B line 408
  56. def OAI.DeligneDrinfeld.TruncatedFree.trunc line 410
  57. theorem OAI.DeligneDrinfeld.TruncatedFree.trunc_val line 413
  58. theorem OAI.DeligneDrinfeld.TruncatedFree.trunc_above line 416
  59. theorem OAI.DeligneDrinfeld.TruncatedFree.sub_trunc_above line 420
  60. theorem OAI.DeligneDrinfeld.TruncatedFree.all_ge_zero line 427
  61. theorem OAI.DeligneDrinfeld.TruncatedFree.trunc_mul_trunc_right line 429
  62. theorem OAI.DeligneDrinfeld.TruncatedFree.trunc_mul_trunc_left line 437
  63. def OAI.DeligneDrinfeld.TruncatedFree.action line 445
  64. def OAI.DeligneDrinfeld.TruncatedFree.quotientAction line 471
  65. def OAI.DeligneDrinfeld.TruncatedFree.oneVector line 485
  66. def OAI.DeligneDrinfeld.TruncatedFree.normal line 487
  67. theorem OAI.DeligneDrinfeld.TruncatedFree.normal_quotient line 490
  68. theorem OAI.DeligneDrinfeld.TruncatedFree.normal_inverse line 497
  69. def OAI.DeligneDrinfeld.TruncatedFree.equiv line 503
  70. theorem OAI.DeligneDrinfeld.TruncatedFree.equiv_eq_normal line 513
  71. def OAI.DeligneDrinfeld.TruncatedFree.coefficient line 515
  72. theorem OAI.DeligneDrinfeld.TruncatedFree.coefficient_quotient line 519
  73. structure OAI.DeligneDrinfeld.FilteredComparison.Filtration line 530
  74. def OAI.DeligneDrinfeld.FilteredComparison.Preserves line 539
  75. def OAI.DeligneDrinfeld.FilteredComparison.GrInjective line 541
  76. def OAI.DeligneDrinfeld.FilteredComparison.GrSurjective line 543
  77. theorem OAI.DeligneDrinfeld.FilteredComparison.injective line 545
  78. theorem OAI.DeligneDrinfeld.FilteredComparison.lift_step line 557
  79. theorem OAI.DeligneDrinfeld.FilteredComparison.surjective line 567
  80. def OAI.DeligneDrinfeld.FilteredComparison.equivalence line 573
  81. theorem OAI.DeligneDrinfeld.FilteredComparison.inverse_preserves line 576
  82. theorem OAI.DeligneDrinfeld.FilteredComparison.comparison_raises line 590
  83. def OAI.DeligneDrinfeld.TruncatedSubstitution.gen line 608
  84. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.gen_mem line 610
  85. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.lift_word_mem line 613
  86. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.lift_mem line 621
  87. def OAI.DeligneDrinfeld.TruncatedSubstitution.subst line 625
  88. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.subst_quotient line 632
  89. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.subst_gen line 636
  90. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.subst_preserves line 639
  91. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.lift_word_difference line 646
  92. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.lift_difference line 663
  93. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.lift_gen line 669
  94. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.subst_raises line 674
  95. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.filtration_initial line 681
  96. def OAI.DeligneDrinfeld.TruncatedSubstitution.filtered line 687
  97. theorem OAI.DeligneDrinfeld.TruncatedSubstitution.subst_bijective line 693
  98. def OAI.DeligneDrinfeld.TruncatedSubstitution.equiv line 708
  99. theorem OAI.DeligneDrinfeld.NilpotentFreeLift.lift_word_mem line 718
  100. theorem OAI.DeligneDrinfeld.NilpotentFreeLift.lift_mem line 724
  101. def OAI.DeligneDrinfeld.NilpotentFreeLift.eval line 726
  102. theorem OAI.DeligneDrinfeld.NilpotentFreeLift.eval_quotient line 732
  103. theorem OAI.DeligneDrinfeld.NilpotentFreeLift.eval_gen line 734
  104. theorem OAI.DeligneDrinfeld.NilpotentFreeLift.eval_preserves line 736