homCongr_symm_apply — Mathlib

English

The symmetric application on the inverse side yields the corresponding formula using f1.hom and f2.inv.

Русский

Симметричное применение к обратной стороне задаёт формулу через f1.hom и f2.inv.

LaTeX

$$$\\bigl(\\mathrm{homCongr}\\,k\\, f_1\\, f_2\\bigr)^{\\,-1}(f) = f_1.hom \\circ f \\circ f_2^{-1}.$$$

Lean4

theorem homCongr_symm_apply (k : Type*) {C : Type*} [Category C] [Semiring k] [Preadditive C] [Linear k C] {X Y W Z : C}
    (f₁ : X ≅ Y) (f₂ : W ≅ Z) (f : Y ⟶ Z) : (homCongr k f₁ f₂).symm f = f₁.hom ≫ f ≫ f₂.inv :=
  rfl

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