English
The inverse map defined by eHomCongr respects composition of morphisms in the opposite direction.
Русский
Обратная карта, задаваемая eHomCongr, сохраняет композицию морфизмов в противоположном направлении.
LaTeX
$$$\mathrm{eHomEquiv}(V\, (f \circ g)) \circ (\mathrm{eHomCongr}(V, \alpha, \gamma))^{-1} = (\lambda_{(\mathbf{1}_V)})^{-1} \circ (\mathrm{eHomEquiv}(V,f) \circ (\mathrm{eHomCongr}(V, \alpha, \beta))^{-1}) \otimes (\mathrm{eHomEquiv}(V,g) \circ (\mathrm{eHomCongr}(V, \beta, \gamma))^{-1}) \circ eComp V X Y Z.$$$
Lean4
/-- The inverse map defined by `eHomCongr` respects composition of morphisms. -/
@[reassoc]
theorem eHomCongr_inv_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X₁ ⟶ Y₁) (g : Y₁ ⟶ Z₁) :
eHomEquiv V (f ≫ g) ≫ (eHomCongr V α γ).inv =
(λ_ _).inv ≫
(eHomEquiv V f ≫ (eHomCongr V α β).inv) ▷ _ ≫ _ ◁ (eHomEquiv V g ≫ (eHomCongr V β γ).inv) ≫ eComp V X Y Z :=
eHomCongr_comp V α.symm β.symm γ.symm f g
