Isomorphism theory of fragments

An equivalence of fragments Fragment.Equiv W₁ W₂ (defined in RS/Definitions.lean) is a pair of type equivalences on flags and vertices commuting with attachment, pairing, and boundary-flag data, preserving the circle count. This module proves the equivalences form a groupoid (refl, symm, trans) and are congruences for the fragment operations: relabelling, disjoint union, and single-pair gluing.

theorem RS.Fragment.Equiv.boundaryFlag_comm {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (ℓ : α) : e.flagEquiv (W₁.boundaryFlag ℓ) = W₂.boundaryFlag ℓ

The flag equivalence sends boundary flags to boundary flags.

def RS.Fragment.Equiv.refl {α : Type} (W : Fragment α) : W.Equiv W

The identity equivalence.

Equations

• RS.Fragment.Equiv.refl W = { flagEquiv := Equiv.refl W.Flag, vertexEquiv := Equiv.refl W.Vertex, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

def RS.Fragment.Equiv.symm {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) : W₂.Equiv W₁

The inverse equivalence.

Equations

• e.symm = { flagEquiv := e.flagEquiv.symm, vertexEquiv := e.vertexEquiv.symm, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

def RS.Fragment.Equiv.trans {α : Type} {W₁ W₂ W₃ : Fragment α} (e₁ : W₁.Equiv W₂) (e₂ : W₂.Equiv W₃) : W₁.Equiv W₃

The composite equivalence.

Equations

• e₁.trans e₂ = { flagEquiv := e₁.flagEquiv.trans e₂.flagEquiv, vertexEquiv := e₁.vertexEquiv.trans e₂.vertexEquiv, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

Congruences

def RS.Fragment.Equiv.relabelCongr {α β : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (σ : α ≃ β) : (W₁.relabel σ).Equiv (W₂.relabel σ)

Relabelling commutes with fragment equivalence.

Equations

• e.relabelCongr σ = { flagEquiv := e.flagEquiv, vertexEquiv := e.vertexEquiv, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

def RS.Fragment.Equiv.disjUnionCongr {α β : Type} {W₁ W₂ : Fragment α} {V₁ V₂ : Fragment β} (e₁ : W₁.Equiv W₂) (e₂ : V₁.Equiv V₂) : (W₁.disjUnion V₁).Equiv (W₂.disjUnion V₂)

Disjoint union commutes with fragment equivalence.

Equations

• e₁.disjUnionCongr e₂ = { flagEquiv := e₁.flagEquiv.sumCongr e₂.flagEquiv, vertexEquiv := e₁.vertexEquiv.sumCongr e₂.vertexEquiv, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

Glue-pair congruence

def RS.Fragment.Equiv.survivingFlagEquiv {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (i j : α) : W₁.SurvivingFlag i j ≃ W₂.SurvivingFlag i j

The flag equivalence restricts to surviving flags.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Fragment.Equiv.gluePair_case_preserved {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (i j : α) : W₁.pairing (W₁.boundaryFlag i) = W₁.boundaryFlag j ↔ W₂.pairing (W₂.boundaryFlag i) = W₂.boundaryFlag j

The glue case (closed vs open) is preserved by the equivalence.

def RS.Fragment.Equiv.gluePairClosedCongr {α : Type} {W₁ W₂ : Fragment α} {i j : α} (e : W₁.Equiv W₂) (h₁ : W₁.pairing (W₁.boundaryFlag i) = W₁.boundaryFlag j) (h₂ : W₂.pairing (W₂.boundaryFlag i) = W₂.boundaryFlag j) : (W₁.gluePairClosed i j h₁).Equiv (W₂.gluePairClosed i j h₂)

The closed case: the flag equivalence restricts to a gluePairClosed congruence.

Equations

• e.gluePairClosedCongr h₁ h₂ = { flagEquiv := e.survivingFlagEquiv i j, vertexEquiv := e.vertexEquiv, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

Rewire commutation

def RS.Fragment.Equiv.gluePairOpenCongr {α : Type} {W₁ W₂ : Fragment α} {i j : α} (e : W₁.Equiv W₂) (hopen₁ : W₁.pairing (W₁.boundaryFlag i) ≠ W₁.boundaryFlag j) (hopen₂ : W₂.pairing (W₂.boundaryFlag i) ≠ W₂.boundaryFlag j) (hij : i ≠ j) : (W₁.gluePairOpen i j hij hopen₁).Equiv (W₂.gluePairOpen i j hij hopen₂)

The open case: the flag equivalence restricts to a gluePairOpen congruence.

Equations

• e.gluePairOpenCongr hopen₁ hopen₂ hij = { flagEquiv := e.survivingFlagEquiv i j, vertexEquiv := e.vertexEquiv, attach_comm := ⋯, pairing_comm := ⋯, circles_eq := ⋯ }

def RS.Fragment.Equiv.gluePairCongr {α : Type} {W₁ W₂ : Fragment α} {i j : α} (e : W₁.Equiv W₂) (hij : i ≠ j) : (W₁.gluePair i j hij).Equiv (W₂.gluePair i j hij)

Single-pair gluing commutes with fragment equivalence.

Equations

• e.gluePairCongr hij = id (if h : W₁.pairing (W₁.boundaryFlag i) = W₁.boundaryFlag j then ⋯.mpr (⋯.mpr (e.gluePairClosedCongr h ⋯)) else ⋯.mpr (⋯.mpr (e.gluePairOpenCongr h ⋯ hij)))

Relabel algebra

def RS.Fragment.Equiv.relabelRefl {α : Type} (W : Fragment α) : (W.relabel (_root_.Equiv.refl α)).Equiv W

Relabelling by the identity is the identity on fragments, up to equivalence.

Equations

• One or more equations did not get rendered due to their size.

def RS.Fragment.Equiv.relabelTrans {α β : Type} (W : Fragment α) (e₁ : α ≃ β) {γ : Type} (e₂ : β ≃ γ) : ((W.relabel e₁).relabel e₂).Equiv (W.relabel (e₁.trans e₂))

Relabelling twice composes, up to equivalence.

Equations

• One or more equations did not get rendered due to their size.

Sanity checks