le_comap — Mathlib

English

Let φ be a Frobenius endomorphism at Q. Then Q is contained in its preimage under φ, i.e., φ maps Q back into Q; equivalently, every element of Q is sent into Q by φ.

Русский

Пусть φ — это Фробениус-отображение в отношении Q. Тогда Q содержится в образе под обратным изображением φ, то есть φ отображает Q в Q; иными словами, каждый элемент Q переображается в Q.

LaTeX

$$$Q \subseteq \varphi^{-1}(Q)$$$

Lean4

theorem le_comap : Q ≤ Q.comap φ := by
  intro x hx
  simp_all only [Ideal.mem_comap, ← Ideal.Quotient.eq_zero_iff_mem (I := Q), H.mk_apply, zero_pow_eq, ite_eq_right_iff,
    H.card_pos.ne', false_implies]

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