instIsEquivalenceLeftExtensionPostcomp₁OfIsIso

English

If G is an equivalence and f is a map in the costructured arrow giving a postcomposition, then the induced functor is an equivalence; the universal property respects isomorphisms.

Русский

Если G — эквивалентность, и f — отображение вCostructuredArrow, задающее пост-композицию, тогда индуцированная конструкция эквивалентна; универсальное свойство сохраняется по изоморфизмам.

LaTeX

$$$\text{(LeftExtension.postcomp₁ } G f F) \text{ IsEquivalence}$$$

Lean4

noncomputable instance (f : L' ⟶ L ⋙ G) [IsIso f] (F : C ⥤ H) : IsEquivalence (LeftExtension.postcomp₁ G f F) := by
  apply StructuredArrow.isEquivalenceMap₂

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