mem_orbit_iff — Mathlib

English

An infinite place w' lies in the orbit of w under the Galois group iff their restrictions to the base field coincide.

Русский

Бесконечное место w' принадлежит орбите w под действием Галуа тогда и только тогда, когда их ограничения на осн. поле совпадают.

LaTeX

$$$ w' \in \mathrm{orbit}(K \simeq_k K) w \iff w.\mathrm{comap}(\mathrm{algebraMap}_{kK}) = w'.\mathrm{comap}(\mathrm{algebraMap}_{kK}) $$$

Lean4

theorem mem_orbit_iff [IsGalois k K] {w w' : InfinitePlace K} :
    w' ∈ MulAction.orbit (K ≃ₐ[k] K) w ↔ w.comap (algebraMap k K) = w'.comap (algebraMap k K) :=
  by
  refine ⟨?_, exists_smul_eq_of_comap_eq⟩
  rintro ⟨σ, rfl : σ • w = w'⟩
  rw [← mk_embedding w, comap_mk, smul_mk, comap_mk]
  congr 1; ext1; simp

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