isUniversalPrecompEquiv — Mathlib

English

There is an equivalence between universality of a right extension and the universality of its precomposition with G.

Русский

Существует эквивалентность универсальности правого расширения и его предрасширения с G.

LaTeX

$$ex.IsUniversal ≃ ((RightExtension.precomp L F G).obj ex).IsUniversal$$

Lean4

/-- If `G` is an equivalence, then a right extension of `F` along `L` is universal iff
the corresponding left extension of `G ⋙ F` along `G ⋙ L` is. -/
noncomputable def isUniversalPrecompEquiv (e : RightExtension L F) :
    e.IsUniversal ≃ ((RightExtension.precomp L F G).obj e).IsUniversal := by
  apply IsTerminal.isTerminalIffObj (RightExtension.precomp L F G)

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