English
For kernels κ and η, composing η with Kernel.id on either side via parallel composition commutes: (id ∥ₖ κ) ∘ₖ (η ∥ₖ Kernel.id) = (η ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ).
Русский
Для ядер κ и η композиция η с Kernel.id по обеим сторонам через параллельную композицию коммутирует: (id ∥ₖ κ) ∘ₖ (η ∥ₖ Kernel.id) = (η ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ).
LaTeX
$$$$(\\text{Kernel.id} \\parallel_k \\kappa) \\circ_k (\\eta \\parallel_k \\text{Kernel.id}) = (\\eta \\parallel_k \\text{Kernel.id}) \\circ_k (\\text{Kernel.id} \\parallel_k \\kappa).$$$$
Lean4
theorem parallelComp_comm {η : Kernel Z T} :
(Kernel.id ∥ₖ κ) ∘ₖ (η ∥ₖ Kernel.id) = (η ∥ₖ Kernel.id) ∘ₖ (Kernel.id ∥ₖ κ) :=
by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
by_cases hη : IsSFiniteKernel η
swap; · simp [hη]
rw [parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp, comp_id, comp_id]
