OAI/RingTheory/Tachikawa/Cone.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.CompleteCone.complex line 12
  2. lemma OAI.Tachikawa.CompleteCone.rel line 13
  3. abbrev OAI.Tachikawa.CompleteCone.left line 15
  4. abbrev OAI.Tachikawa.CompleteCone.right line 17
  5. abbrev OAI.Tachikawa.CompleteCone.inLeft line 19
  6. abbrev OAI.Tachikawa.CompleteCone.inRight line 21
  7. lemma OAI.Tachikawa.CompleteCone.inLeft_left line 24
  8. lemma OAI.Tachikawa.CompleteCone.inLeft_right line 26
  9. lemma OAI.Tachikawa.CompleteCone.inRight_left line 28
  10. lemma OAI.Tachikawa.CompleteCone.inRight_right line 30
  11. lemma OAI.Tachikawa.CompleteCone.total line 32
  12. lemma OAI.Tachikawa.CompleteCone.ext_element line 37
  13. lemma OAI.Tachikawa.CompleteCone.left_d line 46
  14. lemma OAI.Tachikawa.CompleteCone.right_d line 50
  15. lemma OAI.Tachikawa.CompleteCone.inRight_d line 55
  16. lemma OAI.Tachikawa.CompleteCone.inLeft_d line 57
  17. lemma OAI.Tachikawa.CompleteCone.exact line 61
  18. lemma OAI.Tachikawa.CompleteCone.boundaries line 114
  19. lemma OAI.Tachikawa.CompleteCone.totallyAcyclic line 120
  20. def OAI.Tachikawa.CompleteCone.termEquiv line 168
  21. lemma OAI.Tachikawa.CompleteCone.finite line 172
  22. lemma OAI.Tachikawa.CompleteCone.projective line 177
  23. abbrev OAI.Tachikawa.DownCone.C line 195
  24. abbrev OAI.Tachikawa.DownCone.iL line 196
  25. abbrev OAI.Tachikawa.DownCone.pL line 197
  26. def OAI.Tachikawa.DownCone.low line 199
  27. def OAI.Tachikawa.DownCone.high line 201
  28. def OAI.Tachikawa.DownCone.cross line 203
  29. def OAI.Tachikawa.DownCone.assemble line 206
  30. lemma OAI.Tachikawa.DownCone.inl_fst_apply line 212
  31. lemma OAI.Tachikawa.DownCone.apply_inl_fst line 220
  32. lemma OAI.Tachikawa.DownCone.block_transport line 228
  33. lemma OAI.Tachikawa.DownCone.cross_transport line 238
  34. lemma OAI.Tachikawa.DownCone.low_assemble line 246
  35. lemma OAI.Tachikawa.DownCone.high_assemble line 253
  36. lemma OAI.Tachikawa.DownCone.cross_assemble line 259
  37. lemma OAI.Tachikawa.DownCone.assemble_blocks line 269
  38. lemma OAI.Tachikawa.DownCone.d_left line 309
  39. lemma OAI.Tachikawa.DownCone.d_right line 316
  40. lemma OAI.Tachikawa.DownCone.inRight_dcat line 319
  41. lemma OAI.Tachikawa.DownCone.apply_inl_d line 322
  42. lemma OAI.Tachikawa.DownCone.diff_assemble line 335
  43. lemma OAI.Tachikawa.DownCone.low_diff line 352
  44. lemma OAI.Tachikawa.DownCone.high_diff line 355
  45. lemma OAI.Tachikawa.DownCone.cross_diff line 358
  46. lemma OAI.Tachikawa.DownCone.low_zero line 373
  47. lemma OAI.Tachikawa.DownCone.high_zero line 375
  48. lemma OAI.Tachikawa.DownCone.cross_zero line 377
  49. lemma OAI.Tachikawa.DownCone.low_add line 379
  50. lemma OAI.Tachikawa.DownCone.high_add line 381
  51. lemma OAI.Tachikawa.DownCone.cross_add line 383
  52. lemma OAI.Tachikawa.DownCone.blocks_ext line 388
  53. lemma OAI.Tachikawa.DownCone.closed_blocks_aux line 393
  54. lemma OAI.Tachikawa.DownCone.closed_blocks line 407
  55. theorem OAI.Tachikawa.DownCone.boundary_of_delta line 416
  56. abbrev OAI.Tachikawa.Triangular.cone line 477
  57. lemma OAI.Tachikawa.Triangular.cone_closed_boundary line 480
  58. abbrev OAI.Tachikawa.Triangular.oneFree line 514
  59. instance OAI.Tachikawa.Triangular.(instance at line 515) line 515
  60. instance OAI.Tachikawa.Triangular.(instance at line 516) line 516
  61. def OAI.Tachikawa.Triangular.regIn₀ line 517
  62. def OAI.Tachikawa.Triangular.regIn₁ line 519
  63. def OAI.Tachikawa.Triangular.regOut₀ line 521
  64. def OAI.Tachikawa.Triangular.regOut₁ line 523
  65. lemma OAI.Tachikawa.Triangular.reg_split line 525
  66. lemma OAI.Tachikawa.Triangular.D₀_totallyAcyclic line 541
  67. lemma OAI.Tachikawa.Triangular.D₁_totallyAcyclic line 564
  68. lemma OAI.Tachikawa.DownHom.homology_subsingleton line 608
  69. lemma OAI.Tachikawa.Triangular.cone_totallyAcyclic line 639
  70. lemma OAI.Tachikawa.Triangular.cone_finite line 645
  71. lemma OAI.Tachikawa.Triangular.cone_projective line 660
  72. lemma OAI.Tachikawa.DownHom.actionDelta_injective line 688
  73. lemma OAI.Tachikawa.DownHom.actionDelta_surjective line 708