homCongr_apply — Mathlib

English

The linear equivalence homCongr acts on a morphism f by f ↦ f1^{-1} f f2, matching the canonical left-right action of iso.

Русский

Линейное эквалентное отображение homCongr действует на морфизм f как f ↦ f1^{-1} f f2.

LaTeX

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

Lean4

theorem homCongr_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 : X ⟶ W) : homCongr k f₁ f₂ f = (f₁.inv ≫ f) ≫ f₂.hom :=
  rfl

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