regOfFamily_div_regOfFamily — Mathlib

English

For a fixed w′ and equivalence e, the product finrank_Q(K)·regulator(K) equals the absolute determinant of a matrix whose columns are formed as specified by the construction in the statement.

Русский

Для заданного w′ и эквивалентности e, произведение finrank_Q(K)·regulator(K) равно модулю детерминанта матрицы, чьи столбцы образованы согласно конструкции.

LaTeX

$$$\\mathrm{finrank}_{\\mathbb{Q}} K \\cdot \\mathrm{regulator}(K) = \\left| \\det \\left( \\text{Matrix.of}\\big( i,w: \\inftyplace K \\; |\\; w\\neq w' \\mapsto \\text{...} \\right) \\right|$$$

Lean4

/-- Let `u` and `v` be two families of units. Assume that the subgroup `U` generated by `u` and
`torsion K` is contained in the subgroup `V` generated by `v` and `torsion K`. Then the ratio
`regOfFamily u / regOfFamily v` is equal to the index of `U` inside `V`.
-/
theorem regOfFamily_div_regOfFamily {u v : Fin (rank K) → (𝓞 K)ˣ} (hv : IsMaxRank v)
    (h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K) :
    regOfFamily u / regOfFamily v =
      (Subgroup.closure (Set.range u) ⊔ (torsion K)).relIndex (Subgroup.closure (Set.range v) ⊔ (torsion K)) :=
  by
  classical
  by_cases hu : IsMaxRank u
  · have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) :=
      by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv, ←
        map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup, ←
        map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup, ← SupHomClass.map_sup, ←
        SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
    rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv, covolume_div_covolume_eq_relIndex _ _ this,
      span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker, ←
      OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]
  · rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]
    have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 :=
      by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
    rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h, ← Subgroup.not_finiteIndex_iff, ←
      finiteIndex_iff_sup_torsion_finiteIndex, ← isMaxRank_iff_closure_finiteIndex.not]

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