orbit_eq_primesOver — Mathlib

English

The G-action orbit of a prime Q over P equals the primes over P in B.

Русский

Орбитa действия G над Q совпадает с множеством простых идеалов над P.

LaTeX

$$$\mathrm{orbit}_G(Q) = P^{\ primesOver\ B}$$$

Lean4

theorem orbit_eq_primesOver [Finite G] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [hP : Q.LiesOver P]
    [hQ : Q.IsPrime] : MulAction.orbit G Q = P.primesOver B :=
  by
  refine Set.ext fun R ↦ ⟨fun ⟨g, hg⟩ ↦ hg ▸ ⟨hQ.smul g, hP.smul g⟩, fun h ↦ ?_⟩
  have : R.IsPrime := h.1
  obtain ⟨g, hg⟩ := exists_smul_of_under_eq A B G Q R (hP.over.symm.trans h.2.over)
  exact ⟨g, hg.symm⟩

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