English
Analogous to the left case: α : L' ⋯ F' ⟶ F gives F' isRightKanExtension α iff (G ⋙ F') isRightKanExtension ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α).
Русский
Аналогично левому случаю: α : L' ⋯ F' ⟶ F даёт F'RightKanExtension α тогда и только тогда, когда (G ⋙ F') является правым Кан-расширением ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α).
LaTeX
$$$F'.IsRightKanExtension α \iff (G ⋙ F').IsRightKanExtension ((associator _ _ _).inv \gg whiskerRight e.hom F' \gg α)$$$
Lean4
theorem isRightKanExtension_iff_postcomp₁ (α : L' ⋙ F' ⟶ F) :
F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α) :=
by
let eq :
(RightExtension.mk _ α).IsUniversal ≃
(RightExtension.mk _ ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
(RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
(IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
constructor
· exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
· exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩
