isLeftKanExtension_iff_precomp — Mathlib

English

ALeftKanExtension α along L is equivalent to aLeftKanExtension along G with adjusted whiskering and associator factors.

Русский

Левое Кан-расширение α вдоль L эквивалентно левому Кан-расширению вдоль G с учётом поправок whisker и associator.

LaTeX

$$isLeftKanExtension_iff_precomp$$

Lean4

theorem isLeftKanExtension_iff_precomp (α : F ⟶ L ⋙ F') :
    F'.IsLeftKanExtension α ↔ F'.IsLeftKanExtension (whiskerLeft G α ≫ (associator _ _ _).inv) :=
  by
  let eq :
    (LeftExtension.mk _ α).IsUniversal ≃ (LeftExtension.mk _ (whiskerLeft G α ≫ (associator _ _ _).inv)).IsUniversal :=
    (LeftExtension.isUniversalPrecompEquiv L F G _).trans (IsInitial.equivOfIso (StructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsLeftKanExtension _ _)⟩⟩

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