map_isoCongr — Mathlib

English

A functor preserves the isomorphism-based congruence between morphisms and their images under isomorphisms.

Русский

Функтор сохраняет конгруэнцию между морфизмами и их образами при изоморфизмах.

LaTeX

$$$ F.mapIso (\\alpha.isoCongr \\beta f) = (F.mapIso \\alpha).isoCongr (F.mapIso \\beta) (F.mapIso f) $$$

Lean4

theorem map_isoCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y) :
    F.mapIso (Iso.isoCongr α β f) = Iso.isoCongr (F.mapIso α) (F.mapIso β) (F.mapIso f) := by simp

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