Theorems · Theorem · number theory

IsArithFrobAt.exists_of_isInvariant

∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] (Q : Ideal S) [Finite G]
  [Algebra.IsInvariant R S G] [Q.IsPrime] [Finite (S ⧸ Q)], ∃ σ, IsArithFrobAt R σ Q

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.

Defined in

Mathlib.RingTheory.Frobenius

Cited by

1 results in Mathlib

Foundations

Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraGroupMulSemiringActionSMulCommClassFiniteAlgebra.IsInvariantIdeal.IsPrimeFinite