English
There is a map on quotients by integer powers, induced by a pair of homomorphisms; composition respects the quotient construction.
Русский
Существует отображение на фактор-группах по степеням целого числа, индуцированное парой гомоморфизмов; композиция сохраняет фактор-структуру.
LaTeX
$$homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n)$$
Lean4
/-- The map of quotients by powers of an integer induced by a group homomorphism. -/
@[to_additive /-- The map of quotients by multiples of an integer induced by an additive group
homomorphism. -/
]
def homQuotientZPowOfHom : A ⧸ (zpowGroupHom n : A →* A).range →* B ⧸ (zpowGroupHom n : B →* B).range :=
lift _ ((mk' _).comp f) fun g ⟨h, (hg : h ^ n = g)⟩ =>
(eq_one_iff _).mpr ⟨f h, by simp only [← hg, map_zpow, zpowGroupHom_apply]⟩
