English
Let G be finite, S and R as above, and Q a prime of S with finite residue field. Then there exists a Frobenius element σ ∈ G such that Q is a Frobenius at σ.
Русский
Пусть G конечен, S и R как выше, и Q — простый идеал S с конечным остаточным полем. Существует элемент Фробениуса σ ∈ G, для которого Q является Фробениусом в точке σ.
LaTeX
$$$\exists \sigma \in G,\ IsArithFrobAt\; R\; \sigma\; Q.$$$
Lean4
/-- Let `G` be a finite group acting on `S`, and `R` be the fixed subring.
If `Q` is a prime of `S` with finite residue field,
then there exists a Frobenius element `σ : G` at `Q`. -/
theorem exists_of_isInvariant [Q.IsPrime] [Finite (S ⧸ Q)] : ∃ σ : G, IsArithFrobAt R σ Q :=
by
let P := Q.under R
have := Algebra.IsInvariant.isIntegral R S G
have : Q.IsMaximal := Ideal.Quotient.maximal_of_isField _ (Finite.isField_of_domain (S ⧸ Q))
have : P.IsMaximal := Ideal.isMaximal_comap_of_isIntegral_of_isMaximal Q
obtain ⟨p, hc⟩ := CharP.exists (R ⧸ P)
have : Finite (R ⧸ P) := .of_injective _ Ideal.algebraMap_quotient_injective
cases nonempty_fintype (R ⧸ P)
obtain ⟨k, hp, hk⟩ := FiniteField.card (R ⧸ P) p
have := CharP.of_ringHom_of_ne_zero (algebraMap (R ⧸ P) (S ⧸ Q)) p hp.ne_zero
have : ExpChar (S ⧸ Q) p := .prime hp
let l : (S ⧸ Q) ≃ₐ[R ⧸ P] S ⧸ Q :=
{ __ := iterateFrobeniusEquiv (S ⧸ Q) p k,
commutes'
r := by
dsimp [iterateFrobenius_def]
rw [← map_pow, ← hk, FiniteField.pow_card] }
obtain ⟨σ, hσ⟩ := Ideal.Quotient.stabilizerHom_surjective G P Q l
refine ⟨σ, fun x ↦ ?_⟩
rw [← Ideal.Quotient.eq, Nat.card_eq_fintype_card, hk]
exact DFunLike.congr_fun hσ (Ideal.Quotient.mk Q x)
