OAI/Geometry/Coboundary/Frames.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Unimodular frames, bad-simplex transport, height reduction, and partial-basis exactness.

  1. def OAI.CoboundaryExpanders.Unimodular.IsFrame line 16
  2. lemma OAI.CoboundaryExpanders.Unimodular.frame_empty line 20
  3. lemma OAI.CoboundaryExpanders.Unimodular.frame_reindex line 25
  4. lemma OAI.CoboundaryExpanders.Unimodular.frame_equiv line 34
  5. def OAI.CoboundaryExpanders.Unimodular.combine line 43
  6. lemma OAI.CoboundaryExpanders.Unimodular.combine_apply line 46
  7. lemma OAI.CoboundaryExpanders.Unimodular.combine_single line 49
  8. lemma OAI.CoboundaryExpanders.Unimodular.retract_combine line 54
  9. def OAI.CoboundaryExpanders.Unimodular.quotientProjection line 60
  10. lemma OAI.CoboundaryExpanders.Unimodular.quotientProjection_val line 67
  11. lemma OAI.CoboundaryExpanders.Unimodular.quotientProjection_family line 71
  12. lemma OAI.CoboundaryExpanders.Unimodular.quotientProjection_ker line 77
  13. def OAI.CoboundaryExpanders.Unimodular.splitEquiv line 83
  14. theorem OAI.CoboundaryExpanders.Unimodular.frame_sum_iff line 98
  15. lemma OAI.CoboundaryExpanders.Unimodular.frame_rank_split line 131
  16. def OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.stage line 151
  17. def OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.goodLink line 159
  18. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.block_faces line 168
  19. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.block_stage line 178
  20. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.old_stage line 185
  21. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.block_relative line 193
  22. abbrev OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.BadFaces line 213
  23. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.stage_succ line 217
  24. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.blocks_inter line 239
  25. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.relative_self line 254
  26. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.relative_stage_succ line 258
  27. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.exactIn_of_relative line 277
  28. lemma OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.relative_trans line 294
  29. theorem OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.relative line 313
  30. theorem OAI.CoboundaryExpanders.InfiniteChains.BadSimplex.exactIn line 340
  31. def OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel line 377
  32. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_single line 381
  33. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_supported line 386
  34. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_graded line 395
  35. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_injective line 405
  36. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_boundary line 409
  37. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_comp line 422
  38. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_id line 430
  39. theorem OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.exactIn_equiv line 437
  40. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_equiv_cancel line 462
  41. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relabel_boundary_apply line 471
  42. theorem OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.relativeIn_equiv line 475
  43. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.rawCone_supported line 500
  44. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.rawCone_graded line 510
  45. lemma OAI.CoboundaryExpanders.InfiniteChains.ChainTransport.exactIn_of_extend line 518
  46. def OAI.CoboundaryExpanders.Unimodular.complex line 541
  47. lemma OAI.CoboundaryExpanders.Unimodular.frame_image line 552
  48. def OAI.CoboundaryExpanders.Unimodular.disjSumEquiv line 557
  49. lemma OAI.CoboundaryExpanders.Unimodular.frame_disjSum line 579
  50. lemma OAI.CoboundaryExpanders.Unimodular.frame_inl line 591
  51. lemma OAI.CoboundaryExpanders.Unimodular.frame_adjoin line 598
  52. def OAI.CoboundaryExpanders.Unimodular.insertEquiv line 611
  53. lemma OAI.CoboundaryExpanders.Unimodular.insert_mem line 632
  54. lemma OAI.CoboundaryExpanders.Unimodular.fill_zero_coordinate line 644
  55. def OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.bounded line 664
  56. abbrev OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.Bad line 671
  57. abbrev OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.Good line 672
  58. def OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.split line 674
  59. def OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.splitComplex line 677
  60. lemma OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.stage0_iff line 684
  61. lemma OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.relative_lower line 709
  62. theorem OAI.CoboundaryExpanders.InfiniteChains.HeightReduction.exactIn line 726
  63. structure OAI.CoboundaryExpanders.Unimodular.EuclideanHeight line 778
  64. abbrev OAI.CoboundaryExpanders.Unimodular.standardCoordinate line 785
  65. lemma OAI.CoboundaryExpanders.Unimodular.split_frame line 788
  66. lemma OAI.CoboundaryExpanders.Unimodular.goodLink_eq line 795
  67. lemma OAI.CoboundaryExpanders.Unimodular.reduced_projection_surjective line 816
  68. theorem OAI.CoboundaryExpanders.Unimodular.exactIn_complex line 848
  69. def OAI.CoboundaryExpanders.Unimodular.fieldHeight line 890
  70. def OAI.CoboundaryExpanders.Unimodular.polynomialHeight line 897
  71. theorem OAI.CoboundaryExpanders.Unimodular.polynomial_exact line 909
  72. theorem OAI.CoboundaryExpanders.Unimodular.field_exact line 915