leftAdjointMate_comp — Mathlib

English

The mate of a composition is the composition of mates in the reverse order: rightAdjointMate(f ∘ g) = rightAdjointMate(g) ∘ rightAdjointMate(f).

Русский

Сопряженная композиция отображений равна композиции их сопряжений в противоположном порядке: rightAdjointMate(f ∘ g) = rightAdjointMate(g) ∘ rightAdjointMate(f).

LaTeX

$$$$ (f g)^{\\ast} = g^{\\ast} f^{\\ast} $$$$

Lean4

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

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