Divisors (CC2) and the divisor map divisor : ℳ X → Divisor X (CC3)

Unit: meromorphic-and-divisors (docs/design/meromorphic-and-divisors.md §4.6, D7, proof plan §6.3).

• Function.locallyFinsuppWithin.degree (Compat, upstreamable): the degree of a divisor on a compact T2Space, D.degree := ∑ x ∈ (D.finiteSupport isCompact_univ).toFinset, D x.
• RS.Divisor X := Function.locallyFinsuppWithin (Set.univ : Set X) ℤ (CC2, frozen).
• MeroGermOn.divisorOn φ : Function.locallyFinsuppWithin U ℤ, toFun x = (φ.ord x).untop₀; local finiteness (§6.3) via eventually_ordAtX_eq_top/eventually_ordAtX_eq_zero.
• divisor : ℳ X → Divisor X (CC3's div, renamed to avoid Div-notation collision): total, divisor 0 = 0 honestly (empty support, no case split). Algebra (divisor_mul/inv/smul), effectivity (divisor_nonneg_iff), compactness finiteness (finite_support_divisor, finite_setOf_ord_neg/pos, eventually_ord_eq_zero).

Compat: degree (upstreamable to Function.locallyFinsuppWithin)

noncomputable def Function.locallyFinsuppWithin.degree {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {Y : Type u_2} [AddCommMonoid Y] (D : locallyFinsuppWithin Set.univ Y) : Y

Degree of a divisor on a compact T2Space (CC2's deg; absent from mathlib at the pin).

Equations

• D.degree = ∑ x ∈ ⋯.toFinset, D x

theorem Function.locallyFinsuppWithin.degree_eq_sum_of_subset {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {Y : Type u_2} [AddCommMonoid Y] {D : locallyFinsuppWithin Set.univ Y} {S : Finset X} (hS : D.support ⊆ ↑S) : D.degree = ∑ x ∈ S, D x

@[simp]

theorem Function.locallyFinsuppWithin.degree_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {Y : Type u_2} [AddCommMonoid Y] : degree 0 = 0

theorem Function.locallyFinsuppWithin.degree_add {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {Y : Type u_2} [AddCommMonoid Y] (D E : locallyFinsuppWithin Set.univ Y) : (D + E).degree = D.degree + E.degree

theorem Function.locallyFinsuppWithin.degree_neg {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {Y : Type u_2} [AddCommGroup Y] (D : locallyFinsuppWithin Set.univ Y) : (-D).degree = -D.degree

theorem Function.locallyFinsuppWithin.degree_mono {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {D E : locallyFinsuppWithin Set.univ ℤ} (h : D ≤ E) : D.degree ≤ E.degree

theorem Function.locallyFinsuppWithin.degree_nonneg_of_nonneg {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {D : locallyFinsuppWithin Set.univ ℤ} (h : 0 ≤ D) : 0 ≤ D.degree

@[reducible, inline]

abbrev RS.Divisor (X : Type u_1) [TopologicalSpace X] : Type u_1

CC2 (frozen).

Equations

• RS.Divisor X = Function.locallyFinsuppWithin Set.univ ℤ

noncomputable def RS.MeroGermOn.divisorOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : MeroGermOn X U) : Function.locallyFinsuppWithin U ℤ

Relative divisor of a germ class (support automatically inside U by the D3 junk).

Equations

• φ.divisorOn = { toFun := fun (x : X) => (φ.ord x).untop₀, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }

@[simp]

theorem RS.MeroGermOn.divisorOn_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : MeroGermOn X U) (x : X) : φ.divisorOn x = (φ.ord x).untop₀

@[reducible, inline]

noncomputable abbrev RS.divisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Mero X) : Divisor X

CC3's div : ℳ X → Divisor X (renamed divisor; total, divisor 0 = 0 honestly).

Equations

• RS.divisor φ = RS.MeroGermOn.divisorOn φ

@[simp]

theorem RS.divisor_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Mero X) (x : X) : (divisor φ) x = (MeroGermOn.ord φ x).untop₀

@[simp]

theorem RS.divisor_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : divisor 0 = 0

theorem RS.divisor_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {φ ψ : Mero X} (hφ : φ ≠ 0) (hψ : ψ ≠ 0) : divisor (φ * ψ) = divisor φ + divisor ψ

theorem RS.divisor_inv {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Mero X) : divisor φ⁻¹ = -divisor φ

theorem RS.divisor_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {c : ℂ} [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {φ : Mero X} (hc : c ≠ 0) : divisor (c • φ) = divisor φ

theorem RS.divisor_algebraMap {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) : divisor ((algebraMap ℂ (Mero X)) c) = 0

theorem RS.min_divisor_le_divisor_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {φ ψ : Mero X} (h : φ + ψ ≠ 0) : divisor φ ⊓ divisor ψ ≤ divisor (φ + ψ)

theorem RS.divisor_nonneg_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {φ : Mero X} : 0 ≤ divisor φ ↔ ∀ (x : X), 0 ≤ MeroGermOn.ord φ x

theorem RS.finite_support_divisor {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] (φ : Mero X) : (Function.locallyFinsuppWithin.support (divisor φ)).Finite

theorem RS.finite_setOf_ord_neg {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {φ : Mero X} (h : φ ≠ 0) : {x : X | MeroGermOn.ord φ x < 0}.Finite

theorem RS.finite_setOf_ord_pos {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] {φ : Mero X} (h : φ ≠ 0) : {x : X | 0 < MeroGermOn.ord φ x}.Finite

theorem RS.eventually_ord_eq_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [T1Space X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] {φ : Mero X} (h : φ ≠ 0) (x : X) : ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, MeroGermOn.ord φ y = 0