map₂_hom_inv — Mathlib

English

If η is an isomorphism, then the composed map on η.inv and η.hom yields an isomorphism with the inverse given by the other component.

Русский

Если η — изоморфизм, то композиция F.map₂ η.inv и F.map₂ η.hom образует изоморфизм; обратный относящийся к другой компоненте.

LaTeX

$$IsIso (F.map₂ η.inv)$$

Lean4

@[reassoc, simp]
theorem map₂_hom_inv {f g : a ⟶ b} (η : f ≅ g) : F.map₂ η.hom ≫ F.map₂ η.inv = 𝟙 (F.map f) := by
  rw [← F.map₂_comp, Iso.hom_inv_id, F.map₂_id]

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