English
Analogous to additive case, the index of a subgroup of ι → Multiplicative ℤ corresponds to a multiplicative equivalence with ι → Multiplicative ℤ.
Русский
Индекс подгруппы ι → Multiplicative ℤ соответствует мультипликативному эквиваленту с ι → Multiplicative ℤ.
LaTeX
$$H.index ≠ 0 ↔ ∃ e, H ≃* (ι → Multiplicative ℤ)$$
Lean4
theorem subgroup_index_ne_zero_iff {H : Subgroup (ι → Multiplicative ℤ)} :
H.index ≠ 0 ↔ Nonempty (H ≃* (ι → Multiplicative ℤ)) :=
by
let em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative _ _
let H' : Subgroup (Multiplicative (ι → ℤ)) := H.comap em
let eH' : H' ≃* H :=
(MulEquiv.subgroupCongr <| Subgroup.comap_equiv_eq_map_symm em H).trans (MulEquiv.subgroupMap em.symm _).symm
have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective
rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]
exact
⟨fun ⟨e⟩ ↦ ⟨(eH'.symm.trans (AddEquiv.toMultiplicative e)).trans em⟩, fun ⟨e⟩ ↦
⟨(MulEquiv.toAdditive ((eH'.trans e).trans em.symm)).trans (AddEquiv.additiveMultiplicative _)⟩⟩
