OAI/Topology/EilenbergGanea/LevelBasis.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EilenbergGanea.LevelBasis.ht line 16
  2. theorem OAI.EilenbergGanea.LevelBasis.ht_mul line 17
  3. theorem OAI.EilenbergGanea.LevelBasis.ht_one line 18
  4. theorem OAI.EilenbergGanea.LevelBasis.ht_inv line 19
  5. theorem OAI.EilenbergGanea.LevelBasis.ht_zpow line 20
  6. theorem OAI.EilenbergGanea.LevelBasis.ht_ker line 21
  7. theorem OAI.EilenbergGanea.LevelBasis.ht_generator line 25
  8. theorem OAI.EilenbergGanea.LevelBasis.ht_step line 28
  9. def OAI.EilenbergGanea.LevelBasis.Shape line 30
  10. def OAI.EilenbergGanea.LevelBasis.basisIndex line 32
  11. theorem OAI.EilenbergGanea.LevelBasis.basisIndex_height line 36
  12. theorem OAI.EilenbergGanea.LevelBasis.basisIndex_injective line 41
  13. theorem OAI.EilenbergGanea.LevelBasis.basisIndex_mem line 52
  14. theorem OAI.EilenbergGanea.LevelBasis.exists_basisIndex line 61
  15. def OAI.EilenbergGanea.LevelBasis.includeBasis line 75
  16. theorem OAI.EilenbergGanea.LevelBasis.includeBasis_single line 77
  17. theorem OAI.EilenbergGanea.LevelBasis.includeBasis_injective line 81
  18. theorem OAI.EilenbergGanea.LevelBasis.includeBasis_range line 85
  19. def OAI.EilenbergGanea.LevelBasis.projectBasis line 98
  20. theorem OAI.EilenbergGanea.LevelBasis.project_include line 101
  21. theorem OAI.EilenbergGanea.LevelBasis.include_project line 106
  22. theorem OAI.EilenbergGanea.LevelBasis.includeBasis_mem line 113
  23. theorem OAI.EilenbergGanea.LevelBasis.shape_two_form line 119

    Source documentation

    The level edge parameter has precisely two directions and initial height -1.

    theorem shape_two_form (s : Shape L 2) : ∃ a b, s.val = ([a,b],-1) := by
…

    Mentions: OAI.EilenbergGanea.LevelBasis.Shape

  24. def OAI.EilenbergGanea.LevelBasis.generator line 127
  25. def OAI.EilenbergGanea.LevelBasis.includeVertices line 130
  26. theorem OAI.EilenbergGanea.LevelBasis.includeVertices_single line 133
  27. theorem OAI.EilenbergGanea.LevelBasis.includeVertices_injective line 136
  28. theorem OAI.EilenbergGanea.LevelBasis.boundary_square line 143
  29. theorem OAI.EilenbergGanea.LevelBasis.levelBoundary_include_single line 157
  30. theorem OAI.EilenbergGanea.LevelBasis.levelBoundary_include line 175
  31. def OAI.EilenbergGanea.LevelBasis.triangleBoundary line 186

    Source documentation

    The literal based integral boundary of the crossing three-cubes.

    def triangleBoundary : (φ.ker × Shape L 3 →₀ ℤ) →ₗ[ℤ] (φ.ker × Shape L 2 →₀ ℤ) :=
…

    Mentions: OAI.EilenbergGanea.LevelBasis.Shape

  32. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_inclusion line 190
  33. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_cycle line 198
  34. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_range line 209
  35. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_injective line 225
  36. def OAI.EilenbergGanea.LevelBasis.leftTranslate line 238

    Source documentation

    Left translation on the actual ambient cube chains.

    def leftTranslate (g : G) : CubicalChains.Chains G A →ₗ[ℤ] CubicalChains.Chains G A :=
…

    Mentions: OAI.CubicalChains.Chains

  37. theorem OAI.EilenbergGanea.LevelBasis.leftTranslate_single line 241
  38. theorem OAI.EilenbergGanea.LevelBasis.leftTranslate_front line 244
  39. theorem OAI.EilenbergGanea.LevelBasis.leftTranslate_boundaryTerm line 251
  40. theorem OAI.EilenbergGanea.LevelBasis.leftTranslate_boundary line 257
  41. theorem OAI.EilenbergGanea.LevelBasis.leftTranslate_crossPart line 264
  42. theorem OAI.EilenbergGanea.LevelBasis.includeBasis_translate line 274
  43. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_equivariant line 285
  44. def OAI.EilenbergGanea.LevelBasis.pairShape line 297
  45. theorem OAI.EilenbergGanea.LevelBasis.generator_pair line 300
  46. theorem OAI.EilenbergGanea.LevelBasis.generator_surjective line 305

    Source documentation

    The actual oriented crossing-square edges generate precisely the height kernel.

    theorem generator_surjective (hconn : L.Preconnected) (root : V) :
    Function.Surjective (FreeGroup.lift (generator L (height L) (artinGenerator L) root (height_generator L))) := by
…

    Mentions: OAI.EilenbergGanea.LevelBasis.generator, OAI.EilenbergGanea.artinGenerator, OAI.EilenbergGanea.height_generator

  47. theorem OAI.EilenbergGanea.LevelBasis.artin_total_cycle_bounds line 335

    Source documentation

    The exactness input to the level slicing is the actual RAAG cube-chain contraction, not an assumption about a classifying space.

    theorem artin_total_cycle_bounds {k : ℕ} (hk : 0 < k)
    (c : Chains (ArtinGroup L) V) (hc : c ∈ total (G := ArtinGroup L) L k)
…
  48. theorem OAI.EilenbergGanea.LevelBasis.artin_height_kernel_cd_le_two line 347

    Source documentation

    Integral cd at most two for the genuine height kernel, from a genuine finite augmented link contraction and the dimension of its flag complex.

    theorem artin_height_kernel_cd_le_two (root : V) (hconn : L.Preconnected)
    (K : SimplicialChains.Contraction L)
    (dim : ∀ w, SimplicialChains.Valid L w → w.length ≤ 3) :
    cohomologicalDimension (height L).ker ≤ 2 := by
…

    Mentions: OAI.SimplicialChains.Contraction, OAI.SimplicialChains.Valid

  49. instance OAI.EilenbergGanea.LevelBasis.shape_finite line 368
  50. instance OAI.EilenbergGanea.LevelBasis.shape_fintype line 385
  51. def OAI.EilenbergGanea.LevelBasis.edgeShape line 387
  52. def OAI.EilenbergGanea.LevelBasis.triangleShape line 390
  53. theorem OAI.EilenbergGanea.LevelBasis.generator_edgeShape line 394
  54. theorem OAI.EilenbergGanea.LevelBasis.valid_triangle_edges line 397
  55. theorem OAI.EilenbergGanea.LevelBasis.edge_values_compose line 404
  56. def OAI.EilenbergGanea.LevelBasis.lowerTriangleWord line 420
  57. def OAI.EilenbergGanea.LevelBasis.upperTriangleWord line 423
  58. theorem OAI.EilenbergGanea.LevelBasis.triangle_words_trivial line 428
  59. theorem OAI.EilenbergGanea.LevelBasis.triangle_boundary_low line 446
  60. theorem OAI.EilenbergGanea.LevelBasis.triangle_boundary_high line 469
  61. theorem OAI.EilenbergGanea.LevelBasis.lowerTriangleWord_chain line 510
  62. theorem OAI.EilenbergGanea.LevelBasis.upperTriangleWord_chain line 520
  63. theorem OAI.EilenbergGanea.LevelBasis.triangle_words_chain line 536
  64. def OAI.EilenbergGanea.LevelBasis.triangleWordList line 562
  65. def OAI.EilenbergGanea.LevelBasis.triangleWord line 570
  66. theorem OAI.EilenbergGanea.LevelBasis.shape_three_form line 573
  67. theorem OAI.EilenbergGanea.LevelBasis.triangleWord_trivial line 586
  68. theorem OAI.EilenbergGanea.LevelBasis.triangleWord_chain line 596
  69. theorem OAI.EilenbergGanea.LevelBasis.triangleBoundary_eq_relatorChainMap line 615
  70. def OAI.EilenbergGanea.LevelBasis.triangleBasis line 632
  71. theorem OAI.EilenbergGanea.LevelBasis.triangleBasis_value line 645
  72. def OAI.EilenbergGanea.LevelBasis.levelEquiv line 656
  73. def OAI.EilenbergGanea.LevelBasis.basedLabel line 671
  74. theorem OAI.EilenbergGanea.LevelBasis.basedLabel_edge line 675
  75. theorem OAI.EilenbergGanea.LevelBasis.levelEquiv_edge line 679
  76. theorem OAI.EilenbergGanea.LevelBasis.shape_two_presentation line 690
  77. theorem OAI.EilenbergGanea.LevelBasis.levelEquiv_edge_inv line 701
  78. theorem OAI.EilenbergGanea.LevelBasis.basedLabel_inv_edge line 715
  79. def OAI.EilenbergGanea.LevelBasis.orientedWord line 722
  80. theorem OAI.EilenbergGanea.LevelBasis.orientedWord_value line 730
  81. theorem OAI.EilenbergGanea.LevelBasis.levelEquiv_orientedWord line 742
  82. theorem OAI.EilenbergGanea.LevelBasis.orientedWord_product line 750
  83. theorem OAI.EilenbergGanea.LevelBasis.inverse_edgeWord_product line 761
  84. theorem OAI.EilenbergGanea.LevelBasis.lowerTriangleWord_product line 774
  85. theorem OAI.EilenbergGanea.LevelBasis.upperInnerWord_product line 806
  86. theorem OAI.EilenbergGanea.LevelBasis.upperTriangleWord_product line 835
  87. theorem OAI.EilenbergGanea.LevelBasis.triangleWord_product line 858
  88. def OAI.EilenbergGanea.LevelBasis.walkWord line 870
  89. theorem OAI.EilenbergGanea.LevelBasis.walkWord_endpoint line 874
  90. theorem OAI.EilenbergGanea.LevelBasis.walkWord_product line 887
  91. theorem OAI.EilenbergGanea.LevelBasis.nontrivial_word_of_walk line 900
  92. theorem OAI.EilenbergGanea.LevelBasis.no_boundary_basis_presentation line 928

    Source documentation

    The source obstruction's algebraic endpoint, with no cardinal bound on an alleged presentation. Its geometric premise must still be derived from an ordinary two-dimensional classifying CW space.

    theorem no_boundary_basis_presentation
    (small : ∀ ε : ℝ, 0 < ε →
      ∃ N : ℕ, 1 < N ∧ ∃ a : NegativeLevel L N → V → V → SU2,
      (∀ g q r, a (edgeVertex L N g q r) r q = (a g q r)⁻¹) ∧
      (∀ g q r, dist (a g q r) 1 < ε) ∧
      (∀ g₀ g₁ g₂ q₀ r₀ q₁ r₁ q₂ r₂,
        edgeVertex L N g₀ q₀ r₀ = g₁ →
        edgeVertex L N g₁ q₁ r₁ = g₂ →
        edgeVertex L N g₂ q₂ r₂ = g₀ →
        a g₀ q₀ r₀ * a g₁ q₁ r₁ * a g₂ q₂ r₂ = 1) ∧
      ∃ (g : NegativeLevel L N) (p : Walk L N g g), p.eval a ≠ 1)
    {A R : Type*} (a₀ : A → (height L).ker)
…

    Mentions: OAI.EilenbergGanea.SU2