OAI/Geometry/HyperbolicGroups/ActualPosition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.ConeSkeleton.squareField line 18
  2. lemma OAI.HyperbolicObstruction.ConeSkeleton.squareField_injective line 22
  3. lemma OAI.HyperbolicObstruction.ConeSkeleton.squareField_surjective line 27
  4. def OAI.HyperbolicObstruction.ConeSkeleton.rawToPosition line 38

    Source documentation

    Reindexing uses the original edge/decoration field, never its label value.

    def rawToPosition : RawPosition n w d → (occurrenceShape n w).Pos (Fintype.card (Six n d))
  | .inl a => .inl (enumTop n w a)
  | .inr (.inl ⟨b,e⟩) => .inr (.inl ⟨enumFan n w b,⟨.inl e.val,by
      simpa only [occurrenceShape,Equiv.symm_apply_apply,rowSupport,Finset.mem_map,
        Function.Embedding.inl_apply,Sum.inl.injEq,exists_eq_right] using e.property⟩⟩)
  | .inr (.inr (.inl (s,i))) => .inr (.inr (.inl ⟨enumSquare n w s,⟨(squareField s.1 i).val,by
      simpa only [occurrenceShape,Equiv.symm_apply_apply,rowSupport] using (squareField s.1 i).property⟩⟩))
  | .inr (.inr (.inr (s,i))) => .inr (.inr (.inr (enumSix n d s,i)))

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RawPosition, OAI.HyperbolicObstruction.ConeSkeleton.occurrenceShape, OAI.HyperbolicObstruction.ConeSkeleton.Six, OAI.HyperbolicObstruction.ConeSkeleton.enumTop, OAI.HyperbolicObstruction.ConeSkeleton.enumFan, OAI.HyperbolicObstruction.ConeSkeleton.enumSquare, OAI.HyperbolicObstruction.ConeSkeleton.squareField, OAI.HyperbolicObstruction.ConeSkeleton.enumSix

  5. lemma OAI.HyperbolicObstruction.ConeSkeleton.rawToPosition_injective line 47
  6. lemma OAI.HyperbolicObstruction.ConeSkeleton.rawToPosition_surjective line 68