OAI/AlgebraicGeometry/CharacterVarieties/Frames/NamedSeams.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_reindex line 11
2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedParentLinear line 30
3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedChildInverse line 31
4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedSeamLeft line 34
5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedSeamRight line 55
6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_named_seam line 70

   Source documentation

   The named seam relation of a solution.

   lemma old_named_seam [Algebra R K] (P : D.Punctures R) (x : D.Solution P K) :
       SameFramedFlag (fun i : (i : Fin (arity q)) × Fin (D.childDim q i) => i.1.val)
         ((D.namedSeamFrame q (x.val.val (.frame q false))).trans (D.namedParentLinear q x.val.val))
         ((D.namedChildInverse q x.val.val).trans (D.namedSeamFrame q (x.val.val (.frame q true)))) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.SameFramedFlag

7. lemma OAI.IntegralCharacterVarieties.MatrixIso.sameFramedFlag_reindex_iff line 99
8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.named_seam_iff line 121