app — Mathlib

English

Let app' assign to each object X an isomorphism F.obj X ≅ G.obj X, with a naturality condition. Then the X-component of the constructed natural isomorphism equals app' X.

Русский

Пусть каждому объекту X ставится изоморфизм F.obj X ≅ G.obj X и выполняется условие естественности. Тогда X-компонента полученного натурального изоморфизма равна app' X.

LaTeX

$$$ (\mathrm{ofComponents}\ app'\ \mathrm{naturality}).\mathrm{app}(X) = app'(X) $$$

Lean4

@[simp]
theorem app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) : (ofComponents app' naturality).app X = app' X := by
  cat_disch
    -- Making this an instance would cause a typeclass inference loop with `isIso_app_of_isIso`.

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