hom_inv_id_eval — Mathlib

English

If a morphism f between graded objects is an isomorphism after applying map to each component, then f is an isomorphism.

Русский

Если морфизм f между градуированными объектами изоморфизм после применения отображения к каждому компоненту, тогда f — изоморфизм.

LaTeX

$$$ \\forall i, IsIso (f i) \\Rightarrow IsIso f $$$

Lean4

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

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