English
If two infinite places have the same comap along the base field, there exists a Galois automorphism σ with σ • w = w'.
Русский
Если две бесконечных места имеют одинаковое ограничение на осн. поле, существует Галуа-автоморфизм σ, такой что σ • w = w'.
LaTeX
$$$ \exists \sigma : K \simeq_k K, \; \sigma \cdot w = w' $$$
Lean4
theorem exists_smul_eq_of_comap_eq [IsGalois k K] {w w' : InfinitePlace K}
(h : w.comap (algebraMap k K) = w'.comap (algebraMap k K)) : ∃ σ : K ≃ₐ[k] K, σ • w = w' :=
by
rw [← mk_embedding w, ← mk_embedding w', comap_mk, comap_mk, mk_eq_iff] at h
cases h with
| inl h =>
obtain ⟨σ, hσ⟩ := ComplexEmbedding.exists_comp_symm_eq_of_comp_eq w.embedding w'.embedding h
use σ
rw [← mk_embedding w, ← mk_embedding w', smul_mk, hσ]
| inr
h =>
obtain ⟨σ, hσ⟩ :=
ComplexEmbedding.exists_comp_symm_eq_of_comp_eq ((starRingEnd ℂ).comp (embedding w)) w'.embedding h
use σ
rw [← mk_embedding w, ← mk_embedding w', smul_mk, mk_eq_iff]
exact Or.inr hσ
