English
In a CM-field K, the closure of the subgroup generated by the real fundamental system together with torsion coincides with the subgroup of real units together with torsion; i.e., closure of realFundSystem(K) and torsion(K) equals realUnits(K) and torsion(K).
Русский
В поле CM K замыкание подгруппы, порождаемой реальной фундаментальной системой вместе с torsion, совпадает с подгруппой реальных единиц вместе с torsion; то есть closure(realFundSystem(K)) ⊔ torsion(K) = realUnits(K) ⊔ torsion(K).
LaTeX
$$$\\overline{\\langle \\mathrm{realFundSystem}(K) \\rangle} \\;\\sqcup\\; \\mathrm{torsion}(K) \;=\\; \\mathrm{realUnits}(K) \\;\\sqcup\\; \\mathrm{torsion}(K)$$$
Lean4
theorem closure_realFundSystem_sup_torsion :
Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K = realUnits K ⊔ torsion K :=
by
have : Subgroup.map (Units.map (algebraMap (𝓞 K⁺) (𝓞 K))) (torsion K⁺) ≤ torsion K :=
by
rintro _ ⟨x, hx, rfl⟩
exact MonoidHom.isOfFinOrder _ hx
rw [realUnits, MonoidHom.range_eq_map, ← closure_fundSystem_sup_torsion_eq_top, Subgroup.map_sup, sup_assoc,
RingHom.toMonoidHom_eq_coe, sup_eq_right.mpr this, MonoidHom.map_closure]
congr; ext
simp [realFundSystem, Equiv.exists_congr_left (finCongr (units_rank_eq_units_rank K).symm)]
