Fundamental Cone

Let K be a number field of signature (r₁, r₂). We define an action of the units (𝓞 K)ˣ on the mixed space ℝ^r₁ × ℂ^r₂ via the mixedEmbedding. The fundamental cone is a cone in the mixed space that is a fundamental domain for the action of (𝓞 K)ˣ modulo torsion.

Main definitions and results

• NumberField.mixedEmbedding.unitSMul: the action of (𝓞 K)ˣ on the mixed space defined, for u : (𝓞 K)ˣ, by multiplication component by component with mixedEmbedding K u.

• NumberField.mixedEmbedding.fundamentalCone: a cone in the mixed space, ie. a subset stable 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_unit_smul_mem_of_mem.

• NumberField.mixedEmbedding.fundamentalCone.integralPoint: the subset of elements of the fundamental cone that are images of algebraic integers of K.

Tags

number field, canonical embedding, units, principal ideals

@[simp]

theorem NumberField.mixedEmbedding.unitSMul_smul (K : Type u_1) [Field K] (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K) : u • x = (NumberField.mixedEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) * x

instance NumberField.mixedEmbedding.unitSMul (K : Type u_1) [Field K] : SMul (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)

The action of (𝓞 K)ˣ on the mixed space ℝ^r₁ × ℂ^r₂ defined, for u : (𝓞 K)ˣ, by multiplication component by component with mixedEmbedding K u.

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.mixedEmbedding.instMulActionUnitsRingOfIntegersMixedSpace (K : Type u_1) [Field K] : MulAction (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)

Equations

• NumberField.mixedEmbedding.instMulActionUnitsRingOfIntegersMixedSpace K = MulAction.mk ⋯ ⋯

instance NumberField.mixedEmbedding.instSMulZeroClassUnitsRingOfIntegersMixedSpace (K : Type u_1) [Field K] : SMulZeroClass (NumberField.RingOfIntegers K)ˣ (NumberField.mixedEmbedding.mixedSpace K)

Equations

• NumberField.mixedEmbedding.instSMulZeroClassUnitsRingOfIntegersMixedSpace K = SMulZeroClass.mk ⋯

theorem NumberField.mixedEmbedding.unit_smul_eq_zero {K : Type u_1} [Field K] (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K) : u • x = 0 ↔ x = 0

theorem NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq {K : Type u_1} [Field K] [NumberField K] {x : NumberField.RingOfIntegers K} {y : NumberField.RingOfIntegers K} {u : (NumberField.RingOfIntegers K)ˣ} : u • (NumberField.mixedEmbedding K) ↑x = (NumberField.mixedEmbedding K) ↑y ↔ ↑u * x = y

theorem NumberField.mixedEmbedding.norm_unit_smul {K : Type u_1} [Field K] [NumberField K] (u : (NumberField.RingOfIntegers K)ˣ) (x : NumberField.mixedEmbedding.mixedSpace K) : NumberField.mixedEmbedding.norm (u • x) = NumberField.mixedEmbedding.norm x

def NumberField.mixedEmbedding.logMap {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℝ

The map from the mixed space to {w : InfinitePlace K // w ≠ w₀} → ℝ (with w₀ the fixed place from the proof of Dirichlet Unit Theorem) defined in such way that: 1) it factors the map logEmbedding, see logMap_eq_logEmbedding; 2) it is constant on the sets {c • x | c ∈ ℝ, c ≠ 0} if norm x ≠ 0, see logMap_real_smul.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.mixedEmbedding.logMap_apply {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) (w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : NumberField.mixedEmbedding.logMap x w = ↑(↑w).mult * (Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x) - Real.log (NumberField.mixedEmbedding.norm x) * (↑(FiniteDimensional.finrank ℚ K))⁻¹)

@[simp]

theorem NumberField.mixedEmbedding.logMap_zero {K : Type u_1} [Field K] [NumberField K] : NumberField.mixedEmbedding.logMap 0 = 0

@[simp]

theorem NumberField.mixedEmbedding.logMap_one {K : Type u_1} [Field K] [NumberField K] : NumberField.mixedEmbedding.logMap 1 = 0

theorem NumberField.mixedEmbedding.logMap_mul {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {y : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x ≠ 0) (hy : NumberField.mixedEmbedding.norm y ≠ 0) : NumberField.mixedEmbedding.logMap (x * y) = NumberField.mixedEmbedding.logMap x + NumberField.mixedEmbedding.logMap y

theorem NumberField.mixedEmbedding.logMap_apply_of_norm_one {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x = 1) (w : { w : NumberField.InfinitePlace K // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }) : NumberField.mixedEmbedding.logMap x w = ↑(↑w).mult * Real.log ((NumberField.mixedEmbedding.normAtPlace ↑w) x)

@[simp]

theorem NumberField.mixedEmbedding.logMap_eq_logEmbedding {K : Type u_1} [Field K] [NumberField K] (u : (NumberField.RingOfIntegers K)ˣ) : NumberField.mixedEmbedding.logMap ((NumberField.mixedEmbedding K) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) = (NumberField.Units.logEmbedding K) (Additive.ofMul u)

theorem NumberField.mixedEmbedding.logMap_unit_smul {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (u : (NumberField.RingOfIntegers K)ˣ) (hx : NumberField.mixedEmbedding.norm x ≠ 0) : NumberField.mixedEmbedding.logMap (u • x) = (NumberField.Units.logEmbedding K) (Additive.ofMul u) + NumberField.mixedEmbedding.logMap x

theorem NumberField.mixedEmbedding.logMap_torsion_smul {K : Type u_1} [Field K] [NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K) {ζ : (NumberField.RingOfIntegers K)ˣ} (hζ : ζ ∈ NumberField.Units.torsion K) : NumberField.mixedEmbedding.logMap (ζ • x) = NumberField.mixedEmbedding.logMap x

theorem NumberField.mixedEmbedding.logMap_real {K : Type u_1} [Field K] [NumberField K] (c : ℝ) : NumberField.mixedEmbedding.logMap (c • 1) = 0

theorem NumberField.mixedEmbedding.logMap_real_smul {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x ≠ 0) {c : ℝ} (hc : c ≠ 0) : NumberField.mixedEmbedding.logMap (c • x) = NumberField.mixedEmbedding.logMap x

theorem NumberField.mixedEmbedding.logMap_eq_of_normAtPlace_eq {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {y : NumberField.mixedEmbedding.mixedSpace K} (h : ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) x = (NumberField.mixedEmbedding.normAtPlace w) y) : NumberField.mixedEmbedding.logMap x = NumberField.mixedEmbedding.logMap y

def NumberField.mixedEmbedding.fundamentalCone (K : Type u_1) [Field K] [NumberField K] : Set (NumberField.mixedEmbedding.mixedSpace K)

The fundamental cone is a cone in the mixed space, ie. 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.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) : 0 < NumberField.mixedEmbedding.norm x

theorem NumberField.mixedEmbedding.fundamentalCone.normAtPlace_pos_of_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) (w : NumberField.InfinitePlace K) : 0 < (NumberField.mixedEmbedding.normAtPlace w) x

theorem NumberField.mixedEmbedding.fundamentalCone.mem_of_normAtPlace_eq {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {y : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) (hy : ∀ (w : NumberField.InfinitePlace K), (NumberField.mixedEmbedding.normAtPlace w) y = (NumberField.mixedEmbedding.normAtPlace w) x) : y ∈ NumberField.mixedEmbedding.fundamentalCone K

theorem NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {c : ℝ} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) (hc : c ≠ 0) : c • x ∈ NumberField.mixedEmbedding.fundamentalCone K

theorem NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {c : ℝ} (hc : c ≠ 0) : c • x ∈ NumberField.mixedEmbedding.fundamentalCone K ↔ x ∈ NumberField.mixedEmbedding.fundamentalCone K

theorem NumberField.mixedEmbedding.fundamentalCone.exists_unit_smul_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : NumberField.mixedEmbedding.norm x ≠ 0) : ∃ (u : (NumberField.RingOfIntegers K)ˣ), u • x ∈ NumberField.mixedEmbedding.fundamentalCone K

theorem NumberField.mixedEmbedding.fundamentalCone.torsion_smul_mem_of_mem {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) {ζ : (NumberField.RingOfIntegers K)ˣ} (hζ : ζ ∈ NumberField.Units.torsion K) : ζ • x ∈ NumberField.mixedEmbedding.fundamentalCone K

theorem NumberField.mixedEmbedding.fundamentalCone.unit_smul_mem_iff_mem_torsion {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone K) (u : (NumberField.RingOfIntegers K)ˣ) : u • x ∈ NumberField.mixedEmbedding.fundamentalCone K ↔ u ∈ NumberField.Units.torsion K

def NumberField.mixedEmbedding.fundamentalCone.integralPoint (K : Type u_1) [Field K] [NumberField K] : Set (NumberField.mixedEmbedding.mixedSpace K)

The set of images by mixedEmbedding of algebraic integers of K contained in the fundamental cone.

Equations

• NumberField.mixedEmbedding.fundamentalCone.integralPoint K = NumberField.mixedEmbedding.fundamentalCone K ∩ ↑(NumberField.mixedEmbedding.integerLattice K)

theorem NumberField.mixedEmbedding.fundamentalCone.mem_integralPoint {K : Type u_1} [Field K] [NumberField K] {a : NumberField.mixedEmbedding.mixedSpace K} : a ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K ↔ a ∈ NumberField.mixedEmbedding.fundamentalCone K ∧ ∃ (x : NumberField.RingOfIntegers K), (NumberField.mixedEmbedding K) ↑x = a

theorem NumberField.mixedEmbedding.fundamentalCone.exists_unique_preimage_of_integralPoint {K : Type u_1} [Field K] [NumberField K] {a : NumberField.mixedEmbedding.mixedSpace K} (ha : a ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K) : ∃! x : NumberField.RingOfIntegers K, (NumberField.mixedEmbedding K) ↑x = a

If a is an integral point, then there is a unique algebraic integer in 𝓞 K such that mixedEmbedding K x = a.

theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_ne_zero {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : ↑a ≠ 0

def NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : { x : NumberField.RingOfIntegers K // x ∈ nonZeroDivisors (NumberField.RingOfIntegers K) }

For a : integralPoint K, the unique nonzero algebraic integer whose image by mixedEmbedding is equal to a, see mixedEmbedding_preimageOfIntegralPoint.

Equations

• NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint a = ⟨⋯.choose, ⋯⟩

@[simp]

theorem NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfIntegralPoint {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : (NumberField.mixedEmbedding K) ↑↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint a) = ↑a

theorem NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint_mixedEmbedding {K : Type u_1} [Field K] [NumberField K] {x : { x : NumberField.RingOfIntegers K // x ∈ nonZeroDivisors (NumberField.RingOfIntegers K) }} (hx : (NumberField.mixedEmbedding K) ↑↑x ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K) : NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint ⟨(NumberField.mixedEmbedding K) ↑↑x, hx⟩ = x

theorem NumberField.mixedEmbedding.fundamentalCone.exists_unitSMul_mem_integralPoint {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} (hx : x ≠ 0) (hx' : x ∈ ⇑(NumberField.mixedEmbedding K) '' Set.range ⇑(algebraMap (NumberField.RingOfIntegers K) K)) : ∃ (u : (NumberField.RingOfIntegers K)ˣ), u • x ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K

If x : mixedSpace K is nonzero and the image of an algebraic integer, then there exists a unit such that u • x ∈ integralPoint K.

theorem NumberField.mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integralPoint {K : Type u_1} [Field K] [NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K} {ζ : (NumberField.RingOfIntegers K)ˣ} (hζ : ζ ∈ NumberField.Units.torsion K) (hx : x ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K) : ζ • x ∈ NumberField.mixedEmbedding.fundamentalCone.integralPoint K

The set integralPoint K is stable under the action of the torsion.

@[simp]

theorem NumberField.mixedEmbedding.fundamentalCone.integralPoint_torsionSMul_smul_coe {K : Type u_1} [Field K] [NumberField K] : ∀ (x : { x : (NumberField.RingOfIntegers K)ˣ // x ∈ NumberField.Units.torsion K }) (x_1 : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)), ↑(x • x_1) = ↑x • ↑x_1

instance NumberField.mixedEmbedding.fundamentalCone.integralPoint_torsionSMul {K : Type u_1} [Field K] [NumberField K] : SMul { x : (NumberField.RingOfIntegers K)ˣ // x ∈ NumberField.Units.torsion K } ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)

The action of torsion K on integralPoint K.

Equations

• One or more equations did not get rendered due to their size.

instance NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegralPoint {K : Type u_1} [Field K] [NumberField K] : MulAction { x : (NumberField.RingOfIntegers K)ˣ // x ∈ NumberField.Units.torsion K } ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)

Equations

• NumberField.mixedEmbedding.fundamentalCone.instMulActionSubtypeUnitsRingOfIntegersMemSubgroupTorsionElemMixedSpaceIntegralPoint = MulAction.mk ⋯ ⋯

def NumberField.mixedEmbedding.fundamentalCone.intNorm {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : ℕ

The mixedEmbedding.norm of a : integralPoint K as a natural number, see also intNorm_coe.

Equations

• NumberField.mixedEmbedding.fundamentalCone.intNorm a = ((Algebra.norm ℤ) ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfIntegralPoint a)).natAbs

@[simp]

theorem NumberField.mixedEmbedding.fundamentalCone.intNorm_coe {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : ↑(NumberField.mixedEmbedding.fundamentalCone.intNorm a) = NumberField.mixedEmbedding.norm ↑a

def NumberField.mixedEmbedding.fundamentalCone.quotIntNorm {K : Type u_1} [Field K] [NumberField K] : Quotient (MulAction.orbitRel { x : (NumberField.RingOfIntegers K)ˣ // x ∈ NumberField.Units.torsion K } ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) → ℕ

The norm intNorm lifts to a function on integralPoint K modulo torsion K.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply {K : Type u_1} [Field K] [NumberField K] (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integralPoint K)) : NumberField.mixedEmbedding.fundamentalCone.quotIntNorm ⟦a⟧ = NumberField.mixedEmbedding.fundamentalCone.intNorm a