hom_inv_id_apply — Mathlib

English

Let F: J ⥤ Type be a functor and f: X ⟶ Y, g: Y ⟶ Z be morphisms. For a ∈ F.obj X, the map F.map (f ≫ g) applied to a equals F.map g (F.map f a).

Русский

Пусть F: J ⥤ Type — функтор, а f: X ⟶ Y, g: Y ⟶ Z — морфизмы. Для a ∈ F.obj X выполняется F.map (f ≫ g) a = F.map g (F.map f a).

LaTeX

$$$$ F.map (f \gg g)\, a = F.map g\,(F.map f\, a). $$$$

Lean4

@[simp]
theorem hom_inv_id_apply {X Y : Type u} (f : X ≅ Y) (x : X) : f.inv (f.hom x) = x :=
  congr_fun f.hom_inv_id x

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