English
The cyclotomic character is continuous with respect to the natural topologies on automorphisms and the units of Padic integers, under suitable hypotheses on roots of unity.
Русский
Циклотомический характер непрерывен относительно естественных топологий автоморфизмов и единиц Padic, при подходящих предпосылках на корни единицы.
LaTeX
$$$\\text{continuous}(\\chi) \\quad\\text{in the appropriate topologies}$$$
Lean4
theorem continuous (p : ℕ) [Fact p.Prime] (K L : Type*) [Field K] [Field L] [Algebra K L] :
Continuous ((cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut (L ≃ₐ[K] L) L)) :=
by
by_cases H : ∀ (i : ℕ), ∃ ζ : L, IsPrimitiveRoot ζ (p ^ i); swap
· simp only [cyclotomicCharacter, cyclotomicCharacter.toFun, dif_neg H, MonoidHom.coe_comp]
exact continuous_const (y := 1)
haveI _ (i) : HasEnoughRootsOfUnity L (p ^ i) := ⟨H i, rootsOfUnity.isCyclic _ _⟩
choose ζ hζ using H
refine Continuous.of_coeHom_comp ?_
apply continuous_of_continuousAt_one
rw [ContinuousAt, map_one,
(galGroupBasis K L).nhds_one_hasBasis.tendsto_iff (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))]
intro ε hε
obtain ⟨k, hk', hk⟩ : ∃ k : ℕ, k ≠ 0 ∧ p ^ (-k : ℤ) < ε :=
by
obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩
refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
· exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top
· intro σ hσ
refine lt_of_le_of_lt ?_ hk
dsimp
rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow, RingHom.mem_ker, map_sub,
map_one, cyclotomicCharacter.toZModPow, sub_eq_zero, eq_comm]
apply modularCyclotomicCharacter.unique
intro t ht
obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht
rw [ZMod.val_one'', pow_one]
· exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩
· exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'
