eqToHom_iso_hom_naturality — Mathlib

English

A variant of eqToHom_naturality using isomorphisms: for z_b: f(b) ≅ g(b), the hom-component naturality holds: (z_j).hom ≫ eqToHom(h) = eqToHom(h) ≫ (z_{j'}).hom when w: j = j'.

Русский

Вариант eqToHom_naturality с изоморфизмами: для z_b: f(b) ≅ g(b) выполняется натуральность гомоморфизмов: (z_j).hom ≫ eqToHom(h) = eqToHom(h) ≫ (z_{j'}).hom при w: j = j'.

LaTeX

$$$ (z_j).hom \\circ eqToHom( by simp [w] ) = eqToHom( by simp [w] ) \\circ (z_{j}).hom $$$

Lean4

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

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