def Lemma22_15.addPlace {Place : Type u_1} [DecidableEq Place] (D : Place → ℤ) (P : Place) : Place → ℤ

Increment a divisor $D$ by one at the place $P$, leaving all other places unchanged.

@[simp]

theorem Lemma22_15.addPlace_self {Place : Type u_1} [DecidableEq Place] (D : Place → ℤ) (P : Place) : addPlace D P P = D P + 1

Value of addPlace D P at P itself: it equals $D(P) + 1$.

theorem Lemma22_15.addPlace_ne {Place : Type u_1} [DecidableEq Place] (D : Place → ℤ) (P Q : Place) (h : Q ≠ P) : addPlace D P Q = D Q

Value of addPlace D P at $Q \neq P$: it is unchanged, equal to $D(Q)$.

theorem Lemma22_15.le_addPlace {Place : Type u_1} [DecidableEq Place] (D : Place → ℤ) (P : Place) : D ≤ addPlace D P

The increment-at-P operation only enlarges a divisor pointwise: $D \le \mathrm{addPlace}\,D\,P$.

def Lemma22_15.IsMaximalDivisorFor {Place : Type u_1} {Ω : Type u_2} (omegaD : Ω → (Place → ℤ) → Prop) (ω : Ω) (D : Place → ℤ) : Prop

Abstract statement that the divisor $D$ is maximal for the relation omegaD ω · : $\omega$ is associated to $D$ and every other associated divisor $D'$ satisfies $D' \le D$. Used to formulate the unique divisor of a Weil differential (Lemma 22.15).

theorem Lemma22_15.exists_maximal_divisor {Place : Type u_1} [DecidableEq Place] {Ω : Type u_2} [Zero Ω] (omegaD : Ω → (Place → ℤ) → Prop) (adele_decomp : ∀ (ω : Ω) (D₁ D₂ : Place → ℤ) (P : Place), omegaD ω D₁ → omegaD ω D₂ → D₁ P < D₂ P → omegaD ω (addPlace D₁ P)) (ω : Ω) (_hω : ω ≠ 0) (hex : ∃ (D : Place → ℤ), omegaD ω D) (hfin : {D : Place → ℤ | omegaD ω D}.Finite) : ∃ (D : Place → ℤ), IsMaximalDivisorFor omegaD ω D

Existence half of Lemma 22.15. Under the "increment" closure hypothesis adele_decomp and finiteness of associated divisors, every nonzero $\omega$ admits a maximal divisor $D$ with omegaD ω D and $D' \le D$ for all associated $D'$.

theorem Lemma22_15.unique_maximal_divisor {Place : Type u_1} [DecidableEq Place] {Ω : Type u_2} [Zero Ω] (omegaD : Ω → (Place → ℤ) → Prop) (ω : Ω) {D₁ D₂ : Place → ℤ} (h₁ : IsMaximalDivisorFor omegaD ω D₁) (h₂ : IsMaximalDivisorFor omegaD ω D₂) : D₁ = D₂

Uniqueness half of Lemma 22.15. Any two maximal divisors for the same $\omega$ coincide.

theorem Lemma22_15.exists_unique_maximal_divisor {Place : Type u_1} [DecidableEq Place] {Ω : Type u_2} [Zero Ω] (omegaD : Ω → (Place → ℤ) → Prop) (adele_decomp : ∀ (ω : Ω) (D₁ D₂ : Place → ℤ) (P : Place), omegaD ω D₁ → omegaD ω D₂ → D₁ P < D₂ P → omegaD ω (addPlace D₁ P)) (ω : Ω) (hω : ω ≠ 0) (hex : ∃ (D : Place → ℤ), omegaD ω D) (hfin : {D : Place → ℤ | omegaD ω D}.Finite) : ∃! D : Place → ℤ, IsMaximalDivisorFor omegaD ω D

Lemma 22.15 (unique maximal divisor $D_\omega$ of a Weil differential). Combining existence and uniqueness: every nonzero $\omega$ has a unique divisor $D$ with IsMaximalDivisorFor omegaD ω D.