OAI/Geometry/HyperbolicGroups/BoundaryLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.pullback_surviving line 19

   Source documentation

   A literal boundary can be pulled back through an injective survival map, provided every one of its sides survives and its successor is retained.

   lemma IsBoundary.pullback_surviving {D E : Type*} [DecidableEq D] [DecidableEq E]
       {p : Perm D} {q : Perm E} {xs : List D} (h : IsBoundary p xs)
       (j : E → D) (hj : Function.Injective j)
       (hcomplete : ∀ x ∈ xs, ∃ y, j y = x)
       (hface : ∀ y, j y ∈ xs → j (q y) = p (j y)) :
       ∃ ys : List E, IsBoundary q ys ∧ ys.map j = xs := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

2. theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Preserves.boundary line 48

   Source documentation

   Protected-boundary normalization retains the EXACT enumerated word, not merely its conjugacy class or its image in the presented group.

   theorem Preserves.boundary (hPQ : P.Preserves keep Q)
       (hk : ∀ s, keep s → T.free (T.kind s) = false)
       (xs : List P.Dart) (hx : IsBoundary P.pairing.face xs)
       (hs : ∀ x, keep (P.index x) ↔ x ∈ xs) :
       ∃ ys : List Q.Dart, IsBoundary Q.pairing.face ys ∧
         ys.map hPQ.map = xs ∧
         ys.map (T.label ∘ Q.index) = xs.map (T.label ∘ P.index) ∧
         ∀ y, keep (Q.index y) ↔ y ∈ ys := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary