English
Let f: A →* B and g: B →* A be group homomorphisms with g a right inverse of f (i.e., g ∘ f = id_A). Then for every integer n, the induced maps on the quotients by the image of the n-th power map satisfy (homQuotientZPowOfHom f n) ∘ (homQuotientZPowOfHom g n) = id on B/(z^n)-range, i.e., the two induced quotients are inverse to each other.
Русский
Пусть f: A →* B и g: B →* A — гомоморфизмы групп, причём g является правым обратным к f (g ∘ f = id_A). Тогда для любого целого n индуцированные отображения на фактор-группах по образу отображения z^n удовлетворяют (homQuotientZPowOfHom f n) ∘ (homQuotientZPowOfHom g n) = id на B/(zpowGroupHom n).range, то есть полученные фактор-гомоморфизмы взаимно обратны.
LaTeX
$$$(\\mathrm{homQuotientZPowOfHom}(f,n))\\circ(\\mathrm{homQuotientZPowOfHom}(g,n))=\\mathrm{id}_{\\,B\\,\\big/\\,(zpowGroupHom n).range}$$$
Lean4
@[to_additive (attr := simp)]
theorem homQuotientZPowOfHom_comp_of_rightInverse (i : Function.RightInverse g f) :
(homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) = MonoidHom.id _ :=
monoidHom_ext _ <| MonoidHom.ext fun x => congrArg _ <| i x
