eqToHom_iso_inv_naturality — Mathlib

English

If H: E ⥤ C is a functor and F ≍ G as functors from C to D (in terms of maps), then composing with H on the left preserves HEq: (H ⋙ F) ≍ (H ⋙ G).

Русский

Если H: E ⥤ C и F ≍ G как Функторы C ⥤ D (но в терминах отображений), то левая композиция сохраняет HEq: (H ⋙ F) ≍ (H ⋙ G).

LaTeX

$$$ (H \\; \\cdot\\; F) \\mathrel{\\equiv} (H \\; \\cdot\\; G) $$$

Lean4

/-- A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`. -/
@[reassoc (attr := simp)]
theorem eqToHom_iso_inv_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
    (z j).inv ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').inv :=
  by
  cases w
  simp

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