OAI/Geometry/HyperbolicGroups/Polygons.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.IntegralIncidence.Polygons.offset line 18

   Source documentation

   Basing a lift at the first boundary vertex fixes every corner lift.

   def offset (c : C) (i : Fin (B.size c)) : G :=
   …

2. def OAI.HyperbolicObstruction.IntegralIncidence.Polygons.liftedSide line 21
3. def OAI.HyperbolicObstruction.IntegralIncidence.Polygons.faceBoundary line 24
4. def OAI.HyperbolicObstruction.IntegralIncidence.Polygons.d₂ line 27
5. lemma OAI.HyperbolicObstruction.IntegralIncidence.Polygons.offset_next line 33
6. lemma OAI.HyperbolicObstruction.IntegralIncidence.Polygons.liftedSide_closed line 38
7. lemma OAI.HyperbolicObstruction.IntegralIncidence.Polygons.boundary_faceBoundary line 47
8. theorem OAI.HyperbolicObstruction.IntegralIncidence.Polygons.boundary_boundary line 59

   Source documentation

   The independently indexed lifted integral incidence is a chain complex.

   theorem boundary_boundary (z : (G × C) →₀ ℤ) :
       d₁ B.start voltage (B.d₂ voltage z) = 0 := by
   …

   Mentions: OAI.HyperbolicObstruction.IntegralIncidence.d₁

9. lemma OAI.HyperbolicObstruction.IntegralIncidence.Polygons.d₁_comp_d₂ line 69