cocyclesMap_id_comp — Mathlib

English

For φ: A ⟶ B and ψ: B ⟶ C, and n ∈ ℕ, cocyclesMap(id_G) (φ ≫ ψ) n equals cocyclesMap id_G φ n composed with cocyclesMap id_G ψ n, reflecting functoriality with respect to composing morphisms in the target representation.

Русский

Для φ: A ⟶ B и ψ: B ⟶ C и n ∈ ℕ верно cocyclesMap(id_G)(φ ≫ ψ) n = cocyclesMap id_G φ n ∘ cocyclesMap id_G ψ n.

LaTeX

$$$\\\\cocyclesMap(\\\\mathrm{id}_G)(\\\\varphi \\\\gg \\\\psi)\\\\, n = \\\\cocyclesMap(\\\\mathrm{id}_G)\\\\varphi n \\\\circ \\\\cocyclesMap(\\\\mathrm{id}_G)\\\\psi n$$$

Lean4

@[reassoc]
theorem cocyclesMap_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ) :
    cocyclesMap (MonoidHom.id G) (φ ≫ ψ) n = cocyclesMap (MonoidHom.id G) φ n ≫ cocyclesMap (MonoidHom.id G) ψ n := by
  simp [cocyclesMap, cochainsMap_id_comp, HomologicalComplex.cyclesMap_comp]

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