map_conj — Mathlib

English

For a functor F: C → D, an isomorphism α: X ≅ Y and f ∈ End(X), the functor commutes with conjugation: F.map (α.conj f) = (F.mapIso α).conj (F.map f).

Русский

Пусть F: C → D — функтор, α: X ≅ Y, и f ∈ End(X). Тогда отображение функтором сохраняет сопряжение: F.map (α.conj f) = (F.mapIso α).conj (F.map f).

LaTeX

$$$ F(\\alpha.\\mathrm{conj} f) = (F(\\alpha)).\\mathrm{conj} (F(f)) $$$

Lean4

theorem map_conj {X Y : C} (α : X ≅ Y) (f : End X) : F.map (α.conj f) = (F.mapIso α).conj (F.map f) :=
  map_homCongr F α α f

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