OAI/AlgebraicGeometry/CharacterVarieties/Seams/InternalSeams.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Internal seam equations

Compatibility of the frames on adjacent original, reflected, and transverse branches of an identified band.

  1. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.OriginalChildrenMatch line 26

    Source documentation

    The child identifications across every original internal seam.

    def OriginalChildrenMatch : Prop :=
…
  2. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origChildMatch line 31
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.OriginalFrameMatch line 63

    Source documentation

    Compatibility of the transported frames across an original internal seam.

    def OriginalFrameMatch (j : Fin w.shape.atomicBand.length) : Prop :=
…
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origFrameMatch line 70
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.OriginalFrameValuesAgree line 88

    Source documentation

    Equality of the two frame values on an original internal seam.

    def OriginalFrameValuesAgree (j : Fin w.shape.atomicBand.length) : Prop :=
…
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.origFrameValues_eq line 97
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues_original_succ line 123
  8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandValues_mirror_castSucc line 131
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.OriginalInternalSideValuesTrivial line 158

    Source documentation

    The side values on every original internal seam are trivial.

    def OriginalInternalSideValuesTrivial : Prop :=
…
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_original_succ line 163
  11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInternalSideValuesTrivial line 171

    Source documentation

    The side values on every reflected internal seam are trivial.

    def MirrorInternalSideValuesTrivial : Prop :=
…
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_mirror_castSucc line 176
  13. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.trivialSides_seam_eq line 193
  14. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.trivialSides_seamHolds line 211
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.OriginalInternalFlagsHold line 245

    Source documentation

    The framed flag equations on every original internal seam.

    def OriginalInternalFlagsHold : Prop :=
…
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.originalInternal_seamHolds line 253
  17. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.interiorChild_enumeration line 276
  18. lemma OAI.IntegralCharacterVarieties.NamedBandGrades.IdentifiedBand.mirrorInteriorChild_enumeration line 283
  19. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorOutputAttached line 312

    Source documentation

    The attachment of each reflected output port.

    def MirrorOutputAttached : Prop :=
…
  20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorOutput_attach line 316
  21. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInputAttached line 323

    Source documentation

    The attachment of each reflected input port.

    def MirrorInputAttached : Prop :=
…
  22. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorInput_attach line 327
  23. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorAdjacentSeamsAgree line 337

    Source documentation

    Adjacent reflected ports attach to the same seam.

    def MirrorAdjacentSeamsAgree : Prop :=
…
  24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorAdjacentSame line 341
  25. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorChildrenMatch line 362

    Source documentation

    The child identifications across every reflected internal seam.

    def MirrorChildrenMatch : Prop :=
…
  26. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorChildMatch line 368
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_eq_of_matched_ports line 386
  28. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFrameMatch line 420

    Source documentation

    Compatibility of the transported frames across a reflected internal seam.

    def MirrorFrameMatch (j : Fin w.shape.atomicBand.length) : Prop :=
…
  29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorFrameMatch line 429
  30. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorFrameValuesAgree line 449

    Source documentation

    Equality of the two frame values on a reflected internal seam.

    def MirrorFrameValuesAgree (j : Fin w.shape.atomicBand.length) : Prop :=
…
  31. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorFrameValues_eq line 458
  32. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MirrorInternalFlagsHold line 496

    Source documentation

    The framed flag equations on every reflected internal seam.

    def MirrorInternalFlagsHold : Prop :=
…
  33. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mirrorInternal_seamHolds line 504
  34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_plus_branch line 526
  35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_minus_branch line 529
  36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_plus_branch_neg line 532
  37. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_minus_branch_neg line 535
  38. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.PositiveBranch line 542
  39. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.NegativeBranch line 544
  40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchPlus line 546
  41. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchMinus line 548
  42. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchNegPlus line 550
  43. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchNegMinus line 552
  44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_branchPlus line 554
  45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_branchNegPlus line 561
  46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.positive_not_output line 577
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.negative_not_input line 582
  48. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.exposed_positive_not_input line 587
  49. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VariableGallery.exposed_negative_not_output line 600
  50. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchOriginalAttached line 633

    Source documentation

    The attachment of the original port of a positive transverse branch.

    def PositiveBranchOriginalAttached : Prop :=
…
  51. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_original_attach line 638
  52. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchMirrorAttached line 644

    Source documentation

    The attachment of the reflected port of a positive transverse branch.

    def PositiveBranchMirrorAttached : Prop :=
…
  53. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_mirror_attach line 649
  54. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchSameSeam line 658

    Source documentation

    The two ports of each positive transverse branch attach to the same seam.

    def PositiveBranchSameSeam : Prop :=
…
  55. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_same line 664
  56. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_not_input line 672
  57. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_not_output line 677
  58. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchChildrenMatch line 680

    Source documentation

    The child identifications along each positive transverse branch.

    def PositiveBranchChildrenMatch : Prop :=
…
  59. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_childMatch line 686
  60. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchFrameMatch line 718

    Source documentation

    Compatibility of the transported frames across a positive transverse branch.

    def PositiveBranchFrameMatch : Prop :=
…
  61. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPosFrameMatch line 723
  62. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchFrameValuesAgree line 739

    Source documentation

    Equality of the two frame values on a positive transverse branch.

    def PositiveBranchFrameValuesAgree : Prop :=
…
  63. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPosFrameValues_eq line 742
  64. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchOriginalAttached line 769

    Source documentation

    The attachment of the original port of a negative transverse branch.

    def NegativeBranchOriginalAttached : Prop :=
…
  65. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_original_attach line 774
  66. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchMirrorAttached line 783

    Source documentation

    The attachment of the reflected port of a negative transverse branch.

    def NegativeBranchMirrorAttached : Prop :=
…
  67. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_mirror_attach line 788
  68. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchSameSeam line 794

    Source documentation

    The two ports of each negative transverse branch attach to the same seam.

    def NegativeBranchSameSeam : Prop :=
…
  69. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_same line 800
  70. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_not_input line 808
  71. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_not_output line 811
  72. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchChildrenMatch line 816

    Source documentation

    The child identifications along each negative transverse branch.

    def NegativeBranchChildrenMatch : Prop :=
…
  73. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_childMatch line 822
  74. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchFrameMatch line 854

    Source documentation

    Compatibility of the transported frames across a negative transverse branch.

    def NegativeBranchFrameMatch : Prop :=
…
  75. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNegFrameMatch line 859
  76. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchFrameValuesAgree line 875

    Source documentation

    Equality of the two frame values on a negative transverse branch.

    def NegativeBranchFrameValuesAgree : Prop :=
…
  77. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNegFrameValues_eq line 878
  78. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchSideValuesTrivial line 904

    Source documentation

    The side values on each positive transverse branch are trivial.

    def PositiveBranchSideValuesTrivial : Prop :=
…
  79. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_branchPos line 909
  80. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchSideValuesTrivial line 921

    Source documentation

    The side values on each negative transverse branch are trivial.

    def NegativeBranchSideValuesTrivial : Prop :=
…
  81. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutSideValues_branchNeg line 926
  82. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PositiveBranchFlagsHold line 962

    Source documentation

    The framed flag equations on each positive transverse branch.

    def PositiveBranchFlagsHold : Prop :=
…
  83. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchPos_seamHolds line 972
  84. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.NegativeBranchFlagsHold line 987

    Source documentation

    The framed flag equations on each negative transverse branch.

    def NegativeBranchFlagsHold : Prop :=
…
  85. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.branchNeg_seamHolds line 997