parallelComp_id_right_comp_parallelComp

English

ParallelComp interacts with comp in a Law-like equality: parallelComp_prodMkLeft = comp with left/right prod.

Русский

Параллельная композиция ведёт себя как законоподобное равенство с левой и правой проделкой.

LaTeX

$$$$ κ ⊗ₖ (prodMkLeft X η) = (id × η) ∘ κ $$$$

Lean4

theorem parallelComp_id_right_comp_parallelComp {η : Kernel X' Z} [IsSFiniteKernel η] {ξ : Kernel Z T}
    [IsSFiniteKernel ξ] : (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = (ξ ∘ₖ η) ∥ₖ κ :=
  by
  suffices swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ) = swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ) by
    calc
      ξ ∥ₖ Kernel.id ∘ₖ (η ∥ₖ κ)
      _ = swap Y T ∘ₖ (swap T Y ∘ₖ (ξ ∥ₖ Kernel.id) ∘ₖ (η ∥ₖ κ)) := by simp_rw [← comp_assoc, swap_swap, id_comp]
      _ = swap Y T ∘ₖ (swap T Y ∘ₖ ((ξ ∘ₖ η) ∥ₖ κ)) := by rw [this]
      _ = ξ ∘ₖ η ∥ₖ κ := by simp_rw [← comp_assoc, swap_swap, id_comp]
  simp_rw [swap_parallelComp, comp_assoc, swap_parallelComp, ← comp_assoc, parallelComp_id_left_comp_parallelComp]

Похожие утверждения