OAI/Geometry/HyperbolicGroups/CyclicTriangleBoundary.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Integral boundary elimination for a collared fan triangulation of a polygon. Independent lifted polygons may index C; there is no finite-cover or coefficient-identification assumption. This is chain algebra, not a claim of topological Hurewicz or cellular approximation.

  1. abbrev OAI.HyperbolicObstruction.CyclicTriangleBoundary.Corner line 16
  2. abbrev OAI.HyperbolicObstruction.CyclicTriangleBoundary.Triangle line 17
  3. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.next line 19
  4. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.first line 20
  5. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.first_injective line 21
  6. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.collapse line 25
  7. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.expansionColumn line 28
  8. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.expand line 31
  9. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.expansionColumn_apply line 34
  10. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.expand_apply line 53
  11. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.rotate_invariant_constant line 64
  12. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.expand_collapse line 79

    Source documentation

    The three internal edge coordinates force every triangle in a lifted polygon to have one common coefficient.

    lemma expand_collapse (z : Triangle size →₀ ℤ)
    (diag : ∀ q, z (q,1) = z (q,0))
    (outer : ∀ q, z (q,2) = z (q,1))
    (radial : ∀ q, z (next size q,2) = z (q,2)) :
    expand size (collapse size pos z) = z := by
…

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.Triangle, OAI.HyperbolicObstruction.CyclicTriangleBoundary.next, OAI.HyperbolicObstruction.CyclicTriangleBoundary.expand, OAI.HyperbolicObstruction.CyclicTriangleBoundary.collapse

  13. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.polygonBoundary line 99
  14. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.polygonD₂ line 100
  15. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.graphPart line 102
  16. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.graphPart_expand line 105
  17. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.cycle_zero line 117

    Source documentation

    Full independent cycle elimination, not a scalar augmentation test.

    lemma cycle_zero (hinj : Function.Injective (polygonD₂ size edge))
    (z : Triangle size →₀ ℤ)
    (graph : graphPart size edge z = 0)
    (diag : ∀ q, z (q,1) = z (q,0))
    (outer : ∀ q, z (q,2) = z (q,1))
    (radial : ∀ q, z (next size q,2) = z (q,2)) : z = 0 := by
…

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.polygonD₂, OAI.HyperbolicObstruction.CyclicTriangleBoundary.Triangle, OAI.HyperbolicObstruction.CyclicTriangleBoundary.graphPart, OAI.HyperbolicObstruction.CyclicTriangleBoundary.next

  18. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.prev line 131

    Source documentation

    The previous boundary occurrence, within the same independent polygon.

    def prev (q : Corner size) : Corner size := ⟨q.1,(finRotate _).symm q.2⟩

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.Corner

  19. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.prev_next line 133
  20. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.next_prev line 137
  21. def OAI.HyperbolicObstruction.CyclicTriangleBoundary.fullD₂ line 146

    Source documentation

    Full oriented boundary in edge coordinates. The internal factors are, respectively, radial, collar diagonal, outer and apex edges. Their indices include the entire independent polygon index; no deck augmentation occurs. The graph factor can itself be an arbitrary lifted-edge module.

    def fullD₂ : (Triangle size →₀ ℤ) →ₗ[ℤ]
    ((A →₀ ℤ) × (Corner size → ℤ) × (Corner size → ℤ) ×
      (Corner size → ℤ) × (Corner size → ℤ)) where
…

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.Triangle, OAI.HyperbolicObstruction.CyclicTriangleBoundary.Corner

  22. lemma OAI.HyperbolicObstruction.CyclicTriangleBoundary.fullD₂_injective line 162

    Source documentation

    Elimination of the actual collared-fan boundary equations.

    lemma fullD₂_injective (hinj : Function.Injective (polygonD₂ size edge)) :
    Function.Injective (fullD₂ size edge) := by
…

    Mentions: OAI.HyperbolicObstruction.CyclicTriangleBoundary.polygonD₂, OAI.HyperbolicObstruction.CyclicTriangleBoundary.fullD₂