English
An abstract notion of Frobenius at an ideal Q in a ring S, defined via a compatible action of a monoid on S that is trivial on the base ring R.
Русский
Абстрактное понятие Фробениуса по идеалу Q в кольце S, определяемое через совместное действие моноида на S, тривиальное на базовом кольце R.
LaTeX
$$IsArithFrobAt(σ, Q) := (MulSemiringAction.toAlgHom R S σ).IsArithFrobAt Q$$
Lean4
/-- Suppose `S` is an `R` algebra, `M` is a monoid acting on `S` whose action is trivial on `R`
`σ : M` is an (arithmetic) Frobenius at an ideal `Q` of `S` if `σ • x ≡ x ^ q (mod Q)` for all `x`.
-/
abbrev IsArithFrobAt {M : Type*} [Monoid M] [MulSemiringAction M S] [SMulCommClass M R S] (σ : M) (Q : Ideal S) :
Prop :=
(MulSemiringAction.toAlgHom R S σ).IsArithFrobAt Q
