English
For any family u, regOfFamily(u)/regulator(K) equals the index of the closed span of u together with torsion inside the full unit group.
Русский
Для любой семьи u отношение regOfFamily(u)/regulator(K) равно индексу замыкания поршня в группе единиц.
LaTeX
$$regOfFamily u / regulator K = (Subgroup.closure (Set.range u) ⊔ (torsion K)).index$$
Lean4
/-- If `f` is bounded and not trivial, then it is equivalent to a p-adic absolute value. -/
theorem equiv_padic_of_bounded : ∃! p, ∃ (_ : Fact p.Prime), f.IsEquiv (padic p) :=
by
obtain ⟨p, hfp, hmin⟩ := exists_minimal_nat_zero_lt_and_lt_one hf_nontriv bdd
have hprime := is_prime_of_minimal_nat_zero_lt_and_lt_one hfp.1 hfp.2 hmin
have hprime_fact : Fact p.Prime := ⟨hprime⟩
obtain ⟨t, h⟩ := exists_pos_eq_pow_neg hfp.1 hfp.2 hmin
simp_rw [← exists_nat_rpow_iff_isEquiv]
refine ⟨p, ⟨hprime_fact, t⁻¹, inv_pos_of_pos h.1, fun n ↦ ?_⟩, fun q ⟨hq_prime, h_equiv⟩ ↦ ?_⟩
· have ht : t⁻¹ ≠ 0 := inv_ne_zero h.1.ne'
rcases eq_or_ne n 0 with rfl | hn
· simp [ht]
· /- Any natural number can be written as a power of p times a natural number not divisible
by p -/
rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hprime.ne_one with ⟨e, m, hpm, rfl⟩
simp only [Nat.cast_mul, Nat.cast_pow, map_mul, map_pow, h.2, eq_one_of_not_dvd bdd hfp.1 hfp.2 hmin hpm,
padic_eq_padicNorm, padicNorm.padicNorm_p_of_prime, cast_inv, cast_natCast, inv_pow]
rw [← padicNorm.nat_eq_one_iff] at hpm
simp only [← rpow_natCast, p.cast_nonneg, ← rpow_mul, neg_mul, mul_one, ← rpow_neg, hpm, cast_one]
congr
field_simp [h.1.ne']
· by_contra! hne
apply hq_prime.elim.ne_one
rw [ne_comm, ← Nat.coprime_primes hprime hq_prime.elim, hprime.coprime_iff_not_dvd] at hne
rcases h_equiv with ⟨c, _, h_eq⟩
simpa [eq_one_of_not_dvd bdd hfp.1 hfp.2 hmin hne] using h_eq q
