English
For hα: (LeftExtension.mk F1 α).IsUniversal and b : L'.LeftExtension F1, there is an equivalence between the universality of b and the universality of its precomp₂ image: b.IsUniversal ≃ ((LeftExtension.precomp₂ L' α).obj b).IsUniversal.
Русский
Для hα: (LeftExtension.mk F1 α).IsUniversal и b : L'.LeftExtension F1 существует эквивалентность между универсальностью b и универсальностью его образа под precomp₂: b.IsUniversal ≃ ((LeftExtension.precomp₂ L' α).obj b).IsUniversal.
LaTeX
$$$b.IsUniversal \\simeq ((\\text{LeftExtension.precomp₂ } L' \\alpha).\\text{obj } b).IsUniversal$$$
Lean4
/-- If the left extension defined by `α : F₀ ⟶ L ⋙ F₁` is universal,
then for every `L' : D ⥤ D'`, `F₁ : D ⥤ H`, an extension
`b : L'.LeftExtension F₁` is universal if and only if
`(LeftExtension.precomp₂ L' α).obj b` is universal. -/
def isUniversalPrecomp₂Equiv (hα : (LeftExtension.mk F₁ α).IsUniversal) (b : L'.LeftExtension F₁) :
b.IsUniversal ≃ ((LeftExtension.precomp₂ L' α).obj b).IsUniversal
where
toFun h := LeftExtension.isUniversalPrecomp₂ α hα h
invFun h := LeftExtension.isUniversalOfPrecomp₂ α hα h
left_inv x := by subsingleton
right_inv x := by subsingleton
