isRightKanExtension_iff_precomp — Mathlib

English

A RightKanExtension α along L' is equivalent to a RightKanExtension along G with adjusted associator factors.

Русский

Правое Кан-расширение α вдоль L' эквивалентно правому Кан-расширению вдоль G с поправкой на associator.

LaTeX

$$isRightKanExtension_iff_precomp$$

Lean4

theorem isRightKanExtension_iff_precomp (α : L ⋙ F' ⟶ F) :
    F'.IsRightKanExtension α ↔ F'.IsRightKanExtension ((associator _ _ _).hom ≫ whiskerLeft G α) :=
  by
  let eq :
    (RightExtension.mk _ α).IsUniversal ≃
      (RightExtension.mk _ ((associator _ _ _).hom ≫ whiskerLeft G α)).IsUniversal :=
    (RightExtension.isUniversalPrecompEquiv L F G _).trans
      (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

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