English
The fundamental cone is the subset of the mixed space consisting of those x whose logMap lies in the fundamental domain of the norm-lattice, excluding points with zero norm.
Русский
Фундаментальный конус — это подмножество смешанного пространства, состоящее из тех точек x, для которых logMap(x) принадлежит фундаментальному домену нормированной решетки, за исключением точек с нулевой нормой.
LaTeX
$$$\text{fundamentalCone}(K) = \logMap^{-1}\bigl( ZSpan.fundamentalDomain((\text{basisUnitLattice}(K)).ofZLatticeBasis\,\mathbb{R}\,\_), \bigr) \setminus \{x\;|\; \text{mixedEmbedding.norm}(x)=0\}$$$
Lean4
/-- The fundamental cone is a cone in the mixed space, i.e. a subset fixed by multiplication by
a nonzero real number, see `smul_mem_of_mem`, that is also a fundamental domain for the action
of `(𝓞 K)ˣ` modulo torsion, see `exists_unit_smul_mem` and `torsion_smul_mem_of_mem`. -/
def fundamentalCone : Set (mixedSpace K) :=
logMap ⁻¹' (ZSpan.fundamentalDomain ((basisUnitLattice K).ofZLatticeBasis ℝ _)) \ {x | mixedEmbedding.norm x = 0}
