rightAdjointMate_comp — Mathlib

English

Naturality of the right distributor with respect to postcomposition on the target: the mate respects composition on the right.

Русский

Единство правого распределителя по отношению к постсоставлению на мишени: мача сохраняет композицию справа.

LaTeX

$$$$ (tensorRightHomEquiv X Y Y' Z).symm \\circ (f \\circ g) = (tensorRightHomEquiv X Y Y' Z).symm f \\circ g $$$$

Lean4

theorem rightAdjointMate_comp {X Y Z : C} [HasRightDual X] [HasRightDual Y] {f : X ⟶ Y} {g : Xᘁ ⟶ Z} :
    fᘁ ≫ g = (ρ_ (Yᘁ)).inv ≫ _ ◁ η_ X (Xᘁ) ≫ _ ◁ (f ⊗ₘ g) ≫ (α_ (Yᘁ) Y Z).inv ≫ ε_ Y (Yᘁ) ▷ _ ≫ (λ_ Z).hom :=
  calc
    _ = 𝟙 _ ⊗≫ (Yᘁ : C) ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 _ := by dsimp only [rightAdjointMate];
      monoidal
    _ = _ := by rw [← whisker_exchange, tensorHom_def]; monoidal

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