unop_inv_hom_id_app — Mathlib

English

For e: F ≅ G with F,G: C ⥤ D^{op}, and any X, the composite (e.inv.app X)^{unop} ∘ (e.hom.app X)^{unop} equals the identity on F.obj X.

Русский

Для изоморфизма e: F ≅ G между F,G: C \\\\to D^{op} и любого X: (e.inv.app X)^{unop} ∘ (e.hom.app X)^{unop} = id_{F.obj X}.

LaTeX

$$$\\\\forall {C} [Category C], \\\\forall {D} [Category D^{op}], \\\\forall {F G : C \\\\to D^{op}}, \\\\forall e: F \\\\cong G, \\\\forall X, (e.inv.app X)^{\\\\mathrm{unop}} \\\\circ (e.hom.app X)^{\\\\mathrm{unop}} = id_{F.obj X}.$$$

Lean4

@[reassoc (attr := simp)]
theorem unop_inv_hom_id_app : (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 _ := by
  rw [← unop_comp, hom_inv_id_app, unop_id]

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