English
If an element σ ∈ G yields a Frobenius at Q, then for any τ ∈ G the element τ σ τ^{-1} yields a Frobenius at the τ-action on Q, i.e. at τ · Q.
Русский
Если σ ∈ G дает Фробениус на Q, то для любого τ ∈ G элемент τ σ τ^{-1} задает Фробениус над τ · Q.
LaTeX
$$$ (H) \rightarrow \forall \tau \in G,\ IsArithFrobAt\; R\ (\tau\,\sigma\,\tau^{-1})\ (\tau \cdot Q). $$$
Lean4
theorem conj (H : IsArithFrobAt R σ Q) (τ : G) : IsArithFrobAt R (τ * σ * τ⁻¹) (τ • Q) :=
by
intro x
have : (Q.map (MulSemiringAction.toRingEquiv G S τ)).under R = Q.under R :=
by
rw [← Ideal.comap_symm, ← Ideal.comap_coe, Ideal.under, Ideal.comap_comap]
congr 1
exact (MulSemiringAction.toAlgEquiv R S τ).symm.toAlgHom.comp_algebraMap
rw [Ideal.pointwise_smul_eq_comap, Ideal.mem_comap]
simpa [smul_sub, mul_smul, this] using H (τ⁻¹ • x)
