of_lan_comp_iso — Mathlib

English

If f,g have HasLeftKanLift, and h: x ⟶ c, then HasLeftKanLift f (h ≫ g).

Русский

Если f,g имеют HasLeftKanLift, и h: x ⟶ c, тогда HasLeftKanLift f (h ≫ g).

LaTeX

$$$[HasLeftKanLift f g] \Rightarrow [HasLeftKanLift f (h \gg g)].$$$

Lean4

theorem of_lan_comp_iso [HasLeftKanExtension f g] {x : B} {h : c ⟶ x} [HasLeftKanExtension f (g ≫ h)]
    (i : f⁺ (g ≫ h) ≅ f⁺ g ≫ h) (w : lanUnit f (g ≫ h) ≫ f ◁ i.hom = lanUnit f g ▷ h ≫ (α_ _ _ _).hom) :
    Lan.CommuteWith f g h :=
  ⟨⟨(lanIsKan f (g ≫ h)).ofIsoKan <| StructuredArrow.isoMk i⟩⟩

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