inv_hom_id_eval — Mathlib

English

For an isomorphism of graded objects e : X ≅ Y and a component j, the composition e.hom j ≫ e.inv j equals the identity on Y_j.

Русский

Для изоморфизма e : X ≅ Y и компонента j, композиция e.hom j ∘ e.inv j равна тождественному отображению на Y_j.

LaTeX

$$$ e.hom j \\;∘\\; e.inv j = 𝟙 _ $$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_id_eval (e : X ≅ Y) (j : J) : e.inv j ≫ e.hom j = 𝟙 _ := by
  rw [← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id, GradedObject.categoryOfGradedObjects_id]

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