homCongr_trans — Mathlib

English

Applying the identity isomorphism on both sides leaves the morphism unchanged after homCongr.

Русский

Применение тождественной изоморфности слева и справа оставляет морфизм без изменений после homCongr.

LaTeX

$$$ (\\mathrm{Iso.refl}\\, X).homCongr (\\mathrm{Iso.refl}\\, Y) f = f $$$

Lean4

theorem homCongr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂) (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃)
    (f : X₁ ⟶ Y₁) : (α₁ ≪≫ α₂).homCongr (β₁ ≪≫ β₂) f = (α₁.homCongr β₁).trans (α₂.homCongr β₂) f := by simp

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