Northcott Functions

In number theory, the height function h satisfies the Northcott property that the sets {a | h a ≤ b} are finite. This file extracts this notion as a typeclass and provides some API.

Main definitions

• Northcott h: A function h : α → β is Northcott if the sets {a : α | h a ≤ b} are all finite.

Main theorems

• Northcott.exists_min_image h s hs: If h is Northcott to a linear order, then h has an absolute minimum on every nonempty set s.

References

• D. Northcott, An inequality in the theory of arithmetic on algebraic varieties

class Northcott {α : Type u_1} {β : Type u_2} (h : α → β) [LE β] : Prop

A function h : α → β is Northcott if the sets {a : α | h a ≤ b} are all finite.

• finite_le (b : β) : {a : α | h a ≤ b}.Finite

theorem northcott_iff {α : Type u_1} {β : Type u_2} (h : α → β) [LE β] : Northcott h ↔ ∀ (b : β), {a : α | h a ≤ b}.Finite

theorem northcott_iff_tendsto {α : Type u_1} {β : Type u_2} (h : α → β) [LinearOrder β] [NoMaxOrder β] : Northcott h ↔ Filter.Tendsto h Filter.cofinite Filter.atTop

theorem Northcott.exists_min_image {α : Type u_1} {β : Type u_2} (h : α → β) [LinearOrder β] [Northcott h] (s : Set α) (hs : s.Nonempty) : ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'

theorem Northcott.comp_of_bddAbove {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [Preorder β] [LE γ] [Northcott h] (H : ∀ (c : γ), BddAbove (h' ⁻¹' {x : γ | x ≤ c})) : Northcott (h' ∘ h)

A composition h' ∘ h is Northcott when h is Northcott and preimages of bounded above sets under h' are bounded above.

theorem Northcott.comp_of_finite_fibers {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : α → β) (h' : β → γ) [LE γ] [Northcott h'] [Filter.TendstoCofinite h] : Northcott (h' ∘ h)

A composition h' ∘ h is Northcott when h' is Northcott and the fibers of h are finite.