OAI/RingTheory/Multiplicity/ProductSourceCoverFaceSlice.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.ProductSourceCover.faceSlice_kernel line 22
  2. abbrev OAI.Lech.ProductSourceCover.divisorCochains line 46
  3. def OAI.Lech.ProductSourceCover.divisorInclusion line 48
  4. def OAI.Lech.ProductSourceCover.divisorRestriction line 53
  5. def OAI.Lech.ProductSourceCover.divisorSection line 56
  6. lemma OAI.Lech.ProductSourceCover.divisorRestriction_section line 59
  7. lemma OAI.Lech.ProductSourceCover.divisorInclusion_injective line 63
  8. lemma OAI.Lech.ProductSourceCover.divisorRestriction_surjective line 68
  9. lemma OAI.Lech.ProductSourceCover.divisorRestriction_comp line 72
  10. lemma OAI.Lech.ProductSourceCover.divisorCochains_exact line 78
  11. def OAI.Lech.AlternatingCech.delete line 95
  12. lemma OAI.Lech.AlternatingCech.delete_sorted line 99
  13. lemma OAI.Lech.AlternatingCech.delete_subset line 104
  14. lemma OAI.Lech.AlternatingCech.sortedCoordinates_delta line 112
  15. abbrev OAI.Lech.AlternatingCech.sorted line 127
  16. def OAI.Lech.AlternatingCech.sortedDelta line 129
  17. lemma OAI.Lech.AlternatingCech.cochainsSorted_delta line 139
  18. lemma OAI.Lech.AlternatingCech.sortedDelta_square line 147
  19. theorem OAI.Lech.AlternatingCech.sortedExact line 154
  20. abbrev OAI.Lech.DoubleCech.term line 178
  21. def OAI.Lech.DoubleCech.vertical line 180
  22. def OAI.Lech.DoubleCech.horizontal line 184
  23. lemma OAI.Lech.DoubleCech.vertical_square line 190
  24. lemma OAI.Lech.DoubleCech.horizontal_square line 195
  25. lemma OAI.Lech.DoubleCech.horizontal_vertical line 201
  26. def OAI.Lech.DoubleCech.row line 214
  27. lemma OAI.Lech.DoubleCech.row_d line 221
  28. def OAI.Lech.DoubleCech.rowMap line 226
  29. lemma OAI.Lech.DoubleCech.rowMap_square line 233
  30. def OAI.Lech.DoubleCech.complex line 241
  31. lemma OAI.Lech.DoubleCech.term_zero_horizontal line 244
  32. lemma OAI.Lech.ComplexExtension.negative_zero line 259
  33. def OAI.Lech.ComplexExtension.mapExtendXIso line 266
  34. lemma OAI.Lech.ComplexExtension.map_conjugation_square line 276
  35. lemma OAI.Lech.ComplexExtension.mapExtendXIso_comm line 285
  36. def OAI.Lech.ComplexExtension.mapExtendIso line 312
  37. abbrev OAI.Lech.BicomplexTotal.singleZero line 326
  38. abbrev OAI.Lech.BicomplexTotal.totalSingleZero line 327
  39. def OAI.Lech.BicomplexTotal.intoSingle line 328
  40. def OAI.Lech.BicomplexTotal.outOfSingle line 330
  41. lemma OAI.Lech.BicomplexTotal.into_out_single line 335
  42. lemma OAI.Lech.BicomplexTotal.out_into_single line 340
  43. def OAI.Lech.BicomplexTotal.singleXIso line 355
  44. lemma OAI.Lech.BicomplexTotal.single_d₁ line 360
  45. lemma OAI.Lech.BicomplexTotal.into_single_comm line 365
  46. def OAI.Lech.BicomplexTotal.singleZeroIso line 375
  47. def OAI.Lech.BicomplexTotal.singleIso line 385
  48. def OAI.Lech.BicomplexTotal.singleHomologyIso line 392
  49. theorem OAI.Lech.BicomplexTotal.acyclic_of_rows line 399
  50. def OAI.Lech.FiniteComplex.bottomProjection line 415
  51. instance OAI.Lech.FiniteComplex.bottomProjection_epi line 421
  52. def OAI.Lech.FiniteComplex.dropBottom line 431
  53. def OAI.Lech.FiniteComplex.bottomShortComplex line 433
  54. lemma OAI.Lech.FiniteComplex.bottomShortExact line 436
  55. lemma OAI.Lech.FiniteComplex.bottomShortExact_eval line 441
  56. lemma OAI.Lech.FiniteComplex.bottomProjection_f_isIso line 445
  57. lemma OAI.Lech.FiniteComplex.dropBottom_X_bottom line 450
  58. lemma OAI.Lech.FiniteComplex.dropBottom_ι_isIso line 454
  59. def OAI.Lech.FiniteComplex.dropBottomXIso line 459
  60. def OAI.Lech.FiniteComplex.bottomSplitting line 464
  61. lemma OAI.Lech.FiniteComplex.dropBottom_boundedBelow line 477
  62. lemma OAI.Lech.FiniteComplex.bottomProjection_naturality line 487
  63. def OAI.Lech.FiniteComplex.dropBottomMap line 497
  64. lemma OAI.Lech.FiniteComplex.dropBottomMap_ι line 501
  65. def OAI.Lech.FiniteComplex.bottomShortComplexMap line 506