isUniversalPostcomp₁Equiv — Mathlib

English

There is a natural equivalence between universality of a left extension ex and the universality of its postcomposition ex.postcomp₁ along G with e.inv.

Русский

Существует естественная эквивалентность между универсальностью левого расширения ex и универсальностью полученного после посткомпозиции ex.postcomp₁ вдоль G с e.inv.

LaTeX

$$$ex.IsUniversal \simeq ((LeftExtension.postcomp₁ G e.inv F).obj ex).IsUniversal$$$

Lean4

/-- Given an isomorphism `e : L ⋙ G ≅ L'`, a left extension of `F` along `L'` is universal
iff the corresponding left extension of `L` along `L` is. -/
noncomputable def isUniversalPostcomp₁Equiv (ex : LeftExtension L' F) :
    ex.IsUniversal ≃ ((LeftExtension.postcomp₁ G e.inv F).obj ex).IsUniversal := by
  apply IsInitial.isInitialIffObj (LeftExtension.postcomp₁ G e.inv F)

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