English
The mixed embedding of an element x coincides with composing the algebra map with the mixed space embedding.
Русский
Смешанное вложение элемента x совпадает с композицией алгебраической карты и вложения в смешанном пространстве.
LaTeX
$$$\\text{mixedEmbedding}(K)\\, x = \\text{ringEquiv\\_mixedSpace}(K)\\, (\\text{algebraMap } K \\ (\\text{InfiniteAdeleRing } K))\\, x$$$
Lean4
/-- The ring isomorphism between the infinite adele ring of a number field and the
space `ℝ ^ r₁ × ℂ ^ r₂`, where `(r₁, r₂)` is the signature of the number field. -/
abbrev ringEquiv_mixedSpace : InfiniteAdeleRing K ≃+* mixedEmbedding.mixedSpace K :=
RingEquiv.trans
(RingEquiv.piEquivPiSubtypeProd (fun (v : InfinitePlace K) => IsReal v) (fun (v : InfinitePlace K) => v.Completion))
(RingEquiv.prodCongr (RingEquiv.piCongrRight (fun ⟨_, hv⟩ => Completion.ringEquivRealOfIsReal hv))
(RingEquiv.trans
(RingEquiv.piCongrRight (fun v => Completion.ringEquivComplexOfIsComplex ((not_isReal_iff_isComplex.1 v.2))))
(RingEquiv.piCongrLeft (fun _ => ℂ) <| Equiv.subtypeEquivRight (fun _ => not_isReal_iff_isComplex))))
