English
There is a natural equivalence between real embeddings and real infinite places given by mkReal.
Русский
Существует естественное эквивалентное соответствие между реальными вложениями и реальными бесконечными местами через mkReal.
LaTeX
$$mkReal : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : \\mathrm{InfinitePlace}(K) // IsReal w }$$
Lean4
/-- The map from real embeddings to real infinite places as an equiv -/
noncomputable def mkReal : { φ : K →+* ℂ // ComplexEmbedding.IsReal φ } ≃ { w : InfinitePlace K // IsReal w } :=
by
refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
· exact ⟨φ, φ.prop, rfl⟩
· rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self, ← Subtype.ext_iff] at h
· exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩
