comap_eq — Mathlib

English

If φ is a Frobenius endomorphism at Q, then the comap of Q under φ is equal to Q itself when Q is prime; φ preserves Q precisely in the sense that φ^{-1}(Q) = Q.

Русский

Если φ — Фробениус-отображение по Q, то при Q простом обратное образование по φ совпадает с Q: φ^{-1}(Q) = Q.

LaTeX

$$$\operatorname{comap}_{φ}(Q) = Q$ for prime Q$$

Lean4

theorem comap_eq [Q.IsPrime] : Q.comap φ = Q :=
  by
  refine le_antisymm (fun x hx ↦ ?_) H.le_comap
  rwa [← Ideal.Quotient.eq_zero_iff_mem, ← H.restrict_injective.eq_iff, map_zero, restrict_mk,
    Ideal.Quotient.eq_zero_iff_mem, ← Ideal.mem_comap]

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