Documentation

TauCeti.KnotTheory.PDCode.Oriented.DisjointUnion

Disjoint unions of oriented diagrams #

Disjoint union retains each component's direction, including the directions on crossing-free circles. Crossing signs are unchanged, and writhe is additive. Consequently the writhe-normalized Kauffman bracket has the same disjoint-union formula as the unoriented bracket. This is the formula used to transport an invariant local replacement of an isolated diagram into an arbitrary surrounding diagram.

References #

source
def TauCeti.OrientedPDCode.disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
OrientedPDCode (n + m)

Disjoint union retains the direction of each component of the two diagrams.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.OrientedPDCode.toPDCode_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
    (D.disjointUnion E).toPDCode = D.disjointUnion E.toPDCode

    Forgetting orientations commutes with disjoint union.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_disjointUnion_inl {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) (x : Fin (4 * n)) :
    (D.disjointUnion E).orientation ((PDCode.disjointUnionHalfEdgeEquiv n m) (Sum.inl x)) = D.orientation x

    The first diagram's half-edges retain their directions.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.orientation_disjointUnion_inr {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) (x : Fin (4 * m)) :
    (D.disjointUnion E).orientation ((PDCode.disjointUnionHalfEdgeEquiv n m) (Sum.inr x)) = E.orientation x

    The second diagram's half-edges retain their directions.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossinglessComponents_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
    (D.disjointUnion E).crossinglessComponents = D.crossinglessComponents + E.crossinglessComponents

    The crossing-free circles and their directions are concatenated as multisets.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.mirror_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
    (D.disjointUnion E).mirror = D.mirror.disjointUnion E.mirror

    Reflection commutes with oriented disjoint union.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.reverse_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
    (D.disjointUnion E).reverse = D.reverse.disjointUnion E.reverse

    Reversing every component commutes with disjoint union.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_disjointUnion_castAdd {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) (i : Fin n) :
    (D.disjointUnion E).crossingSign (Fin.castAdd m i) = D.crossingSign i

    Every crossing of the first diagram retains its sign.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.crossingSign_disjointUnion_natAdd {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) (i : Fin m) :
    (D.disjointUnion E).crossingSign (Fin.natAdd n i) = E.crossingSign i

    Every crossing of the second diagram retains its sign.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.writhe_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) :
    (D.disjointUnion E).writhe = D.writhe + E.writhe

    Writhe is additive under disjoint union.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_disjointUnion {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hD : 0 < D.componentCount) (hE : 0 < E.componentCount) :
    (D.disjointUnion E).normalizedKauffmanBracket a = TemperleyLieb.jonesDelta a * D.normalizedKauffmanBracket a * E.normalizedKauffmanBracket a

    The normalized bracket of two nonempty disjoint diagrams is the product of their normalized brackets times the circle value.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_disjointUnion_of_componentCount_eq_zero_left {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hD : D.componentCount = 0) :
    (D.disjointUnion E).normalizedKauffmanBracket a = E.normalizedKauffmanBracket a

    An empty first summand leaves the other diagram's normalized bracket unchanged.

    source
    @[simp]
    theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_disjointUnion_of_componentCount_eq_zero_right {n m : ℕ} (D : OrientedPDCode n) (E : OrientedPDCode m) {R : Type u_1} [CommRing R] (a : Rˣ) (hE : E.componentCount = 0) :
    (D.disjointUnion E).normalizedKauffmanBracket a = D.normalizedKauffmanBracket a

    An empty second summand leaves the other diagram's normalized bracket unchanged.