English
Let k be a commutative ring and G, H, K be groups. For representations A ∈ Rep(k, K), B ∈ Rep(k, H), C ∈ Rep(k, G) and group homomorphisms f: H → K, g: G → H, together with a morphism φ: Res_f(A) → B and ψ: Res_g(B) → C, the induced map on first cohomology is functorial with respect to composition; i.e., the map along f ∘ g applied to the composite φ, ψ equals the composite of the maps along f and g.
Русский
Пусть k — коммутативное кольцо, G, H, K — группы. Пусть A ∈ Rep(k, K), B ∈ Rep(k, H), C ∈ Rep(k, G), f: H → K и g: G → H — гомоморфизмы, φ: Res_f(A) → B и ψ: Res_g(B) → C — отображения, индуцируемые на Z¹(H, A) → Z¹(G, B). Тогда совместимость по композиции: для f ∘ g выполняется равенство соответствующих отображений на H¹.
LaTeX
$$$\operatorname{mapShortComplexH1}(f \circ g)\big((\mathrm{Action.res}\, g).map\varphi \;\circ\; \psi\big) = \operatorname{mapShortComplexH1} f \varphi \;\circ\; \operatorname{mapShortComplexH1} g \psi$$$
Lean4
@[reassoc]
theorem mapShortComplexH1_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) :
mapShortComplexH1 (f.comp g) ((Action.res _ g).map φ ≫ ψ) = mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ :=
rfl
