map_homCongr — Mathlib

English

Under a functor F, the map of a homCongr corresponds to the homCongr of the mapped components.

Русский

Под перестановкой через функтор F отображение homCongr соответствует homCongr отображённых компонент.

LaTeX

$$$ F.map (Iso.homCongr \\alpha \\beta f) = Iso.homCongr (F.mapIso \\alpha) (F.mapIso \\beta) (F.map f) $$$

Lean4

theorem map_homCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ⟶ Y) :
    F.map (Iso.homCongr α β f) = Iso.homCongr (F.mapIso α) (F.mapIso β) (F.map f) := by simp

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