mul_inv_mem_inertia — Mathlib

English

If φ and ψ are two Frobenius endomorphisms at Q, then their ratio σ σ'^{-1} lies in the inertia group of Q for the acting group G; i.e., their difference is invisible to the residue action.

Русский

Если оба отображения φ и ψ являются Фробениус-отображениями по Q, то их отношение σ σ'^{-1} лежит в инерционной подгруппе над Q для действующей группы G; т.е. их различие не влияет на остатки.

LaTeX

$$σ * σ'^{-1} ∈ Q.toAddSubgroup.inertia G$$

Lean4

theorem mul_inv_mem_inertia (H : IsArithFrobAt R σ Q) (H' : IsArithFrobAt R σ' Q) :
    σ * σ'⁻¹ ∈ Q.toAddSubgroup.inertia G := by
  intro x
  simpa [mul_smul] using sub_mem (H (σ'⁻¹ • x)) (H' (σ'⁻¹ • x))

Похожие утверждения