OAI/RingTheory/Tachikawa/Counterexample.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Tachikawa.SourceField.sourceF line 10
  2. abbrev OAI.Tachikawa.SourceField.sourceX line 12
  3. abbrev OAI.Tachikawa.SourceField.sourceP line 13
  4. abbrev OAI.Tachikawa.SourceField.sourceU line 22
  5. abbrev OAI.Tachikawa.SourceField.sourceUZero line 24
  6. abbrev OAI.Tachikawa.SourceField.sourceTriangle line 26
  7. abbrev OAI.Tachikawa.SourceField.sourceCone line 27
  8. lemma OAI.Tachikawa.SourceField.sourceCone_totallyAcyclic line 28
  9. lemma OAI.Tachikawa.SourceField.sourceCone_finite line 30
  10. lemma OAI.Tachikawa.SourceField.sourceCone_projective line 32
  11. abbrev OAI.Tachikawa.SourceField.sourceAug line 36
  12. lemma OAI.Tachikawa.SourceField.sourceAug_exact line 37
  13. lemma OAI.Tachikawa.SourceField.sourceAug_zero line 42
  14. lemma OAI.Tachikawa.SourceField.sourceCone_closed_boundary line 46
  15. lemma OAI.Tachikawa.SourceField.sourceCone_homology_zero line 67
  16. def OAI.Tachikawa.DownHom.ofMap line 81
  17. lemma OAI.Tachikawa.DownHom.ofMap_closed line 83
  18. lemma OAI.Tachikawa.DownHom.ofMap_boundary line 89
  19. lemma OAI.Tachikawa.DownHom.ofMap_nullhomotopic line 99
  20. lemma OAI.Tachikawa.DownHom.coker_finite line 126
  21. lemma OAI.Tachikawa.DownHom.id_boundary_of_projective line 130
  22. lemma OAI.Tachikawa.DownHom.projective_of_id_boundary line 138
  23. lemma OAI.Tachikawa.Triangular.low_identity line 156
  24. lemma OAI.Tachikawa.Triangular.down_identity line 162
  25. lemma OAI.Tachikawa.Triangular.cone_id_boundary line 171
  26. lemma OAI.Tachikawa.completeHom_exact_of_zero line 188
  27. lemma OAI.Tachikawa.transfer_of_completeHom_vanishing line 215
  28. abbrev OAI.Tachikawa.SourceField.sourceConeModule line 248
  29. instance OAI.Tachikawa.SourceField.sourceConeModule_finite line 249
  30. instance OAI.Tachikawa.SourceField.sourceConeModule_finiteK line 251
  31. lemma OAI.Tachikawa.SourceField.sourceConeModule_nonprojective line 253
  32. abbrev OAI.Tachikawa.SourceField.sourceAlgebra line 263
  33. abbrev OAI.Tachikawa.SourceField.sourceModule line 264
  34. instance OAI.Tachikawa.SourceField.sourceModule_finite line 265
  35. lemma OAI.Tachikawa.SourceField.sourceModule_nonprojective line 267
  36. lemma OAI.Tachikawa.SourceField.sourceModule_ext line 273
  37. instance OAI.Tachikawa.SourceField.sourceAlgebra_finite line 283
  38. lemma OAI.Tachikawa.SourceField.sourceAlgebra_symmetric line 285
  39. theorem OAI.Tachikawa.main_theorem line 293

    Distinct definitions of this name: ComparatorChallenges/Tachikawa.lean:32 (same statement text; different proof or body). Qualify references as OAI.Tachikawa.main_theorem@path.