Height one and finite multiplicative order

In a field satisfying Northcott's property, an element of multiplicative height one is zero or has finite multiplicative order: its powers all belong to one finite height sublevel set. Applied in the number field generated by an algebraic element, this proves Kronecker's criterion for absolute height one. The logarithmic forms characterize height zero. Off zero and the elements of finite order, the absolute height is therefore strictly greater than one.

The absolute criteria require algebraicity, since the absolute height is totalized on arbitrary elements of characteristic-zero fields.

See Bombieri and Gubler, Heights in Diophantine Geometry (2006), §1.5.9.

theorem Height.mulHeight₁_eq_one_of_isOfFinOrder {K : Type u_1} [Field K] [AdmissibleAbsValues K] {x : K} (hx : IsOfFinOrder x) : mulHeight₁ x = 1

An element of finite multiplicative order has multiplicative height one.

theorem Height.mulHeight₁_eq_one_iff {K : Type u_1} [Field K] [AdmissibleAbsValues K] [Northcott mulHeight₁] (x : K) : mulHeight₁ x = 1 ↔ x = 0 ∨ IsOfFinOrder x

Under Northcott's property, height one characterizes zero and elements of finite multiplicative order.

theorem Height.logHeight₁_eq_zero_iff {K : Type u_1} [Field K] [AdmissibleAbsValues K] [Northcott mulHeight₁] (x : K) : logHeight₁ x = 0 ↔ x = 0 ∨ IsOfFinOrder x

Under Northcott's property, logarithmic height zero characterizes zero and elements of finite multiplicative order.

theorem NumberField.one_le_absMulHeight₁ {F : Type u_1} [Field F] [CharZero F] (x : F) : 1 ≤ absMulHeight₁ x

The absolute multiplicative height is at least one, including its totalized value on nonalgebraic elements.

theorem NumberField.zero_le_absLogHeight₁ {F : Type u_1} [Field F] [CharZero F] (x : F) : 0 ≤ absLogHeight₁ x

The absolute logarithmic height is nonnegative.

theorem NumberField.absMulHeight₁_eq_one_iff {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℚ x) : absMulHeight₁ x = 1 ↔ x = 0 ∨ IsOfFinOrder x

Kronecker's criterion: an algebraic element has absolute multiplicative height one exactly when it is zero or has finite multiplicative order.

theorem NumberField.absLogHeight₁_eq_zero_iff {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℚ x) : absLogHeight₁ x = 0 ↔ x = 0 ∨ IsOfFinOrder x

Kronecker's criterion in logarithmic form for an algebraic element.

theorem NumberField.one_lt_absMulHeight₁ {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℚ x) (h0 : x ≠ 0) (hfin : ¬IsOfFinOrder x) : 1 < absMulHeight₁ x

An algebraic number that is neither zero nor of finite multiplicative order has absolute height strictly greater than one.

theorem NumberField.absLogHeight₁_pos {F : Type u_1} [Field F] [CharZero F] {x : F} (hx : IsIntegral ℚ x) (h0 : x ≠ 0) (hfin : ¬IsOfFinOrder x) : 0 < absLogHeight₁ x

An algebraic number that is neither zero nor of finite multiplicative order has positive absolute logarithmic height.