English
The map Rat.castHom(ℚ_[p]) ∘ WithVal.equiv(Rat.padicValuation p) is a uniform inducing map.
Русский
Отображение Rat.castHom(ℚ_[p]) ∘ WithVal.equiv(Rat.padicValuation p) является равномерно индуктивным отображением.
LaTeX
$$$IsUniformInducing\\left(\\operatorname{Rat.castHom}(\\mathbb{Q}_p) \\circ WithVal.equiv(\\operatorname{Rat.padicValuation}(p)) \\right)$$$
Lean4
theorem isUniformInducing_cast_withVal :
IsUniformInducing ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) :=
by
have hp0' : 0 < (p : ℚ) := by simp [Nat.Prime.pos Fact.out]
have hp0 : 0 < (p : ℝ)⁻¹ := by simp [Nat.Prime.pos Fact.out]
have hp1' : 1 < (p : ℚ) := by simp [Nat.Prime.one_lt Fact.out]
have hp1 : (p : ℝ)⁻¹ < 1 := by simp [inv_lt_one_iff₀, Nat.Prime.one_lt Fact.out]
rw [Filter.HasBasis.isUniformInducing_iff (Valued.hasBasis_uniformity _ _)
(Metric.uniformity_basis_dist_le_pow hp0 hp1)]
simp only [Set.mem_setOf_eq, dist_eq_norm_sub, inv_pow, RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, Rat.coe_castHom,
RingHom.coe_coe, Function.comp_apply, ← Rat.cast_sub, ← map_sub, Padic.eq_padicNorm, true_and, forall_const]
constructor
· intro n
use Units.mk0 (exp (-n : ℤ)) (by simp)
intro x y h
set x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x with hx
set y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y with hy
rw [Valuation.map_sub_swap, Units.val_mk0] at h
change Rat.padicValuation p (x' - y') < exp _ at h
rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le]
· rw [map_sub, ← hx, ← hy]
simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, padicNorm, zpow_neg,
Nat.cast_pow] at h ⊢
split_ifs with H
· simp
· simp only [H, ↓reduceIte, exp_lt_exp, neg_lt_neg_iff] at h
simpa [hp0', zpow_pos, pow_pos, inv_le_inv₀] using
zpow_right_mono₀ (a := (p : ℚ)) (by exact_mod_cast (Nat.Prime.one_le Fact.out)) h.le
· simp [Nat.Prime.ne_zero Fact.out]
· intro γ
use (log (γ.val * exp (-1))).natAbs
intro x y h
set x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x with hx
set y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y with hy
rw [Valuation.map_sub_swap]
change Rat.padicValuation p (x' - y') < γ
rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le] at h
· change padicNorm p (x' - y') ≤ _ at h
simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, padicNorm, zpow_neg,
Nat.cast_pow] at h ⊢
split_ifs with H
· simp
· rw [← lt_log_iff_exp_lt (by simp)]
simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le, Int.lt_iff_add_one_le]
· simp [Nat.Prime.ne_zero Fact.out]
