OAI/AlgebraicTopology/Cubical/Chains.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CubicalChains.Chains line 15
  2. def OAI.CubicalChains.front line 17
  3. def OAI.CubicalChains.shift line 20
  4. theorem OAI.CubicalChains.front_single line 24
  5. theorem OAI.CubicalChains.shift_single line 28
  6. def OAI.CubicalChains.boundaryTerm line 32
  7. def OAI.CubicalChains.boundary line 37
  8. theorem OAI.CubicalChains.boundary_single line 40
  9. theorem OAI.CubicalChains.boundaryTerm_nil line 44
  10. theorem OAI.CubicalChains.boundaryTerm_cons line 45
  11. theorem OAI.CubicalChains.boundary_front line 49
  12. theorem OAI.CubicalChains.shift_front line 59
  13. theorem OAI.CubicalChains.boundaryTerm_shift line 66
  14. theorem OAI.CubicalChains.boundary_boundaryTerm line 76
  15. def OAI.CubicalChains.upperTerm line 89

    Source documentation

    The part of the boundary incident to the top vertex.

    def upperTerm (g : G) : List A → Chains G A
  | [] => 0
  | x :: w => -Finsupp.single (g,w) 1 - front x (upperTerm g w)

    Mentions: OAI.CubicalChains.Chains, OAI.CubicalChains.front

  16. def OAI.CubicalChains.upper line 93
  17. theorem OAI.CubicalChains.upper_single line 97
  18. theorem OAI.CubicalChains.upperTerm_nil line 101
  19. theorem OAI.CubicalChains.upperTerm_cons line 104
  20. theorem OAI.CubicalChains.upper_front line 108
  21. def OAI.CubicalChains.coneTerm line 117
  22. def OAI.CubicalChains.cone line 120
  23. theorem OAI.CubicalChains.cone_single line 124
  24. theorem OAI.CubicalChains.supported_map line 128
  25. theorem OAI.CubicalChains.upperTerm_supported line 141
  26. theorem OAI.CubicalChains.cone_absent_upper line 157
  27. theorem OAI.CubicalChains.cone_front_present line 170
  28. theorem OAI.CubicalChains.upper_cone_identity line 183
  29. def OAI.CubicalChains.Removed line 196

    Source documentation

    A lower face is obtained by deleting one direction and crossing it.

    def Removed (x : A) (w u : List A) : Prop :=
…
  30. theorem OAI.CubicalChains.Removed.mem line 200
  31. theorem OAI.CubicalChains.Removed.sublist line 205
  32. theorem OAI.CubicalChains.Removed.length line 210
  33. theorem OAI.CubicalChains.Removed.not_mem line 215
  34. theorem OAI.CubicalChains.Removed.cons line 223
  35. def OAI.CubicalChains.lowerTerm line 227
  36. def OAI.CubicalChains.lower line 229
  37. theorem OAI.CubicalChains.lower_single line 231
  38. theorem OAI.CubicalChains.lowerTerm_nil line 235
  39. theorem OAI.CubicalChains.lowerTerm_cons line 237
  40. theorem OAI.CubicalChains.lowerTerm_supported line 242
  41. structure OAI.CubicalChains.DescentSystem line 260

    Source documentation

    Local combinatorial descending-cube data. All these fields will be supplied by the actual trace normal form, not by a geometric exactness assumption.

    structure DescentSystem (v : A → G) where
…
  42. def OAI.CubicalChains.DescentSystem.Valid line 273
  43. def OAI.CubicalChains.DescentSystem.admissible line 275
  44. theorem OAI.CubicalChains.DescentSystem.valid_sublist line 278
  45. theorem OAI.CubicalChains.DescentSystem.valid_nodup line 281
  46. theorem OAI.CubicalChains.DescentSystem.valid_removed line 284
  47. theorem OAI.CubicalChains.DescentSystem.valid_zero_length line 291
  48. theorem OAI.CubicalChains.DescentSystem.choose_head line 296
  49. theorem OAI.CubicalChains.DescentSystem.valid_cone line 313
  50. theorem OAI.CubicalChains.DescentSystem.upperTerm_admissible line 323
  51. theorem OAI.CubicalChains.DescentSystem.lowerTerm_admissible line 329
  52. def OAI.CubicalChains.DescentSystem.homotopyTerm line 336
  53. def OAI.CubicalChains.DescentSystem.homotopy line 339
  54. theorem OAI.CubicalChains.DescentSystem.homotopy_single line 342
  55. theorem OAI.CubicalChains.DescentSystem.homotopyTerm_admissible line 345
  56. theorem OAI.CubicalChains.DescentSystem.admissible_mono line 358
  57. theorem OAI.CubicalChains.DescentSystem.upper_admissible line 363
  58. theorem OAI.CubicalChains.DescentSystem.lower_admissible line 371
  59. theorem OAI.CubicalChains.DescentSystem.boundary_admissible line 379
  60. theorem OAI.CubicalChains.DescentSystem.homotopy_admissible line 386
  61. theorem OAI.CubicalChains.DescentSystem.boundary_squared line 394
  62. theorem OAI.CubicalChains.DescentSystem.homotopy_upperTerm line 406
  63. theorem OAI.CubicalChains.DescentSystem.upper_homotopy_identity line 418
  64. def OAI.CubicalChains.DescentSystem.remainder line 424
  65. theorem OAI.CubicalChains.DescentSystem.remainder_single line 427
  66. theorem OAI.CubicalChains.DescentSystem.remainder_admissible line 437
  67. theorem OAI.CubicalChains.DescentSystem.admissible_zero line 458
  68. theorem OAI.CubicalChains.DescentSystem.cycle_bounds line 472

    Source documentation

    Finite-support descending-cube contraction: every positive-dimensional cycle bounds, with no topological exactness or contractibility assumption.

    theorem cycle_bounds {k N : ℕ} (hk : 0 < k) (c : Chains G A)
    (hc : c ∈ D.admissible k N) (hz : boundary v c = 0) :
    ∃ b ∈ D.admissible (k+1) N, boundary v b = c := by
…

    Mentions: OAI.CubicalChains.Chains, OAI.CubicalChains.boundary