Documentation

TauCeti.KnotTheory.PDCode.DisjointUnion.Planar

Planarity of disjoint unions of PD-codes #

Placing diagrams in disjoint discs preserves planarity, and a disjoint union is planar only if both summands are planar. This lets a planar local replacement on isolated components be used inside an arbitrary planar surrounding diagram.

The crossing rotation and face traversal act separately on the two blocks of half-edges. The graph components correspond to the disjoint union of the summands' graph components; this is proved on monodromy orbits, without identifying the monodromy group with a product (it may be a proper subdirect product). Face counts are additive, and the Euler bound for each summand gives the converse of planarity preservation. Crossing-free circles contribute neither graph components nor faces, so the results include diagrams without crossings.

References #

source
@[simp]
theorem TauCeti.PDCode.crossingRotation_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) :
(D.disjointUnion E).crossingRotation = (disjointUnionHalfEdgeEquiv n m).permCongr (D.crossingRotation.sumCongr E.crossingRotation)

The crossing rotation acts independently on the two summands.

source
@[simp]
theorem TauCeti.PDCode.facePerm_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) :
(D.disjointUnion E).facePerm = (disjointUnionHalfEdgeEquiv n m).permCongr (D.facePerm.sumCongr E.facePerm)

Face traversal stays within each summand and follows its original face traversal.

source
@[simp]
theorem TauCeti.PDCode.faceCount_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) :
(D.disjointUnion E).faceCount = D.faceCount + E.faceCount

The faces of disjoint diagrams are counted independently.

source
def TauCeti.PDCode.disjointUnionMonodromyOrbitEquiv {n m : ℕ} (D : PDCode n) (E : PDCode m) :
(D.disjointUnion E).toPermutationTriple.MonodromyOrbit ≃ D.toPermutationTriple.MonodromyOrbit ⊕ E.toPermutationTriple.MonodromyOrbit

The graph components of a disjoint union are exactly the components of its two summands. This correspondence includes empty blocks of half-edges.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.PDCode.disjointUnionMonodromyOrbitEquiv_inl {n m : ℕ} (D : PDCode n) (E : PDCode m) (x : Fin (4 * n)) :
    (D.disjointUnionMonodromyOrbitEquiv E) ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inl x)⟧ = Sum.inl ⟦x⟧

    A representative in the first block maps to its original graph component.

    source
    @[simp]
    theorem TauCeti.PDCode.disjointUnionMonodromyOrbitEquiv_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (x : Fin (4 * m)) :
    (D.disjointUnionMonodromyOrbitEquiv E) ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inr x)⟧ = Sum.inr ⟦x⟧

    A representative in the second block maps to its original graph component.

    source
    @[simp]
    theorem TauCeti.PDCode.disjointUnionMonodromyOrbitEquiv_symm_inl {n m : ℕ} (D : PDCode n) (E : PDCode m) (x : Fin (4 * n)) :
    (D.disjointUnionMonodromyOrbitEquiv E).symm (Sum.inl ⟦x⟧) = ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inl x)⟧

    The inverse component correspondence includes the first block's representative.

    source
    @[simp]
    theorem TauCeti.PDCode.disjointUnionMonodromyOrbitEquiv_symm_inr {n m : ℕ} (D : PDCode n) (E : PDCode m) (x : Fin (4 * m)) :
    (D.disjointUnionMonodromyOrbitEquiv E).symm (Sum.inr ⟦x⟧) = ⟦(disjointUnionHalfEdgeEquiv n m) (Sum.inr x)⟧

    The inverse component correspondence includes the second block's representative.

    source
    @[simp]
    theorem TauCeti.PDCode.card_monodromyOrbit_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) :
    Nat.card (D.disjointUnion E).toPermutationTriple.MonodromyOrbit = Nat.card D.toPermutationTriple.MonodromyOrbit + Nat.card E.toPermutationTriple.MonodromyOrbit

    The number of graph components is additive under disjoint union.

    source
    @[simp]
    theorem TauCeti.PDCode.isPlanar_disjointUnion {n m : ℕ} (D : PDCode n) (E : PDCode m) :
    (D.disjointUnion E).IsPlanar ↔ D.IsPlanar ∧ E.IsPlanar

    A disjoint union is planar exactly when both summands are planar. The converse uses the Euler bound separately on each summand, so a deficit of faces cannot cancel.