Heights of points in projective space #
We define the multiplicative (Projectivization.mulHeight) and the logarithmic
(Projectivization.logHeight) height of a point in a (finite-dimensional) projective space
over a field that has a Height.AdmissibleAbsValues instance.
The height is defined to be the height of any representative tuple; it does not depend on which representative is chosen.
noncomputable def
Projectivization.mulHeight
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
The multiplicative height of a point on a finite-dimensional projective space over K
with a given basis.
Instances For
noncomputable def
Projectivization.logHeight
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
The logarithmic height of a point on a finite-dimensional projective space over K
with a given basis.
Instances For
theorem
Projectivization.mulHeight_mk
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
{x : ι → K}
(hx : x ≠ 0)
:
(mk K x hx).mulHeight = Height.mulHeight x
theorem
Projectivization.logHeight_mk
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
{x : ι → K}
(hx : x ≠ 0)
:
(mk K x hx).logHeight = Height.logHeight x
theorem
Projectivization.logHeight_eq_log_mulHeight
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
theorem
Projectivization.one_le_mulHeight
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
theorem
Projectivization.mulHeight_pos
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
theorem
Projectivization.mulHeight_ne_zero
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
x.mulHeight ≠ 0
theorem
Projectivization.logHeight_nonneg
{K : Type u_1}
[Field K]
[Height.AdmissibleAbsValues K]
{ι : Type u_2}
[Finite ι]
(x : Projectivization K (ι → K))
:
Extension for the positivity tactic: Projectivization.mulHeight is always positive.
Instances For
Extension for the positivity tactic: Projectivization.logHeight is always nonnegative.