instFiniteIntAdditiveUnitsRingOfIntegers

English

A basis for the quotient (𝓞 K)ˣ/(torsion K) as an additive ℤ-module is obtained by a chosen free basis.

Русский

База для модуля (𝓞 K)ˣ/(torsion K) над целочисленным кольцом получается из выбранной свободной базы.

LaTeX

$$basisModTorsion : Basis (Fin (rank K)) \mathbb{Z} (Additive ((𝓞 K)ˣ / (torsion K)))$$

Lean4

instance : Module.Finite ℤ (Additive (𝓞 K)ˣ) := by
  rw [Module.finite_def]
  refine
    Submodule.fg_of_fg_map_of_fg_inf_ker (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ?_ ?_
  · rw [Submodule.map_top, LinearMap.range_eq_top.mpr (by exact QuotientGroup.mk'_surjective (torsion K)), ←
      Module.finite_def]
    infer_instance
  · rw [inf_of_le_right le_top, AddMonoidHom.coe_toIntLinearMap_ker, MonoidHom.coe_toAdditive_ker,
      QuotientGroup.ker_mk', Submodule.fg_iff_addSubgroup_fg, AddSubgroup.toIntSubmodule_toAddSubgroup, ←
      AddGroup.fg_iff_addSubgroup_fg]
    have : Finite (Subgroup.toAddSubgroup (torsion K)) := (inferInstance : Finite (torsion K))
    exact AddGroup.fg_of_finite

Похожие утверждения