map₂_inv_hom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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