of_lanLift_comp_iso — Mathlib

English

If there is an isomorphism i between the whiskered Lan along g and the whiskered Lan along h, then Lan.CommuteWith f g h holds under that isomorphism.

Русский

Если существует изоморфизм i между (t.whisker h) и (lanLeftExtension f g).whisker h, то при этом выполняется Lan.CommuteWith f g h.

LaTeX

$$$\forall i:\ t.whisker h \cong (\mathrm{lanLeftExtension}\ f\ g).\mathrm{whisker}\ h \;\Rightarrow\; \mathrm{Lan.CommuteWith}(f,g,h).$$$

Lean4

theorem of_lanLift_comp_iso [HasLeftKanLift f g] {x : B} {h : x ⟶ c} [HasLeftKanLift f (h ≫ g)]
    (i : f₊ (h ≫ g) ≅ h ≫ f₊ g) (w : lanLiftUnit f (h ≫ g) ≫ i.hom ▷ f = h ◁ lanLiftUnit f g ≫ (α_ _ _ _).inv) :
    LanLift.CommuteWith f g h :=
  ⟨⟨(lanLiftIsKan f (h ≫ g)).ofIsoKan <| StructuredArrow.isoMk i⟩⟩

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