map_comp — Mathlib

English

For morphisms f and g, and corresponding φ and ψ, there is a compatibility between maps: map(g ∘ f, φ ≫ Res_f.map ψ, n) = map f φ n ≫ map g ψ n.

Русский

Для отображений f и g и соответствующих φ и ψ существует совместимость отображений: map(g ∘ f, φ ≫ Res_f.map ψ, n) = map f φ n ≫ map g ψ n.

LaTeX

$$$\mathrm{map}(g \cdot f, \phi \gg (\mathrm{Res}\_f(\psi)), n) = \mathrm{map}(f, \phi, n) \circ \mathrm{map}(g, \psi, n)$$$

Lean4

@[reassoc]
theorem map_comp {G H K : Type u} [Group G] [Group H] [Group K] {A : Rep k G} {B : Rep k H} {C : Rep k K} (f : G →* H)
    (g : H →* K) (φ : A ⟶ (Action.res _ f).obj B) (ψ : B ⟶ (Action.res _ g).obj C) (n : ℕ) :
    map (g.comp f) (φ ≫ (Action.res _ f).map ψ) n = map f φ n ≫ map g ψ n := by
  simp [map, ← HomologicalComplex.homologyMap_comp, ← chainsMap_comp]

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