OAI/Geometry/HyperbolicGroups/MappedPicture.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.ext line 21
2. instance OAI.HyperbolicObstruction.PictureSwitch.PictureMap.(instance at line 28) line 28
3. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Respects line 37

   Source documentation

   Literal oriented-edge and vertex labels into any target one-skeleton. The vertex label of a dart is the initial vertex of its oriented edge label. No filling or normal-form conclusion is included in this compatibility.

   def Respects (M : PictureMap D) (label : D → L) (start : L → V) (rev : L → L) : Prop :=
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.switch_respects line 42
5. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.normalize_radial line 67

   Source documentation

   A finite normalizing producer for radial labels on actual side-pairings. The same darts, face cycles and mapped oriented edge labels are retained. Thus all face maps/lifted face chains remain unchanged. Genus zero is retained by the checked switch theorem, not assumed of the output.

   radial is the target incidence fact: every edge starting at an apex ends at an ordinary vertex. The conclusion says each outgoing radial label occurs at most once in each actual apex vertex-link cycle.

   theorem normalize_radial {M : PictureMap D} {label : D → L} {start : L → V} {rev : L → L}
       (isApex : V → Bool) (hM : M.Respects label start rev) (hG : M.GenusZero)
       (radial : ∀ d, isApex (start (label d)) = true →
         isApex (start (rev (label d))) = false) :
       ∃ N : PictureMap D, N.face = M.face ∧ N.Respects label start rev ∧ N.GenusZero ∧
         ∀ a b, isApex (start (label a)) = true → N.vertex.SameCycle a b →
           label a = label b → a = b := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap