English
Let P be an ideal of R and suppose there exist primes Q over P in S with finite quotients. Then there is a Frobenius assignment σ sending each Q to a Frobenius element in G, and such that Frobenius elements over primes lying over the same P are conjugate.
Русский
Пусть P — идеал R, и существуют простые Q над P в S с конечными частными полями. Тогда существует отображение σ, сопоставляющее каждому Q элемент Фробениуса в G, и такие элементы Ф робениуса над простыми, лежащими над одним P, сопряжены.
LaTeX
$$$\exists \sigma:(P.primesOver\ S) \to G,\ (\forall Q,\ IsArithFrobAt\; R\, (\sigma Q)\; Q.1)\ \land\ (\forall Q_1,Q_2,\ IsConj\ (\sigma Q_1)\ (\sigma Q_2)).$$$
Lean4
theorem exists_primesOver_isConj (P : Ideal R) (hP : ∃ Q : Ideal.primesOver P S, Finite (S ⧸ Q.1)) :
∃ σ : Ideal.primesOver P S → G, (∀ Q, IsArithFrobAt R (σ Q) Q.1) ∧ (∀ Q₁ Q₂, IsConj (σ Q₁) (σ Q₂)) :=
by
obtain ⟨⟨Q, hQ₁, hQ₂⟩, hQ₃⟩ := hP
have (Q' : Ideal.primesOver P S) : ∃ σ : G, Q'.1 = σ • Q :=
Algebra.IsInvariant.exists_smul_of_under_eq R S G _ _ (hQ₂.over.symm.trans Q'.2.2.over)
choose τ hτ using this
obtain ⟨σ, hσ⟩ := exists_of_isInvariant R G Q
refine
⟨fun Q' ↦ τ Q' * σ * (τ Q')⁻¹, fun Q' ↦ hτ Q' ▸ hσ.conj (τ Q'), fun Q₁ Q₂ ↦
.trans (.symm (isConj_iff.mpr ⟨τ Q₁, rfl⟩)) (isConj_iff.mpr ⟨τ Q₂, rfl⟩)⟩
