English
If the kernels and ranges of a homomorphism f have coprime cardinalities and both kernel and range are cyclic, then M is cyclic.
Русский
Если кардинальности ядра и образа гомоморфизма попарно взаимно просты, и оба они цикличны, тогда M циклична.
LaTeX
$$Group.isCyclic_of_coprime_card_ker$$
Lean4
@[to_additive]
theorem isCyclic_of_coprime_card_range_card_ker {M N : Type*} [CommGroup M] [Group N] (f : M →* N)
(h : (Nat.card f.ker).Coprime (Nat.card f.range)) [IsCyclic f.ker] [IsCyclic f.range] : IsCyclic M :=
by
cases (finite_or_infinite f.ker).symm
· rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
rwa [← Subgroup.topEquiv.isCyclic, ← h]
cases (finite_or_infinite f.range).symm
· rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h
rwa [(f.ofInjective (f.ker_eq_bot_iff.mp (f.ker.eq_bot_of_card_eq h))).isCyclic]
have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩
rw [IsCyclic.iff_exponent_eq_card]
apply dvd_antisymm Group.exponent_dvd_nat_card
rw [← f.ker.card_mul_index, Subgroup.index_ker]
apply h.mul_dvd_of_dvd_of_dvd <;> rw [← IsCyclic.exponent_eq_card]
· exact Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective
· exact MonoidHom.exponent_dvd f.rangeRestrict_surjective
