OAI/AlgebraicGeometry/CharacterVarieties/Frames/Mirror.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorColor_eq line 15
  2. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.child_color_ne line 21
  3. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_basis line 29
  4. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.transverse_parent_color line 55
  5. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.transverse_frame_seam line 68

    Source documentation

    The transverse branch has smaller parent rank, so its parent and child transports are identities under the mirror principal gauge.

    lemma transverse_frame_seam (T : MatrixIso K (Fin r) (Fin r))
    (v : Fin (w.shape.atomicBand.length+1)) (p : (w.shape.atomicBand.kind v).table.Port)
    (hin : p≠(w.shape.atomicBand.kind v).input) (hout : p≠(w.shape.atomicBand.kind v).output) :
    (w.mirrorVertexFrames T v ((w.shape.atomicBand.kind v).mirrorPort p)).reindex
      ((w.shape.vertexAtoms v).seamColumns (w.shape.vertexAtoms v).mirror
        p ((w.shape.atomicBand.kind v).mirrorPort p) ((w.shape.atomicBand.kind v).mirrorChild p)
        (fun a => ((w.shape.vertexAtoms v).mirror_atoms ⟨p,some a⟩).symm))
      (finCongr ((w.shape.vertexAtoms v).rank_of_atoms (w.shape.vertexAtoms v).mirror
        ((w.shape.vertexAtoms v).mirror_atoms ⟨p,none⟩).symm))=w.vertexFrames v p := by
…

    Mentions: OAI.IntegralCharacterVarieties.MatrixIso

  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCut_orig_localRanks line 99
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCut_mirror_localRanks line 104
  8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCutOrigFrames line 110
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCutMirrorFrames line 112
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCutVertexFrames line 116
  11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCutPortFrames line 127
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.namedCutPortFrames_holds line 132
  13. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSideValues line 161

    Source documentation

    The selected original parent side changes from P to J; children retain their transports over the coefficient ring.

    def cutOldSideValues (old : D.SideValues (R:=R)) (J : (Matrix (Fin (D.rank (D.ports.facet ⟨q,none⟩))) (Fin (D.rank (D.ports.facet ⟨q,none⟩))) R)ˣ) : D.SideValues (R:=R)
…
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSideValues_selected line 165
  15. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutOldSideValues_child line 167
  16. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutShortSideValues line 172

    Source documentation

    New strip sides have identity transport except for the mirror principal short seam, which carries Y = T⁻¹ J⁻¹ P T.

    def cutShortSideValues (Y : (Matrix (Fin (D.rank (D.ports.facet ⟨q,none⟩))) (Fin (D.rank (D.ports.facet ⟨q,none⟩))) R)ˣ) (b : Bool) (i : Option (Fin (arity q))) :
    FacetUnit (R:=R) D.rank (D.ports.facet ⟨q,i⟩) := by
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FacetUnit

  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedGenus_inl_le line 178
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues line 185
  19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutHandleValues line 194

    Source documentation

    The original handles are retained except for the last handle of the selected parent. New strip facets are disks.

    def refinedCutHandleValues (old : D.HandleValues (R:=R)) : (C).HandleValues (R:=R) := by
…

    Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.HandleValues