Eulerian edge subsets and circuit data

The combinatorial substrate of the mixed partition function — edge subsets, vertex degrees, the Eulerian condition, transition systems and the circuit count — is defined in RS/Definitions.lean. This module carries its transport theory: edge subsets, the Eulerian condition, transition systems and the circuit count all transport along fragment equivalences.

theorem RS.EdgeSubset.ext {α : Type} {W : Fragment α} {F₁ F₂ : EdgeSubset W} (h : F₁.flags = F₂.flags) : F₁ = F₂

Edge subsets are determined by their flag sets.

theorem RS.EdgeSubset.ext_iff {α : Type} {W : Fragment α} {F₁ F₂ : EdgeSubset W} : F₁ = F₂ ↔ F₁.flags = F₂.flags

noncomputable def RS.EdgeSubset.transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) : EdgeSubset W₁ ≃ EdgeSubset W₂

Transport of edge subsets along a fragment equivalence.

Equations

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

theorem RS.EdgeSubset.transport_deg {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) (v : W₁.Vertex) : ((transport e) F).deg (e.vertexEquiv v) = F.deg v

Transport preserves degrees at transported vertices.

theorem RS.EdgeSubset.transport_eulerian {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) : ((transport e) F).Eulerian ↔ F.Eulerian

Transport preserves the Eulerian condition.

theorem RS.EdgeSubset.mem_transport_iff {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) (f : W₂.Flag) : f ∈ ((transport e) F).flags ↔ e.flagEquiv.symm f ∈ F.flags

Membership in a transported edge subset.

theorem RS.EdgeSubset.transport_symm_transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) : (transport e.symm) ((transport e) F) = F

Transporting there and back along an equivalence is the identity on edge subsets.

noncomputable def RS.EdgeSubset.TransitionSystem.transport {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} (κ : F.TransitionSystem) : ((EdgeSubset.transport e) F).TransitionSystem

Transport of a transition system along a fragment equivalence: the conjugated matching.

Equations

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

noncomputable def RS.EdgeSubset.transportFlagsEquiv {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) (F : EdgeSubset W₁) : ↥F.flags ≃ ↥((transport e) F).flags

The flag equivalence restricted to a transported edge subset.

Equations

• RS.EdgeSubset.transportFlagsEquiv e F = e.flagEquiv.subtypeEquiv ⋯

theorem RS.EdgeSubset.TransitionSystem.transport_walkPerm {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} (κ : F.TransitionSystem) : (transport e κ).walkPerm = (transportFlagsEquiv e F).permCongr κ.walkPerm

The transported walk permutation is the transported walk.

theorem RS.EdgeSubset.TransitionSystem.transport_circuitCount {α : Type} {W₁ W₂ : Fragment α} (e : W₁.Equiv W₂) {F : EdgeSubset W₁} (κ : F.TransitionSystem) : (transport e κ).circuitCount = κ.circuitCount

Transport preserves the circuit count.

theorem RS.perm_pmap {β : Type u_1} {γ : Type u_2} {p : β → Prop} (f : (b : β) → p b → γ) {l₁ l₂ : List β} (hp : l₁.Perm l₂) (H₁ : ∀ b ∈ l₁, p b) (H₂ : ∀ b ∈ l₂, p b) : (List.pmap f l₁ H₁).Perm (List.pmap f l₂ H₂)

pmap respects permutations of the underlying list.

theorem RS.pmap_flatMap_congr {β : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {γ : Type u_4} {p₁ p₂ : β → Prop} (f₁ : (b : β) → p₁ b → β₁) (f₂ : (b : β) → p₂ b → β₂) (G₁ : β₁ → List γ) (G₂ : β₂ → List γ) (l : List β) (H₁ : ∀ b ∈ l, p₁ b) (H₂ : ∀ b ∈ l, p₂ b) (hpt : ∀ b ∈ l, ∀ (h₁ : p₁ b) (h₂ : p₂ b), G₁ (f₁ b h₁) = G₂ (f₂ b h₂)) : List.flatMap G₁ (List.pmap f₁ l H₁) = List.flatMap G₂ (List.pmap f₂ l H₂)

Congruent proof-carrying maps followed by list-valued functions give equal flattenings.