Divisors on subsets of normed fields

This file defines divisors, a standard book-keeping tool in complex analysis used to keep track of pole/vanishing orders of meromorphic objects, typically functions or differential forms. It provides supporting API and establishes divisors as an instance of a lattice ordered commutative group.

Throughout the present file, 𝕜 denotes a nontrivially normed field, and U a subset of 𝕜.

TODOs

• Constructions: The divisor of a meromorphic function, behavior under product of meromorphic functions, behavior under addition, behavior under restriction
• Construction: The divisor of a rational polynomial

Definition, coercion to functions and basic extensionality lemmas

A divisor on U is a function 𝕜 → ℤ whose support is discrete within U and entirely contained within U. The theorem supportDiscreteWithin_iff_locallyFiniteWithin shows that this is equivalent to the textbook definition, which requires the support of f to be locally finite within U.

structure DivisorOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : Set 𝕜) : Type u_1

A divisor on U is a triple specified below.

• toFun : 𝕜 → ℤ

  A function 𝕜 → ℤ

• supportWithinDomain' : Function.support self.toFun ⊆ U

  A proof that the support of toFun is contained in U

• supportDiscreteWithinDomain' : self.toFun =ᶠ[Filter.codiscreteWithin U] 0

  A proof the the support is discrete within U

def Divisor (𝕜 : Type u_2) [NontriviallyNormedField 𝕜] : Type u_2

A divisor is a divisor on ⊤ : Set 𝕜.

Equations

• Divisor 𝕜 = DivisorOn ⊤

theorem supportDiscreteWithin_iff_locallyFiniteWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {f : 𝕜 → ℤ} (h : Function.support f ⊆ U) : f =ᶠ[Filter.codiscreteWithin U] 0 ↔ ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support f).Finite

The condition supportDiscreteWithinU in a divisor is equivalent to saying that the support is locally finite near every point of U.

instance DivisorOn.instFunLikeInt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : FunLike (DivisorOn U) 𝕜 ℤ

Divisors are FunLike: the coercion from divisors to functions is injective.

Equations

• DivisorOn.instFunLikeInt = { coe := fun (D : DivisorOn U) => D.toFun, coe_injective' := ⋯ }

@[reducible, inline]

abbrev DivisorOn.support {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : Set 𝕜

This allows writing D.support instead of Function.support D

Equations

• D.support = Function.support ⇑D

theorem DivisorOn.supportWithinDomain {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : D.support ⊆ U

theorem DivisorOn.supportDiscreteWithinDomain {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : ⇑D =ᶠ[Filter.codiscreteWithin U] 0

theorem DivisorOn.ext {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D₁ D₂ : DivisorOn U} (h : ∀ (a : 𝕜), D₁ a = D₂ a) : D₁ = D₂

theorem DivisorOn.coe_injective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Function.Injective fun (x : DivisorOn U) => ⇑x

Elementary properties of the support

@[simp]

theorem DivisorOn.apply_eq_zero_of_not_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜} (D : DivisorOn U) (hz : z ∉ U) : D z = 0

Simplifier lemma: A divisor on U evaluates to zero outside of U.

theorem DivisorOn.discreteSupport {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : DiscreteTopology ↑D.support

The support of a divisor is discrete.

theorem DivisorOn.closedSupport {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) (hU : IsClosed U) : IsClosed D.support

If U is closed, the the support of a divisor on U is also closed.

theorem DivisorOn.finiteSupport {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) (hU : IsCompact U) : D.support.Finite

If U is closed, the the support of a divisor on U is finite.

Lattice ordered group structure

This section equips divisors on U with the standard structure of a lattice ordered group, where addition, comparison, min and max of divisors are defined pointwise.

def DivisorOn.addSubgroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (U : Set 𝕜) : AddSubgroup (𝕜 → ℤ)

Divisors form an additive subgroup of functions 𝕜 → ℤ

Equations

• DivisorOn.addSubgroup U = { carrier := {f : 𝕜 → ℤ | Function.support f ⊆ U ∧ f =ᶠ[Filter.codiscreteWithin U] 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem DivisorOn.memAddSubgroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : ⇑D ∈ DivisorOn.addSubgroup U

def DivisorOn.mk_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (f : 𝕜 → ℤ) (hf : f ∈ DivisorOn.addSubgroup U) : DivisorOn U

Assign a divisor to a function in the subgroup

Equations

• DivisorOn.mk_of_mem f hf = { toFun := f, supportWithinDomain' := ⋯, supportDiscreteWithinDomain' := ⋯ }

@[simp]

theorem DivisorOn.mk_of_mem_toFun {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (f : 𝕜 → ℤ) (hf : f ∈ DivisorOn.addSubgroup U) (a✝ : 𝕜) : (mk_of_mem f hf) a✝ = f a✝

instance DivisorOn.instZero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Zero (DivisorOn U)

Equations

• DivisorOn.instZero = { zero := DivisorOn.mk_of_mem 0 ⋯ }

instance DivisorOn.instAdd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Add (DivisorOn U)

Equations

• DivisorOn.instAdd = { add := fun (D₁ D₂ : DivisorOn U) => DivisorOn.mk_of_mem (⇑D₁ + ⇑D₂) ⋯ }

instance DivisorOn.instNeg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Neg (DivisorOn U)

Equations

• DivisorOn.instNeg = { neg := fun (D : DivisorOn U) => DivisorOn.mk_of_mem (-⇑D) ⋯ }

instance DivisorOn.instSub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Sub (DivisorOn U)

Equations

• DivisorOn.instSub = { sub := fun (D₁ D₂ : DivisorOn U) => DivisorOn.mk_of_mem (⇑D₁ - ⇑D₂) ⋯ }

instance DivisorOn.instSMulNat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : SMul ℕ (DivisorOn U)

Equations

• DivisorOn.instSMulNat = { smul := fun (n : ℕ) (D : DivisorOn U) => DivisorOn.mk_of_mem (n • ⇑D) ⋯ }

instance DivisorOn.instSMulInt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : SMul ℤ (DivisorOn U)

Equations

• DivisorOn.instSMulInt = { smul := fun (n : ℤ) (D : DivisorOn U) => DivisorOn.mk_of_mem (n • ⇑D) ⋯ }

@[simp]

theorem DivisorOn.coe_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : ⇑0 = 0

@[simp]

theorem DivisorOn.coe_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D₁ D₂ : DivisorOn U) : ⇑(D₁ + D₂) = ⇑D₁ + ⇑D₂

@[simp]

theorem DivisorOn.coe_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) : ⇑(-D) = -⇑D

@[simp]

theorem DivisorOn.coe_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D₁ D₂ : DivisorOn U) : ⇑(D₁ - D₂) = ⇑D₁ - ⇑D₂

@[simp]

theorem DivisorOn.coe_nsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) (n : ℕ) : ⇑(n • D) = n • ⇑D

@[simp]

theorem DivisorOn.coe_zsmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} (D : DivisorOn U) (n : ℤ) : ⇑(n • D) = n • ⇑D

instance DivisorOn.instAddCommGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : AddCommGroup (DivisorOn U)

Equations

• DivisorOn.instAddCommGroup = Function.Injective.addCommGroup (fun (x : DivisorOn U) => ⇑x) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance DivisorOn.instLE {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : LE (DivisorOn U)

Equations

• DivisorOn.instLE = { le := fun (D₁ D₂ : DivisorOn U) => ⇑D₁ ≤ ⇑D₂ }

theorem DivisorOn.le_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D₁ D₂ : DivisorOn U} : D₁ ≤ D₂ ↔ ⇑D₁ ≤ ⇑D₂

instance DivisorOn.instLT {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : LT (DivisorOn U)

Equations

• DivisorOn.instLT = { lt := fun (D₁ D₂ : DivisorOn U) => ⇑D₁ < ⇑D₂ }

theorem DivisorOn.lt_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D₁ D₂ : DivisorOn U} : D₁ < D₂ ↔ ⇑D₁ < ⇑D₂

instance DivisorOn.instMax {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Max (DivisorOn U)

Equations

• DivisorOn.instMax = { max := fun (D₁ D₂ : DivisorOn U) => { toFun := fun (z : 𝕜) => D₁ z ⊔ D₂ z, supportWithinDomain' := ⋯, supportDiscreteWithinDomain' := ⋯ } }

@[simp]

theorem DivisorOn.max_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D₁ D₂ : DivisorOn U} {x : 𝕜} : (D₁ ⊔ D₂) x = D₁ x ⊔ D₂ x

instance DivisorOn.instMin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Min (DivisorOn U)

Equations

• DivisorOn.instMin = { min := fun (D₁ D₂ : DivisorOn U) => { toFun := fun (z : 𝕜) => D₁ z ⊓ D₂ z, supportWithinDomain' := ⋯, supportDiscreteWithinDomain' := ⋯ } }

@[simp]

theorem DivisorOn.min_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {D₁ D₂ : DivisorOn U} {x : 𝕜} : (D₁ ⊓ D₂) x = D₁ x ⊓ D₂ x

instance DivisorOn.instLattice {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : Lattice (DivisorOn U)

Equations

• DivisorOn.instLattice = Lattice.mk min ⋯ ⋯ ⋯

instance DivisorOn.instOrderedAddCommGroup {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U : Set 𝕜} : OrderedAddCommGroup (DivisorOn U)

Divisors form an ordered commutative group

Equations

• DivisorOn.instOrderedAddCommGroup = OrderedAddCommGroup.mk ⋯

Restriction

noncomputable def DivisorOn.restrict {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) : DivisorOn V

If V is a subset of U, then a divisor on U restricts to a divisor in V by setting its values to zero outside of V.

Equations

• D.restrict h = { toFun := fun (z : 𝕜) => if hz : z ∈ V then D z else 0, supportWithinDomain' := ⋯, supportDiscreteWithinDomain' := ⋯ }

theorem DivisorOn.restrict_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) (z : 𝕜) : (D.restrict h) z = if z ∈ V then D z else 0

theorem DivisorOn.restrict_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) (⇑D) V

theorem DivisorOn.restrict_eqOn_compl {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) : Set.EqOn (⇑(D.restrict h)) 0 Vᶜ

noncomputable def DivisorOn.restrictMonoidHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (h : V ⊆ U) : DivisorOn U →+ DivisorOn V

Restriction as a group morphism

Equations

• DivisorOn.restrictMonoidHom h = { toFun := fun (D : DivisorOn U) => D.restrict h, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem DivisorOn.restrictMonoidHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) : (restrictMonoidHom h) D = D.restrict h

noncomputable def DivisorOn.restrictLatticeHom {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (h : V ⊆ U) : LatticeHom (DivisorOn U) (DivisorOn V)

Restriction as a lattice morphism

Equations

• DivisorOn.restrictLatticeHom h = { toFun := fun (D : DivisorOn U) => D.restrict h, map_sup' := ⋯, map_inf' := ⋯ }

@[simp]

theorem DivisorOn.restrictLatticeHom_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {U V : Set 𝕜} (D : DivisorOn U) (h : V ⊆ U) : (restrictLatticeHom h) D = D.restrict h