Documentation

LeanPool.ClassificationOfSurfaces.FiniteCyclicMoves

Finite cyclic move closures #

This file combines signed presentation isomorphisms and the two primitive Gallier--Xu subdivisions into stable closure APIs.

Subdivides is the directed reflexive-transitive closure. It preserves ordinary validity, connectivity, and Gallier validity. HasCommonSubdivision P Q supplies a validity-safe common target for topological comparison: starting with two ordinary-valid presentations, both forward chains remain ordinary-valid. This is stronger operational data than an unrestricted symmetric move chain, which may pass through the exceptional empty-word sphere where PolygonalRealization is deliberately unavailable.

MoveEquivalent is also provided as the purely syntactic equivalence closure. A common subdivision implies move equivalence, but no converse or confluence theorem is asserted here.

source
def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep (P Q : FiniteCyclicPresentation) :
Prop

One directed presentation step: a signed isomorphism, P1 subdivision, or P2 subdivision.

Equations
Instances For
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.signedIso {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) :
    P.SubdivisionStep Q
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.p1 {P Q : FiniteCyclicPresentation} (h : P.P1Subdivision Q) :
    P.SubdivisionStep Q
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.p2 {P Q : FiniteCyclicPresentation} (h : P.P2Subdivision Q) :
    P.SubdivisionStep Q
    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.isSurfaceValid {P Q : FiniteCyclicPresentation} (hPQ : P.SubdivisionStep Q) (validP : P.IsSurfaceValid) :
    Q.IsSurfaceValid

    Every directed step preserves ordinary surface incidence validity.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.isConnected {P Q : FiniteCyclicPresentation} (hPQ : P.SubdivisionStep Q) (connectedP : P.IsConnected) :
    Q.IsConnected

    Every directed step preserves face-incidence connectivity.

    source
    theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.isGallierValid {P Q : FiniteCyclicPresentation} (hPQ : P.SubdivisionStep Q) (validP : P.IsGallierValid) :
    Q.IsGallierValid

    Every directed step preserves the packed Gallier--Xu validity predicate.

    source
    def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides (P Q : FiniteCyclicPresentation) :
    Prop

    Directed finite subdivision by signed isomorphisms, P1, and P2.

    Equations
    Instances For
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.refl (P : FiniteCyclicPresentation) :
      P.Subdivides P
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.single {P Q : FiniteCyclicPresentation} (h : P.SubdivisionStep Q) :
      P.Subdivides Q
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.signedIso {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) :
      P.Subdivides Q
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.p1 {P Q : FiniteCyclicPresentation} (h : P.P1Subdivision Q) :
      P.Subdivides Q
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.p2 {P Q : FiniteCyclicPresentation} (h : P.P2Subdivision Q) :
      P.Subdivides Q
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.trans {P Q R : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (hQR : Q.Subdivides R) :
      P.Subdivides R
      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.isSurfaceValid {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (validP : P.IsSurfaceValid) :
      Q.IsSurfaceValid

      Directed subdivision chains preserve ordinary surface incidence validity.

      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.isConnected {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (connectedP : P.IsConnected) :
      Q.IsConnected

      Directed subdivision chains preserve face-incidence connectivity.

      source
      theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.isGallierValid {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (validP : P.IsGallierValid) :
      Q.IsGallierValid

      Directed subdivision chains preserve Gallier validity.

      source
      def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision (P Q : FiniteCyclicPresentation) :
      Prop

      Two presentations have a common directed subdivision.

      Equations
      Instances For
        source
        theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision.refl (P : FiniteCyclicPresentation) :
        P.HasCommonSubdivision P
        source
        theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision.symm {P Q : FiniteCyclicPresentation} (h : P.HasCommonSubdivision Q) :
        Q.HasCommonSubdivision P
        source
        def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.MoveEquivalent (P Q : FiniteCyclicPresentation) :
        Prop

        Purely syntactic equivalence generated by signed isomorphisms, P1, and P2.

        Equations
        Instances For
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.MoveEquivalent.refl (P : FiniteCyclicPresentation) :
          P.MoveEquivalent P
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.MoveEquivalent.ofStep {P Q : FiniteCyclicPresentation} (h : P.SubdivisionStep Q) :
          P.MoveEquivalent Q
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.MoveEquivalent.symm {P Q : FiniteCyclicPresentation} (h : P.MoveEquivalent Q) :
          Q.MoveEquivalent P
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.MoveEquivalent.trans {P Q R : FiniteCyclicPresentation} (hPQ : P.MoveEquivalent Q) (hQR : Q.MoveEquivalent R) :
          P.MoveEquivalent R
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.moveEquivalent {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) :
          P.MoveEquivalent Q

          Every directed subdivision chain is a syntactic move equivalence.

          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision.moveEquivalent {P Q : FiniteCyclicPresentation} (h : P.HasCommonSubdivision Q) :
          P.MoveEquivalent Q

          A common directed subdivision is in particular a syntactic move equivalence.

          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonallyEquivalent.refl (P : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) :
          P.PolygonallyEquivalent P validP validP
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonallyEquivalent.symm {P Q : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} (h : P.PolygonallyEquivalent Q validP validQ) :
          Q.PolygonallyEquivalent P validQ validP
          source
          theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PolygonallyEquivalent.trans {P Q R : FiniteCyclicPresentation} {validP : P.IsSurfaceValid} {validQ : Q.IsSurfaceValid} {validR : R.IsSurfaceValid} (hPQ : P.PolygonallyEquivalent Q validP validQ) (hQR : Q.PolygonallyEquivalent R validQ validR) :
          P.PolygonallyEquivalent R validP validR
          source
          def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.PreservesPolygonalRealization :
          Prop

          The stable proof obligation for primitive realization invariance.

          The P1 and P2 realization files discharge the corresponding disjuncts; signed isomorphisms are already implemented by SignedPresentationIso.polygonallyEquivalent.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1Subdivision.PreservesPolygonalRealization :
            Prop

            The realization-invariance obligation isolated to P1 subdivisions.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.PreservesPolygonalRealization :
              Prop

              The realization-invariance obligation isolated to P2 subdivisions.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SubdivisionStep.preservesPolygonalRealization (hP1 : P1Subdivision.PreservesPolygonalRealization) (hP2 : P2Subdivision.PreservesPolygonalRealization) :
                PreservesPolygonalRealization

                Signed-isomorphism invariance plus the two primitive geometric obligations supplies invariance for every directed elementary step.

                source
                theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.polygonallyEquivalent (hprimitive : SubdivisionStep.PreservesPolygonalRealization) {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) :
                P.PolygonallyEquivalent Q validP validQ

                If every primitive directed step preserves the faithful polygonal quotient, so does every directed subdivision chain.

                source
                theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision.polygonallyEquivalent (hprimitive : SubdivisionStep.PreservesPolygonalRealization) {P Q : FiniteCyclicPresentation} (h : P.HasCommonSubdivision Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) :
                P.PolygonallyEquivalent Q validP validQ

                Primitive realization invariance promotes a common-subdivision certificate to a homeomorphism of faithful polygonal quotients.