OAI/Geometry/HyperbolicGroups/FinitePolyhedronVoltage.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A literal flat principal covering of a barycentric polyhedron, obtained from edge voltages satisfying exactly the two-dimensional face relations. The topology is Mathlib's fiber-bundle gluing topology, not the product. This construction does not assert that the cover is simply connected.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.openStar line 18

    Source documentation

    The open star of a vertex in the actual barycentric realization.

    def openStar (v : V) : Set (Carrier K) := {x | 0 < x.val v}

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier

  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.openStar_isOpen line 20
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.exists_positive line 23
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.face_of_positive line 32
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.triangle_of_positive line 42
  6. structure OAI.HyperbolicObstruction.FinitePolyhedron.Voltage line 53

    Source documentation

    An edge-voltage cocycle. Values off the edge set are immaterial.

    structure Voltage where
…
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.reverse line 62
  8. def OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.core line 74

    Source documentation

    Charts retain the positive barycentric coordinate of their chosen vertex. Multiplicative transition functions are locally constant, with the literal triangular relation providing their cocycle identity.

    def core : FiberBundleCore V (Carrier K) G where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier

  9. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.TotalSpace line 86
  10. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.proj line 87
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.isCoveringMap line 89
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.Voltage.proj_surjective line 91