hom_inv_id_hom_app — Mathlib

English

Let F and G be single-functors with an isomorphism e: F ≅ G. Then for every a ∈ A and every object X ∈ C, the component of e at a on X is invertible and its inverse composes to the identity: (e.hom a)_X ∘ (e.inv a)_X = id_{F(a)(X)}.

Русский

Пусть F и G — однопараметрические функторы, между которыми имеется изоморфизм e: F ≅ G. Тогда для каждого a ∈ A и каждого объекта X ∈ C компонент e на a в X образует изоморфизм с обратным компонентом, и их объединение даёт тождественный морфизм: (e.hom a)_X ∘ (e.inv a)_X = id_{F(a)(X)}.

LaTeX

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

Lean4

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

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