instCommuteWithOfIsLeftAdjoint — Mathlib

English

If f,g have a left Kan extension and h is left adjoint, then Lan.CommuteWith f g h holds.

Русский

Если f,g имеют левое Кан-расширение, а h — левый сопряжённый, то выполняется условие Lan.CommuteWith f g h.

LaTeX

$$$[IsLeftAdjoint(h)] \land [HasLeftKanExtension(f,g)] \Rightarrow \mathrm{Lan.CommuteWith}(f,g,h).$$$

Lean4

instance {f : a ⟶ b} {g : a ⟶ c} {x : B} {h : c ⟶ x} [IsLeftAdjoint h] [HasLeftKanExtension f g] :
    Lan.CommuteWith f g h :=
  ⟨⟨isKanOfWhiskerLeftAdjoint (lanIsKan f g) (Adjunction.ofIsLeftAdjoint h)⟩⟩

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