rightDistributor_ext₂_left — Mathlib

English

In a monoidal category with right duals, the right adjoint mate of the identity morphism is the identity on the right dual: (id X)ᘁ = id (Xᘁ).

Русский

В моноидальной категории с правыми двойниками правая сопряженная композиция (mate) единичного морфизма равна единичному морфизму на правом двойнике: (id X)ᘁ = id(Xᘁ).

LaTeX

$$$$ (\\mathrm{Id}_X)^{\\flat} = \\mathrm{Id}_{X^{\\vee}} $$$$

Lean4

@[ext]
theorem rightDistributor_ext₂_left {J : Type} [Finite J] {f : J → C} {X Y Z : C} {g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z}
    (w : ∀ j, ((biproduct.ι f j ▷ X) ▷ Y) ≫ g = ((biproduct.ι f j ▷ X) ▷ Y) ≫ h) : g = h :=
  by
  apply (cancel_epi (α_ _ _ _).inv).mp
  ext
  simp [w]

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