OAI/AlgebraicGeometry/CharacterVarieties/Frames/InheritedFrames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.transportInheritedFrames_coordinates line 10
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedColumns line 38
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedRows line 42
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInherited_attach line 47
  5. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedFrameCoordinates line 60

    Source documentation

    Every inherited port frame agrees with the original frame in the original seam coordinates.

    def CutInheritedFrameCoordinates : Prop :=
…
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInherited_frameCoordinates line 68
  7. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedChildLabels line 78

    Source documentation

    The inherited column coordinates keep the original child label.

    def CutInheritedChildLabels : Prop :=
…
  8. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedColumns_childEnumeration line 83
  9. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CutInheritedColumnValues line 92

    Source documentation

    The inherited column coordinates keep the position inside each child.

    def CutInheritedColumnValues : Prop :=
…
  10. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cutInheritedColumns_value line 96