English
The set image of normLeOne under normAtAllPlaces has a description as an intersection of a log-map preimage of a fundamental domain and simple positivity/norm conditions: logAtAllPlaces( normLeOne ) equals a specific intersection involving logMap and norm constraints.
Русский
Образ normLeOne под normAtAllPlaces описывается как пересечение предобразной области logMap фундаментальной области и простых условий неотрицательности и нормы.
LaTeX
$$$\\operatorname{normAtAllPlaces}''(\\operatorname{normLeOne} K) = \\bigl( \\operatorname{mixedSpaceOfRealSpace}^{-1} (\\logMap^{-1}(ZSpan.fundamentalDomain (\\cdots )))\\bigr) \\cap \\{x : \\forall w, x_w \\ge 0\\} \\cap \\{x : \\operatorname{mixedEmbedding.norm}(\\mathrm{mixedSpaceOfRealSpace} x) \\neq 0\\} \\cap \\{x : \\operatorname{mixedEmbedding.norm}(\\mathrm{mixedSpaceOfRealSpace} x) \\le 1\\} $$$
Lean4
theorem normLeOne_eq_preimage_image : normLeOne K = normAtAllPlaces ⁻¹' (normAtAllPlaces '' (normLeOne K)) :=
by
refine subset_antisymm (Set.subset_preimage_image _ _) ?_
rintro x ⟨y, hy₁, hy₂⟩
rw [mem_normLeOne, ← normAtAllPlaces_mem_fundamentalCone_iff, ← norm_normAtAllPlaces, ← mem_normLeOne] at hy₁ ⊢
rwa [← hy₂]
