inv_hom_id_hom_app — Mathlib

English

Let e: F ≅ G be an isomorphism of single-functors. For every a ∈ A and every X ∈ C, the inverse component composed with the forward component is the identity on (G(a))(X): (e.inv a)_X ∘ (e.hom a)_X = id_{(G(a))(X)}.

Русский

Пусть e: F ≅ G — изоморфизм однопараметрических функторов. Для каждого a ∈ A и каждого X ∈ C, обратный компонент, взятый на X, компонуется с прямым в точности в тождественный морфизм на (G(a))(X).

LaTeX

$$$ (e.inv(n))_X \circ (e.hom(n))_X = \mathrm{id}_{(G.\mathrm{functor}(n))(X)}. $$$

Lean4

@[reassoc (attr := simp)]
theorem inv_hom_id_hom_app (e : F ≅ G) (n : A) (X : C) : (e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 _ := by
  rw [← NatTrans.comp_app, inv_hom_id_hom, NatTrans.id_app]

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