homCongr_comp — Mathlib

English

Under equivalences eL, eR and a morphism w'.hom that respects these equivalences, the Guitart exactness of the refined vertical composition is equivalent to that of the original w.

Русский

При эквивалентностях eL, eR и отображении w'.hom, сохраняется эквивалентность точности Guitart для уточнённой вертикальной композиции и исходного w.

LaTeX

$$$ (w.vComp' w'.hom eL eR).GuitartExact \\iff w.GuitartExact $$$

Lean4

theorem homCongr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁) (f : X ⟶ Y) (g : Y ⟶ Z) :
    α.homCongr γ (f ≫ g) = α.homCongr β f ≫ β.homCongr γ g := by simp

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