OAI/AlgebraicGeometry/CharacterVarieties/Frames/PortCoordinates.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portNamedFrame line 14
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutPortAttached line 51

    Source documentation

    A port of the cut diagram is attached to a specified seam end.

    def CutPortAttached (p : LocalPort _ (BandGraft.kind (A) q (B)))
    (e : (W).Seam × Bool) : Prop :=
…
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutPortsAdjacent line 56

    Source documentation

    Two ports of the cut diagram meet the same seam.

    def CutPortsAdjacent (p u : LocalPort _ (BandGraft.kind (A) q (B))) : Prop :=
…
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origInput_attach line 58
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origOutput_attach line 63
  6. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_vertex_frame_seam line 83
  7. def OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorInteriorChild line 105
  8. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_interior_parent line 113
  9. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_interior_child line 124
  10. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirror_interior_frame_seam line 141
  11. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.firstOldNegative_attach line 169
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastOriginalOutput_attach line 179
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.lastOldPositive_attach line 191
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorFirstInput_attach line 198
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.transportFrames_seam line 226
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portChildMatch_enumeration line 260
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origAdjacentSame line 267
  18. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portChildMatch_eq_of_enumeration line 284
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.firstAdjacentSame line 309
  20. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstChild line 316
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutFirstChild_enumeration line 323
  22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.firstCutChildTransport line 332

    Source documentation

    Child transport from the old negative end to the first vertex of the cut band.

    def firstCutChildTransport :
    (D.ports.kind (oo).1).table.Child (oo).2 ≃
      (w.shape.atomicBand.kind 0).table.Child (w.shape.atomicBand.kind 0).input :=
…
  23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.firstChildMatch line 338
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.columnCongr_sandwich line 352
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.LocalRanks.parentCongr_sandwich line 367
  26. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.transported_portFrame_match line 383
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.seamGrade_portColumnIndex line 420
  28. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame_namedCoordinates line 429