Documentation

TauCeti.KnotTheory.PDCode.ResolvedCircle.Transport

Transport of the circles of a smoothed PD-code #

The circles of a smoothed PD-code (TauCeti.PDCode.ResolvedCircle) are built from half-edge labels, so two codes describing the same smoothed diagram have different, but canonically bijective, circle types. The Khovanov chain groups are tensor products indexed by these circles, so every comparison of diagrams has to carry such a bijection along, functorially.

A TauCeti.PDCode.SmoothingEquiv D s D' s' is a bijection of half-edges carrying the arcs of D to the arcs of D' and the traversal of D smoothed by s to the traversal of D' smoothed by s', together with a bijection between the labels of the crossing-free circles. It induces a bijection of resolved circles, TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr, sending the circle through a half-edge to the circle through its image. Smoothing equivalences form a groupoid, and the induced bijections respect identities, inverses and composition.

Transport carrying the slots of a crossing bijectively preserves the circles through that crossing and hence their number. When the source and target transports of a saddle use the same half-edge and isolated-circle bijections, the induced circle bijections commute with its saddle correspondence. This supplies the circle-level naturality square for resolution maps.

The smoothing equivalences provided here are those of the native operations which keep the smoothed diagram:

A TauCeti.PDCode.ResolutionEquiv D D' identifies all smoothings of D with those of D' at once, along a bijection of crossings, by one half-edge bijection and one bijection of crossing-free labels. It gives a smoothing equivalence for every state, and so transports the whole cube of resolutions. Relabelling, reading a crossing from another slot and permuting the crossing-free labels are such identifications.

Finally, the circles of a disjoint union (TauCeti.PDCode.disjointUnion) are the circles of the two summands, smoothed by the two restrictions of the state (TauCeti.PDCode.disjointUnionResolvedCircleEquiv).

Main definitions #

Main results #

References #

source
structure TauCeti.PDCode.SmoothingEquiv {n m : ℕ} (D : PDCode n) (s : Fin n → Bool) (D' : PDCode m) (s' : Fin m → Bool) :
Type

An isomorphism between the PD-code D smoothed according to the state s and the PD-code D' smoothed according to s': a bijection of half-edges carrying the arc matching of D to that of D' and the smoothed traversal TauCeti.PDCode.statePerm D s to D'.statePerm s', together with a bijection between the labels of the crossing-free circles. It induces a bijection between the circles of the two smoothed diagrams (TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr).

Instances For
    source
    theorem TauCeti.PDCode.SmoothingEquiv.ext_iff {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {x y : D.SmoothingEquiv s D' s'} :
    x = y ↔ x.halfEdgeEquiv = y.halfEdgeEquiv ∧ x.crossinglessEquiv = y.crossinglessEquiv
    source
    theorem TauCeti.PDCode.SmoothingEquiv.ext {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {x y : D.SmoothingEquiv s D' s'} (halfEdgeEquiv : x.halfEdgeEquiv = y.halfEdgeEquiv) (crossinglessEquiv : x.crossinglessEquiv = y.crossinglessEquiv) :
    x = y

    The groupoid of smoothing equivalences #

    source
    def TauCeti.PDCode.SmoothingEquiv.refl {n : ℕ} (D : PDCode n) (s : Fin n → Bool) :
    D.SmoothingEquiv s D s

    The identity smoothing equivalence.

    Instances For
      source
      @[simp]
      theorem TauCeti.PDCode.SmoothingEquiv.refl_halfEdgeEquiv {n : ℕ} (D : PDCode n) (s : Fin n → Bool) :
      (refl D s).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

      The identity smoothing equivalence is the identity on half-edges.

      source
      @[simp]
      theorem TauCeti.PDCode.SmoothingEquiv.refl_crossinglessEquiv {n : ℕ} (D : PDCode n) (s : Fin n → Bool) :
      (refl D s).crossinglessEquiv = Equiv.refl (Fin D.crossinglessComponentCount)

      The identity smoothing equivalence is the identity on crossing-free labels.

      source
      def TauCeti.PDCode.SmoothingEquiv.symm {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
      D'.SmoothingEquiv s' D s

      The inverse of a smoothing equivalence.

      Instances For
        source
        @[simp]
        theorem TauCeti.PDCode.SmoothingEquiv.symm_halfEdgeEquiv {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
        e.symm.halfEdgeEquiv = e.halfEdgeEquiv.symm

        The inverse smoothing equivalence inverts the half-edge bijection.

        source
        @[simp]
        theorem TauCeti.PDCode.SmoothingEquiv.symm_crossinglessEquiv {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
        e.symm.crossinglessEquiv = e.crossinglessEquiv.symm

        The inverse smoothing equivalence inverts the bijection of crossing-free labels.

        source
        def TauCeti.PDCode.SmoothingEquiv.trans {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') :
        D.SmoothingEquiv s D'' s''

        The composite of two smoothing equivalences.

        Instances For
          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.trans_halfEdgeEquiv {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') :
          (e.trans f).halfEdgeEquiv = e.halfEdgeEquiv.trans f.halfEdgeEquiv

          A composite smoothing equivalence composes the half-edge bijections.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.trans_crossinglessEquiv {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') :
          (e.trans f).crossinglessEquiv = e.crossinglessEquiv.trans f.crossinglessEquiv

          A composite smoothing equivalence composes the bijections of crossing-free labels.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.symm_symm {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          e.symm.symm = e

          Inverting a smoothing equivalence twice gives it back.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.refl_trans {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          (refl D s).trans e = e

          The identity is a left unit for composition.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.trans_refl {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          e.trans (refl D' s') = e

          The identity is a right unit for composition.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.self_trans_symm {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          e.trans e.symm = refl D s

          A smoothing equivalence followed by its inverse is the identity.

          source
          @[simp]
          theorem TauCeti.PDCode.SmoothingEquiv.symm_trans_self {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          e.symm.trans e = refl D' s'

          The inverse of a smoothing equivalence followed by it is the identity.

          source
          theorem TauCeti.PDCode.SmoothingEquiv.trans_assoc {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} {r' : ℕ} {D₃ : PDCode r'} {s₃ : Fin r' → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') (g : D''.SmoothingEquiv s'' D₃ s₃) :
          (e.trans f).trans g = e.trans (f.trans g)

          Composition of smoothing equivalences is associative.

          The induced bijection of circles #

          source
          theorem TauCeti.PDCode.SmoothingEquiv.edgePair_val_eq_permCongr {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          ↑D'.edgePair = e.halfEdgeEquiv.permCongr ↑D.edgePair

          A smoothing equivalence transports the native arc matching by conjugation.

          source
          theorem TauCeti.PDCode.SmoothingEquiv.statePerm_eq_permCongr {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          D'.statePerm s' = e.halfEdgeEquiv.permCongr (D.statePerm s)

          A smoothing equivalence transports the smoothed traversal.

          source
          theorem TauCeti.PDCode.SmoothingEquiv.eqvGen_circleStep_apply_iff {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') {x y : Fin (4 * n)} :
          Relation.EqvGen (D'.CircleStep s') (e.halfEdgeEquiv x) (e.halfEdgeEquiv y) ↔ Relation.EqvGen (D.CircleStep s) x y

          Two half-edges lie on one circle of the smoothed D' exactly when their preimages under a smoothing equivalence lie on one circle of the smoothed D.

          source
          def TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
          D.CrossingCircle s ≃ D'.CrossingCircle s'

          The bijection between the circles meeting a crossing induced by a smoothing equivalence: the circle through a half-edge goes to the circle through its image.

          Instances For
            source
            @[simp]
            theorem TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr_mk {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') (x : Fin (4 * n)) :
            e.crossingCircleCongr ⟦x⟧ = ⟦e.halfEdgeEquiv x⟧

            The induced bijection sends the circle through a half-edge to the circle through its image.

            source
            def TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
            D.ResolvedCircle s ≃ D'.ResolvedCircle s'

            The bijection of circles induced by a smoothing equivalence: the circle through a half-edge goes to the circle through its image, and the crossing-free circles are matched by the bijection of their labels.

            Instances For
              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_inl {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') (c : D.CrossingCircle s) :
              e.resolvedCircleCongr (Sum.inl c) = Sum.inl (e.crossingCircleCongr c)

              On the circles meeting a crossing, the induced bijection is TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_inr {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') (i : Fin D.crossinglessComponentCount) :
              e.resolvedCircleCongr (Sum.inr i) = Sum.inr (e.crossinglessEquiv i)

              On the crossing-free circles, the induced bijection is the bijection of their labels.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr_refl {n : ℕ} {D : PDCode n} {s : Fin n → Bool} :
              (refl D s).crossingCircleCongr = Equiv.refl (D.CrossingCircle s)

              The identity smoothing equivalence induces the identity on the circles meeting a crossing.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr_symm {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
              e.symm.crossingCircleCongr = e.crossingCircleCongr.symm

              The inverse smoothing equivalence induces the inverse bijection of circles meeting a crossing.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.crossingCircleCongr_trans {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') :
              (e.trans f).crossingCircleCongr = e.crossingCircleCongr.trans f.crossingCircleCongr

              A composite of smoothing equivalences induces the composite bijection of circles meeting a crossing.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_refl {n : ℕ} {D : PDCode n} {s : Fin n → Bool} :
              (refl D s).resolvedCircleCongr = Equiv.refl (D.ResolvedCircle s)

              The identity law: the identity smoothing equivalence induces the identity on circles.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_symm {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') :
              e.symm.resolvedCircleCongr = e.resolvedCircleCongr.symm

              The inverse law: the inverse smoothing equivalence induces the inverse bijection of circles.

              source
              @[simp]
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_trans {n m r : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {D'' : PDCode r} {s'' : Fin r → Bool} (e : D.SmoothingEquiv s D' s') (f : D'.SmoothingEquiv s' D'' s'') :
              (e.trans f).resolvedCircleCongr = e.resolvedCircleCongr.trans f.resolvedCircleCongr

              The composition law: a composite of smoothing equivalences induces the composite bijection of circles.

              Transport of the circles through a crossing and of saddle correspondences #

              source
              theorem TauCeti.PDCode.SmoothingEquiv.image_crossingCircleCongr_circlesAt {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') {c : Fin n} {c' : Fin m} (slots : Fin 4 ≃ Fin 4) (hcross : ∀ (k : Fin 4), e.halfEdgeEquiv (D.crossing c k) = D'.crossing c' (slots k)) :
              Finset.image (⇑e.crossingCircleCongr) (D.circlesAt s c) = D'.circlesAt s' c'

              A smoothing equivalence carrying the slots of c bijectively to those of c' carries exactly the circles through c to those through c'. The slot bijection permits a different choice of the first slot at the crossing.

              source
              theorem TauCeti.PDCode.SmoothingEquiv.card_circlesAt_eq {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} (e : D.SmoothingEquiv s D' s') {c : Fin n} {c' : Fin m} (slots : Fin 4 ≃ Fin 4) (hcross : ∀ (k : Fin 4), e.halfEdgeEquiv (D.crossing c k) = D'.crossing c' (slots k)) :
              (D.circlesAt s c).card = (D'.circlesAt s' c').card

              The number of circles through a crossing is preserved when its slots are transported bijectively by a smoothing equivalence. In particular, the merge/split conditions transport.

              source
              theorem TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_saddleResolvedCircleMap {n m : ℕ} {D : PDCode n} {s : Fin n → Bool} {D' : PDCode m} {s' : Fin m → Bool} {t : Fin n → Bool} {t' : Fin m → Bool} {c : Fin n} {c' : Fin m} (es : D.SmoothingEquiv s D' s') (et : D.SmoothingEquiv t D' t') (hhalf : es.halfEdgeEquiv = et.halfEdgeEquiv) (hisolated : es.crossinglessEquiv = et.crossinglessEquiv) (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hst' : ∀ (j : Fin m), j ≠ c' → s' j = t' j) (ht : (D.circlesAt t c).card = 1) (ht' : (D'.circlesAt t' c').card = 1) (C : D.ResolvedCircle s) :
              et.resolvedCircleCongr (D.saddleResolvedCircleMap hst ht C) = D'.saddleResolvedCircleMap hst' ht' (es.resolvedCircleCongr C)

              Saddle correspondences commute with smoothing equivalences that use the same half-edge and isolated-circle bijections at the two endpoints. Every unaffected circle is retained.

              The smoothing equivalences of the native operations #

              source
              def TauCeti.PDCode.SmoothingEquiv.relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (t : Fin m → Bool) :
              D.SmoothingEquiv (t ∘ ⇑cross) (D.relabel half cross) t

              Relabelling the half-edges along half and the crossings along cross is a smoothing equivalence from D smoothed by t ∘ cross to the relabelled code smoothed by t: the state is read at the old crossing names. The crossing-free circles keep their labels.

              Instances For
                source
                @[simp]
                theorem TauCeti.PDCode.SmoothingEquiv.relabel_halfEdgeEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (t : Fin m → Bool) :
                (relabel D half cross t).halfEdgeEquiv = half

                The relabelling smoothing equivalence is the half-edge relabelling.

                source
                @[simp]
                theorem TauCeti.PDCode.SmoothingEquiv.relabel_crossinglessEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (t : Fin m → Bool) :
                (relabel D half cross t).crossinglessEquiv = finCongr ⋯

                The relabelling smoothing equivalence keeps the labels of the crossing-free circles.

                source
                def TauCeti.PDCode.SmoothingEquiv.mirror {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (i : Fin n), t i = !s i) :
                D.SmoothingEquiv t D.mirror s

                Mirroring exchanges the A- and B-smoothings, so it is a smoothing equivalence from D smoothed by a state t to the mirror smoothed by the complementary state s, which is the identity on half-edges.

                Instances For
                  source
                  @[simp]
                  theorem TauCeti.PDCode.SmoothingEquiv.mirror_halfEdgeEquiv {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (i : Fin n), t i = !s i) :
                  (mirror D h).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                  The mirror smoothing equivalence is the identity on half-edges.

                  source
                  @[simp]
                  theorem TauCeti.PDCode.SmoothingEquiv.mirror_crossinglessEquiv {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (i : Fin n), t i = !s i) :
                  (mirror D h).crossinglessEquiv = finCongr ⋯

                  The mirror smoothing equivalence keeps the labels of the crossing-free circles.

                  source
                  def TauCeti.PDCode.SmoothingEquiv.rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) :
                  D.SmoothingEquiv s (D.rotateCrossing i) s

                  Reading a crossing from another slot does not change the smoothed diagram: it is a smoothing equivalence which is the identity on half-edges.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.PDCode.SmoothingEquiv.rotateCrossing_halfEdgeEquiv {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) :
                    (rotateCrossing D i s).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                    The rotation smoothing equivalence is the identity on half-edges.

                    source
                    @[simp]
                    theorem TauCeti.PDCode.SmoothingEquiv.rotateCrossing_crossinglessEquiv {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) :
                    (rotateCrossing D i s).crossinglessEquiv = finCongr ⋯

                    The rotation smoothing equivalence keeps the labels of the crossing-free circles.

                    source
                    def TauCeti.PDCode.SmoothingEquiv.crossinglessPerm {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                    D.SmoothingEquiv s D s

                    Permuting the labels of the crossing-free circles is a smoothing equivalence of every smoothed code to itself, which is the identity on half-edges.

                    Instances For
                      source
                      @[simp]
                      theorem TauCeti.PDCode.SmoothingEquiv.crossinglessPerm_halfEdgeEquiv {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                      (crossinglessPerm D s σ).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                      Permuting the crossing-free labels is the identity on half-edges.

                      source
                      @[simp]
                      theorem TauCeti.PDCode.SmoothingEquiv.crossinglessPerm_crossinglessEquiv {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                      (crossinglessPerm D s σ).crossinglessEquiv = σ

                      Permuting the crossing-free labels by σ acts on them by σ.

                      Transport of all smoothings at once #

                      source
                      structure TauCeti.PDCode.ResolutionEquiv {n m : ℕ} (D : PDCode n) (D' : PDCode m) :
                      Type

                      An identification of all the smoothings of D with those of D' along a bijection of crossings: a bijection of half-edges carrying the arcs of D to those of D', such that for every state t of D' it carries the traversal of D smoothed by t ∘ crossingEquiv to the traversal of D' smoothed by t, together with a bijection between the labels of the crossing-free circles. It then carries the slots of each crossing c bijectively to those of crossingEquiv c (TauCeti.PDCode.ResolutionEquiv.exists_slots). Each state gives a smoothing equivalence (TauCeti.PDCode.ResolutionEquiv.smoothingEquiv), all with the same half-edge and isolated-circle bijections, so these transports commute with every saddle of the cube of resolutions.

                      Relabelling (TauCeti.PDCode.ResolutionEquiv.relabel), reading a crossing from another slot (TauCeti.PDCode.ResolutionEquiv.rotateCrossing) and permuting the crossing-free labels (TauCeti.PDCode.ResolutionEquiv.crossinglessPerm) are such identifications. Mirroring is not: it exchanges the A- and B-smoothings.

                      Instances For
                        source
                        theorem TauCeti.PDCode.ResolutionEquiv.exists_slots {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') (c : Fin n) :
                        ∃ (slots : Fin 4 ≃ Fin 4), ∀ (k : Fin 4), E.halfEdgeEquiv (D.crossing c k) = D'.crossing (E.crossingEquiv c) (slots k)

                        The half-edge bijection carries the four half-edges of c bijectively onto those of crossingEquiv c, by a slot bijection Fin 4 ≃ Fin 4.

                        source
                        theorem TauCeti.PDCode.ResolutionEquiv.ext {n m : ℕ} {D : PDCode n} {D' : PDCode m} {E F : D.ResolutionEquiv D'} (h : E.halfEdgeEquiv = F.halfEdgeEquiv) (h' : E.crossinglessEquiv = F.crossinglessEquiv) :
                        E = F

                        Two identifications of all smoothings with the same half-edge and crossing-free bijections are equal: the crossing bijection is determined by the half-edge bijection, since crossingEquiv c is the crossing of the image of any slot of c.

                        source
                        theorem TauCeti.PDCode.ResolutionEquiv.ext_iff {n m : ℕ} {D : PDCode n} {D' : PDCode m} {E F : D.ResolutionEquiv D'} :
                        E = F ↔ E.halfEdgeEquiv = F.halfEdgeEquiv ∧ E.crossinglessEquiv = F.crossinglessEquiv
                        source
                        def TauCeti.PDCode.ResolutionEquiv.smoothingEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') {s : Fin n → Bool} {t : Fin m → Bool} (h : ∀ (i : Fin n), t (E.crossingEquiv i) = s i) :
                        D.SmoothingEquiv s D' t

                        The smoothing equivalence of an identification of all smoothings, from D smoothed by s to D' smoothed by a state t which agrees with s along the crossing bijection.

                        Instances For
                          source
                          @[simp]
                          theorem TauCeti.PDCode.ResolutionEquiv.smoothingEquiv_halfEdgeEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') {s : Fin n → Bool} {t : Fin m → Bool} (h : ∀ (i : Fin n), t (E.crossingEquiv i) = s i) :
                          (E.smoothingEquiv h).halfEdgeEquiv = E.halfEdgeEquiv

                          The smoothing equivalences of an identification of all smoothings share its half-edge bijection.

                          source
                          @[simp]
                          theorem TauCeti.PDCode.ResolutionEquiv.smoothingEquiv_crossinglessEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') {s : Fin n → Bool} {t : Fin m → Bool} (h : ∀ (i : Fin n), t (E.crossingEquiv i) = s i) :
                          (E.smoothingEquiv h).crossinglessEquiv = E.crossinglessEquiv

                          The smoothing equivalences of an identification of all smoothings share its bijection of crossing-free labels.

                          source
                          def TauCeti.PDCode.ResolutionEquiv.refl {n : ℕ} (D : PDCode n) :
                          D.ResolutionEquiv D

                          The identity identification of the smoothings of D.

                          Instances For
                            source
                            @[simp]
                            theorem TauCeti.PDCode.ResolutionEquiv.refl_crossingEquiv {n : ℕ} (D : PDCode n) :
                            (refl D).crossingEquiv = Equiv.refl (Fin n)

                            The identity identification is the identity on crossings.

                            source
                            @[simp]
                            theorem TauCeti.PDCode.ResolutionEquiv.refl_halfEdgeEquiv {n : ℕ} (D : PDCode n) :
                            (refl D).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                            The identity identification is the identity on half-edges.

                            source
                            @[simp]
                            theorem TauCeti.PDCode.ResolutionEquiv.refl_crossinglessEquiv {n : ℕ} (D : PDCode n) :
                            (refl D).crossinglessEquiv = Equiv.refl (Fin D.crossinglessComponentCount)

                            The identity identification is the identity on crossing-free labels.

                            source
                            @[simp]
                            theorem TauCeti.PDCode.ResolutionEquiv.refl_smoothingEquiv {n : ℕ} (D : PDCode n) {s : Fin n → Bool} (h : ∀ (i : Fin n), s ((refl D).crossingEquiv i) = s i) :
                            (refl D).smoothingEquiv h = SmoothingEquiv.refl D s

                            The identity identification gives the identity smoothing equivalences.

                            source
                            def TauCeti.PDCode.ResolutionEquiv.symm {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                            D'.ResolutionEquiv D

                            The inverse of an identification of all smoothings.

                            Instances For
                              source
                              @[simp]
                              theorem TauCeti.PDCode.ResolutionEquiv.symm_crossingEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                              E.symm.crossingEquiv = E.crossingEquiv.symm

                              The inverse identification inverts the crossing bijection.

                              source
                              @[simp]
                              theorem TauCeti.PDCode.ResolutionEquiv.symm_halfEdgeEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                              E.symm.halfEdgeEquiv = E.halfEdgeEquiv.symm

                              The inverse identification inverts the half-edge bijection.

                              source
                              @[simp]
                              theorem TauCeti.PDCode.ResolutionEquiv.symm_crossinglessEquiv {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                              E.symm.crossinglessEquiv = E.crossinglessEquiv.symm

                              The inverse identification inverts the bijection of crossing-free labels.

                              source
                              @[simp]
                              theorem TauCeti.PDCode.ResolutionEquiv.smoothingEquiv_symm {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') {s : Fin n → Bool} {t : Fin m → Bool} (h : ∀ (i : Fin n), t (E.crossingEquiv i) = s i) :
                              (E.smoothingEquiv h).symm = E.symm.smoothingEquiv ⋯

                              The smoothing equivalences of the inverse identification are the inverses of the smoothing equivalences.

                              source
                              def TauCeti.PDCode.ResolutionEquiv.trans {n m r : ℕ} {D : PDCode n} {D' : PDCode m} {D'' : PDCode r} (E : D.ResolutionEquiv D') (F : D'.ResolutionEquiv D'') :
                              D.ResolutionEquiv D''

                              The composite of two identifications of all smoothings.

                              Instances For
                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.trans_crossingEquiv {n m r : ℕ} {D : PDCode n} {D' : PDCode m} {D'' : PDCode r} (E : D.ResolutionEquiv D') (F : D'.ResolutionEquiv D'') :
                                (E.trans F).crossingEquiv = E.crossingEquiv.trans F.crossingEquiv

                                The crossing bijection of a composite is the composite of the crossing bijections.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.trans_halfEdgeEquiv {n m r : ℕ} {D : PDCode n} {D' : PDCode m} {D'' : PDCode r} (E : D.ResolutionEquiv D') (F : D'.ResolutionEquiv D'') :
                                (E.trans F).halfEdgeEquiv = E.halfEdgeEquiv.trans F.halfEdgeEquiv

                                The half-edge bijection of a composite is the composite of the half-edge bijections.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.trans_crossinglessEquiv {n m r : ℕ} {D : PDCode n} {D' : PDCode m} {D'' : PDCode r} (E : D.ResolutionEquiv D') (F : D'.ResolutionEquiv D'') :
                                (E.trans F).crossinglessEquiv = E.crossinglessEquiv.trans F.crossinglessEquiv

                                The bijection of crossing-free labels of a composite is the composite of these bijections.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.smoothingEquiv_trans_smoothingEquiv {n m r : ℕ} {D : PDCode n} {D' : PDCode m} {D'' : PDCode r} (E : D.ResolutionEquiv D') (F : D'.ResolutionEquiv D'') {s : Fin n → Bool} {t : Fin m → Bool} {u : Fin r → Bool} (h₁ : ∀ (i : Fin n), t (E.crossingEquiv i) = s i) (h₂ : ∀ (i : Fin m), u (F.crossingEquiv i) = t i) :
                                (E.smoothingEquiv h₁).trans (F.smoothingEquiv h₂) = (E.trans F).smoothingEquiv ⋯

                                The smoothing equivalences of a composite are the composites of the smoothing equivalences.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.symm_symm {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                                E.symm.symm = E

                                Inverting an identification of all smoothings twice gives it back.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.self_trans_symm {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                                E.trans E.symm = refl D

                                An identification of all smoothings followed by its inverse is the identity.

                                source
                                @[simp]
                                theorem TauCeti.PDCode.ResolutionEquiv.symm_trans_self {n m : ℕ} {D : PDCode n} {D' : PDCode m} (E : D.ResolutionEquiv D') :
                                E.symm.trans E = refl D'

                                The inverse of an identification of all smoothings followed by it is the identity.

                                source
                                def TauCeti.PDCode.ResolutionEquiv.ofEq {n : ℕ} {D₁ D₂ : PDCode n} (h : D₁ = D₂) :
                                D₁.ResolutionEquiv D₂

                                Equal codes have the same smoothings: the identification along an equality of codes is the identity on crossings, half-edges and crossing-free labels.

                                Instances For
                                  source
                                  @[simp]
                                  theorem TauCeti.PDCode.ResolutionEquiv.ofEq_crossingEquiv {n : ℕ} {D₁ D₂ : PDCode n} (h : D₁ = D₂) :
                                  (ofEq h).crossingEquiv = Equiv.refl (Fin n)

                                  The identification along an equality of codes is the identity on crossings.

                                  source
                                  @[simp]
                                  theorem TauCeti.PDCode.ResolutionEquiv.ofEq_halfEdgeEquiv {n : ℕ} {D₁ D₂ : PDCode n} (h : D₁ = D₂) :
                                  (ofEq h).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                                  The identification along an equality of codes is the identity on half-edges.

                                  source
                                  @[simp]
                                  theorem TauCeti.PDCode.ResolutionEquiv.ofEq_crossinglessEquiv {n : ℕ} {D₁ D₂ : PDCode n} (h : D₁ = D₂) :
                                  (ofEq h).crossinglessEquiv = finCongr ⋯

                                  The identification along an equality of codes keeps the crossing-free labels.

                                  source
                                  def TauCeti.PDCode.ResolutionEquiv.relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :
                                  D.ResolutionEquiv (D.relabel half cross)

                                  Relabelling the half-edges along half and the crossings along cross identifies the smoothings of D with those of the relabelled code. The crossing-free circles keep their labels.

                                  Instances For
                                    source
                                    @[simp]
                                    theorem TauCeti.PDCode.ResolutionEquiv.relabel_crossingEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :
                                    (relabel D half cross).crossingEquiv = cross

                                    Relabelling acts on crossings by cross.

                                    source
                                    @[simp]
                                    theorem TauCeti.PDCode.ResolutionEquiv.relabel_halfEdgeEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :
                                    (relabel D half cross).halfEdgeEquiv = half

                                    Relabelling acts on half-edges by half.

                                    source
                                    @[simp]
                                    theorem TauCeti.PDCode.ResolutionEquiv.relabel_crossinglessEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) :
                                    (relabel D half cross).crossinglessEquiv = finCongr ⋯

                                    Relabelling keeps the labels of the crossing-free circles.

                                    source
                                    @[simp]
                                    theorem TauCeti.PDCode.ResolutionEquiv.relabel_smoothingEquiv {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) (t : Fin m → Bool) (h : ∀ (i : Fin n), t ((relabel D half cross).crossingEquiv i) = (t ∘ ⇑cross) i) :
                                    (relabel D half cross).smoothingEquiv h = SmoothingEquiv.relabel D half cross t

                                    Relabelling is a smoothing equivalence of every state; it is TauCeti.PDCode.SmoothingEquiv.relabel.

                                    source
                                    def TauCeti.PDCode.ResolutionEquiv.rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) :
                                    D.ResolutionEquiv (D.rotateCrossing i)

                                    Reading a crossing from another slot keeps every smoothing: it identifies the smoothings of D with those of the rotated code, by the identity on crossings and half-edges.

                                    Instances For
                                      source
                                      @[simp]
                                      theorem TauCeti.PDCode.ResolutionEquiv.rotateCrossing_crossingEquiv {n : ℕ} (D : PDCode n) (i : Fin n) :
                                      (rotateCrossing D i).crossingEquiv = Equiv.refl (Fin n)

                                      Reading a crossing from another slot is the identity on crossings.

                                      source
                                      @[simp]
                                      theorem TauCeti.PDCode.ResolutionEquiv.rotateCrossing_halfEdgeEquiv {n : ℕ} (D : PDCode n) (i : Fin n) :
                                      (rotateCrossing D i).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                                      Reading a crossing from another slot is the identity on half-edges.

                                      source
                                      @[simp]
                                      theorem TauCeti.PDCode.ResolutionEquiv.rotateCrossing_crossinglessEquiv {n : ℕ} (D : PDCode n) (i : Fin n) :
                                      (rotateCrossing D i).crossinglessEquiv = finCongr ⋯

                                      Reading a crossing from another slot keeps the labels of the crossing-free circles.

                                      source
                                      @[simp]
                                      theorem TauCeti.PDCode.ResolutionEquiv.rotateCrossing_smoothingEquiv {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) (h : ∀ (j : Fin n), s ((rotateCrossing D i).crossingEquiv j) = s j) :
                                      (rotateCrossing D i).smoothingEquiv h = SmoothingEquiv.rotateCrossing D i s

                                      Reading a crossing from another slot is a smoothing equivalence of every state; it is TauCeti.PDCode.SmoothingEquiv.rotateCrossing.

                                      source
                                      def TauCeti.PDCode.ResolutionEquiv.crossinglessPerm {n : ℕ} (D : PDCode n) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                                      D.ResolutionEquiv D

                                      Permuting the labels of the crossing-free circles identifies the smoothings of D with themselves, by the identity on crossings and half-edges.

                                      Instances For
                                        source
                                        @[simp]
                                        theorem TauCeti.PDCode.ResolutionEquiv.crossinglessPerm_crossingEquiv {n : ℕ} (D : PDCode n) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                                        (crossinglessPerm D σ).crossingEquiv = Equiv.refl (Fin n)

                                        Permuting the crossing-free labels is the identity on crossings.

                                        source
                                        @[simp]
                                        theorem TauCeti.PDCode.ResolutionEquiv.crossinglessPerm_halfEdgeEquiv {n : ℕ} (D : PDCode n) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                                        (crossinglessPerm D σ).halfEdgeEquiv = Equiv.refl (Fin (4 * n))

                                        Permuting the crossing-free labels is the identity on half-edges.

                                        source
                                        @[simp]
                                        theorem TauCeti.PDCode.ResolutionEquiv.crossinglessPerm_crossinglessEquiv {n : ℕ} (D : PDCode n) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) :
                                        (crossinglessPerm D σ).crossinglessEquiv = σ

                                        Permuting the crossing-free labels acts on them by σ.

                                        source
                                        @[simp]
                                        theorem TauCeti.PDCode.ResolutionEquiv.crossinglessPerm_smoothingEquiv {n : ℕ} (D : PDCode n) (σ : Equiv.Perm (Fin D.crossinglessComponentCount)) (s : Fin n → Bool) (h : ∀ (i : Fin n), s ((crossinglessPerm D σ).crossingEquiv i) = s i) :
                                        (crossinglessPerm D σ).smoothingEquiv h = SmoothingEquiv.crossinglessPerm D s σ

                                        Permuting the crossing-free labels is a smoothing equivalence of every state; it is TauCeti.PDCode.SmoothingEquiv.crossinglessPerm.

                                        The circles of a disjoint union #

                                        source
                                        theorem TauCeti.PDCode.eqvGen_circleStep_disjointUnion_iff {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) {x y : Fin (4 * n) ⊕ Fin (4 * m)} :
                                        Relation.EqvGen ((D.disjointUnion E).CircleStep s) ((disjointUnionHalfEdgeEquiv n m) x) ((disjointUnionHalfEdgeEquiv n m) y) ↔ Sum.LiftRel (Relation.EqvGen (D.CircleStep (s ∘ Fin.castAdd m))) (Relation.EqvGen (E.CircleStep (s ∘ Fin.natAdd n))) x y

                                        Two half-edges of a disjoint union lie on one circle exactly when they come from the same summand and lie on one circle of that summand, smoothed by the restricted state.

                                        source
                                        def TauCeti.PDCode.disjointUnionCrossingCircleEquiv {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) :
                                        (D.disjointUnion E).CrossingCircle s ≃ D.CrossingCircle (s ∘ Fin.castAdd m) ⊕ E.CrossingCircle (s ∘ Fin.natAdd n)

                                        The circles meeting a crossing of a smoothed disjoint union are those of the two summands, smoothed by the two restrictions of the state.

                                        Instances For
                                          source
                                          @[simp]
                                          theorem TauCeti.PDCode.disjointUnionCrossingCircleEquiv_mk_inl {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (x : Fin (4 * n)) :
                                          (D.disjointUnionCrossingCircleEquiv E s) ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inl x)⟧ = Sum.inl ⟦x⟧

                                          A circle through a half-edge of the first summand is a circle of the first summand.

                                          source
                                          @[simp]
                                          theorem TauCeti.PDCode.disjointUnionCrossingCircleEquiv_mk_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (y : Fin (4 * m)) :
                                          (D.disjointUnionCrossingCircleEquiv E s) ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inr y)⟧ = Sum.inr ⟦y⟧

                                          A circle through a half-edge of the second summand is a circle of the second summand.

                                          source
                                          def TauCeti.PDCode.disjointUnionResolvedCircleEquiv {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) :
                                          (D.disjointUnion E).ResolvedCircle s ≃ D.ResolvedCircle (s ∘ Fin.castAdd m) ⊕ E.ResolvedCircle (s ∘ Fin.natAdd n)

                                          The circles of a smoothed disjoint union are the circles of the two summands, smoothed by the two restrictions of the state. The circle through a half-edge of a summand is the circle through it in that summand, and the crossing-free circles of the first summand are numbered before those of the second.

                                          Instances For
                                            source
                                            @[simp]
                                            theorem TauCeti.PDCode.disjointUnionResolvedCircleEquiv_inl_mk_inl {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (x : Fin (4 * n)) :
                                            (D.disjointUnionResolvedCircleEquiv E s) (Sum.inl ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inl x)⟧) = Sum.inl (Sum.inl ⟦x⟧)

                                            The circle through a half-edge of the first summand is the circle through it in the first summand.

                                            source
                                            @[simp]
                                            theorem TauCeti.PDCode.disjointUnionResolvedCircleEquiv_inl_mk_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (y : Fin (4 * m)) :
                                            (D.disjointUnionResolvedCircleEquiv E s) (Sum.inl ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inr y)⟧) = Sum.inr (Sum.inl ⟦y⟧)

                                            The circle through a half-edge of the second summand is the circle through it in the second summand.

                                            source
                                            @[simp]
                                            theorem TauCeti.PDCode.disjointUnionResolvedCircleEquiv_symm_inl_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (i : Fin D.crossinglessComponentCount) :
                                            (D.disjointUnionResolvedCircleEquiv E s).symm (Sum.inl (Sum.inr i)) = Sum.inr ((finCongr ⋯) (Fin.castAdd E.crossinglessComponentCount i))

                                            The crossing-free circles of the first summand are numbered first in the disjoint union.

                                            source
                                            @[simp]
                                            theorem TauCeti.PDCode.disjointUnionResolvedCircleEquiv_symm_inr_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (s : Fin (n + m) → Bool) (j : Fin E.crossinglessComponentCount) :
                                            (D.disjointUnionResolvedCircleEquiv E s).symm (Sum.inr (Sum.inr j)) = Sum.inr ((finCongr ⋯) (Fin.natAdd D.crossinglessComponentCount j))

                                            The crossing-free circles of the second summand are numbered after those of the first in the disjoint union.