map_comp — Mathlib

English

For f: H →* K and g: G →* H with φ and ψ, the map for f ∘ g equals the composition of maps for f and g, i.e., map (f ∘ g) (res g.map φ ≫ ψ) n = map f φ n ≫ map g ψ n.

Русский

Для f: H →* K и g: G →* H с φ и ψ, отображение для f ∘ g равно композиции отображений: map (f ∘ g) (res g.map φ ≫ ψ) n = map f φ n ≫ map g ψ n.

LaTeX

$$$\\\\map(f\\\\cdot g) ((Action.res _ g).map φ \\\\gg ψ) n = \\\\map f φ n \\\\gg \\\\map g ψ n$$$

Lean4

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

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