English
Let u,v be two families of units of rank K. If the kernel conditions hold (IsMaxRank v and closure relations with torsion), then regOfFamily(u) / regOfFamily(v) equals the index of the closure of the span of u inside the closure of the span of v, modulo torsion.
Русский
Пусть u,v — две пары единиц; если выполняются условия максимального ранга и отношения замыкания с торсионом, то отношение regOfFamily(u) к regOfFamily(v) равно индексу соответствующей группы по отношению к торсиону.
LaTeX
$$regOfFamily u / regOfFamily v = (Subgroup.closure (Set.range u) ⊔ (torsion K)).relIndex (Subgroup.closure (Set.range v) ⊔ (torsion K))$$
Lean4
/-- Let `u` be a family of units. Then the ratio `regOfFamily u / regulator K` is equal to the index
of the subgroup generated by `u` and `torsion K` inside the group of units of `K`.
-/
theorem regOfFamily_div_regulator (u : Fin (rank K) → (𝓞 K)ˣ) :
regOfFamily u / regulator K = (Subgroup.closure (Set.range u) ⊔ (torsion K)).index := by
rw [regulator_eq_regOfFamily_fundSystem,
regOfFamily_div_regOfFamily (isMaxRank_fundSystem K) (by simp only [closure_fundSystem_sup_torsion_eq_top, le_top]),
closure_fundSystem_sup_torsion_eq_top, Subgroup.relIndex_top_right]
