map₂_inv — Mathlib

English

For η : f ≅ g, the composite F.map₂ η.inv ≫ F.map₂ η.hom equals the identity on F.map g.

Русский

Для η : f ≅ g, композиция F.map₂ η.inv ≫ F.map₂ η.hom равна тождественному на F.map g.

LaTeX

$$$F.map₂ η.inv ≫ F.map₂ η.hom = 𝟙 (F.map g)$$$

Lean4

@[simp]
theorem map₂_inv {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] : F.map₂ (inv η) = inv (F.map₂ η) :=
  by
  apply IsIso.eq_inv_of_hom_inv_id
  simp [← F.map₂_comp η (inv η)]

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