OAI/AlgebraicGeometry/CharacterVarieties/Frames/FrameTransport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Transport of local frames along seams

The column and parent coordinate identifications transport local frame matrices between the two ends of a surface seam.

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portParentMatch_index line 18
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFrameUnit_match line 26
  3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFrameUnit_rebase_match line 35
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_match line 43
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_seam_of_ports line 51
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.attachedEnds_same line 67
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_seam_match line 71