inv_map_inv_app — Mathlib

English

Let F : C ⥤ D ⥤ E and e : X ≅ Y. For any Z ∈ D, inv ((F.map e.inv).app Z) = (F.map e.hom).app Z.

Русский

Пусть F : C ⥤ D ⥤ E и e : X ≅ Y. Для любого Z ∈ D выполняется inv ((F.map e.inv).app Z) = (F.map e.hom).app Z.

LaTeX

$$$ inv((F.map e.inv).app Z) = (F.map e.hom).app Z $$$

Lean4

@[simp]
theorem inv_map_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :
    inv ((F.map e.inv).app Z) = (F.map e.hom).app Z := by
  cat_disch
    -- TODO: `hom_inv_id` and `inv_hom_id` are not yet working via `grind`,
    -- but they work fine in my minimization in the `grind` test suite.
    -- Investigate on nightly-testing / the next release?

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