OAI/AlgebraicGeometry/CharacterVarieties/Frames/SeamFactors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamLeft_coordinates line 16

   Source documentation

   Coordinates of the left seam word compose the frame and parent transports.

   lemma seamLeft_coordinates
       (e : α ≃ Fin (D.seamDim s)) (f : β ≃ Fin (D.seamDim s))
       (x : (α → K) ≃ₗ[K] (β → K)) (p : (β → K) ≃ₗ[K] (β → K))
       (hx : ((MatrixIso.unit (g (.frame s false))).reindex e f).linearEquiv=x)
       (hp : ((MatrixIso.unit ((D.parentWord s).eval φ g)).reindex f f).linearEquiv=p) :
       ((MatrixIso.unit ((D.seamLeft s).eval φ g)).reindex e f).linearEquiv=x.trans p := by
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit

2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamRight_coordinates line 27

   Source documentation

   Coordinates of the right seam word compose the child inverse and frame transports.

   lemma seamRight_coordinates
       (e : α ≃ Fin (D.seamDim s)) (f : β ≃ Fin (D.seamDim s))
       (y : (α → K) ≃ₗ[K] (β → K)) (u : (α → K) ≃ₗ[K] (α → K))
       (hy : ((MatrixIso.unit (g (.frame s true))).reindex e f).linearEquiv=y)
       (hu : ((MatrixIso.unit ((Term.block (D.childDim s)
         (fun j => Term.inv (D.childWord s j))).eval φ g)).reindex e e).linearEquiv=u) :
       ((MatrixIso.unit ((D.seamRight s).eval φ g)).reindex e f).linearEquiv=u.trans y := by
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit

3. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamHolds_of_wordCoordinates line 40

   Source documentation

   Common coordinates for the two complete seam words determine their framed flag equation.

   lemma seamHolds_of_wordCoordinates
       (e : α ≃ Fin (D.seamDim s)) (f : β ≃ Fin (D.seamDim s))
       (a : α → ℕ) (x y : (α → K) ≃ₗ[K] (β → K))
       (ha : ∀ i,D.seamGrade s (e i)=a i)
       (hx : ((MatrixIso.unit ((D.seamLeft s).eval φ g)).reindex e f).linearEquiv=x)
       (hy : ((MatrixIso.unit ((D.seamRight s).eval φ g)).reindex e f).linearEquiv=y)
       (hh : SameFramedFlag a x y) :
       SameFramedFlag (D.seamGrade s)
         (matrixUnitEquiv ((D.seamLeft s).eval φ g))
         (matrixUnitEquiv ((D.seamRight s).eval φ g)) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.MatrixIso.unit, OAI.IntegralCharacterVarieties.SameFramedFlag