@[reducible, inline]

abbrev PicardGroup.PicGrp (Div : Type u_1) [AddCommGroup Div] (PrincDiv : AddSubgroup Div) : Type u_1

def PicardGroup.toPic (Div : Type u_1) [AddCommGroup Div] (PrincDiv : AddSubgroup Div) : Div →+ PicGrp Div PrincDiv

def PicardGroup.LinearlyEquivalent (Div : Type u_1) [AddCommGroup Div] (PrincDiv : AddSubgroup Div) (D₁ D₂ : Div) : Prop

def PicardGroup.degPic {Div : Type u_1} [AddCommGroup Div] {PrincDiv : AddSubgroup Div} (deg : Div →+ ℤ) (hdeg : PrincDiv ≤ deg.ker) : PicGrp Div PrincDiv →+ ℤ

theorem PicardGroup.degPic_toPic {Div : Type u_1} [AddCommGroup Div] {PrincDiv : AddSubgroup Div} (deg : Div →+ ℤ) (hdeg : PrincDiv ≤ deg.ker) (D : Div) : (degPic deg hdeg) ((toPic Div PrincDiv) D) = deg D

def PicardGroup.Pic0 {Div : Type u_1} [AddCommGroup Div] {PrincDiv : AddSubgroup Div} (deg : Div →+ ℤ) (hdeg : PrincDiv ≤ deg.ker) : AddSubgroup (PicGrp Div PrincDiv)

theorem PicardGroup.mem_Pic0_iff {Div : Type u_1} [AddCommGroup Div] {PrincDiv : AddSubgroup Div} (deg : Div →+ ℤ) (hdeg : PrincDiv ≤ deg.ker) (x : PicGrp Div PrincDiv) : x ∈ Pic0 deg hdeg ↔ (degPic deg hdeg) x = 0

def CanonicalDivisors.IsMaximalDivisorFor {Div : Type u_2} {Ω : Type u_3} (omegaD : Ω → Div → Prop) [PartialOrder Div] (ω : Ω) (D : Div) : Prop

theorem CanonicalDivisors.exists_maximal_divisor_for_nonzero_differential {Div : Type u_2} {Ω : Type u_3} [Zero Ω] [SemilatticeSup Div] (omegaD : Ω → Div → Prop) (ω : Ω) (_hω : ω ≠ 0) (hex : ∃ (D : Div), omegaD ω D) (hfin : {D : Div | omegaD ω D}.Finite) (hsup : ∀ (D₁ D₂ : Div), omegaD ω D₁ → omegaD ω D₂ → omegaD ω (D₁ ⊔ D₂)) : ∃ (D : Div), omegaD ω D ∧ ∀ (D' : Div), omegaD ω D' → D' ≤ D

structure CanonicalDivisors.IsDivOmegaMaximal {Div : Type u_2} {Ω : Type u_3} (divΩ : Ω → Div) (omegaD : Ω → Div → Prop) [PartialOrder Div] (ω : Ω) : Prop

• mem : omegaD ω (divΩ ω)
• le_divΩ (D : Div) : omegaD ω D → D ≤ divΩ ω

def CanonicalDivisors.div_differential {Div : Type u_2} {Ω : Type u_3} (divΩ : Ω → Div) (ω : Ω) : Div

def CanonicalDivisors.IsCanonical {Div : Type u_2} {Ω : Type u_3} [Zero Ω] (divΩ : Ω → Div) (D : Div) : Prop

def CanonicalDivisors.ordOmega {Div : Type u_2} {Ω : Type u_3} {Place : Type u_4} (divΩ : Ω → Div) (ordP : Place → Div → ℤ) (P : Place) (ω : Ω) : ℤ

theorem CanonicalDivisors.div_smul_eq {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] {Ω : Type u_3} [Zero Ω] (divF : F → Div) (divΩ : Ω → Div) (smulΩ : F → Ω → Ω) (omegaD : Ω → Div → Prop) [PartialOrder Div] [CovariantClass Div Div (fun (x1 x2 : Div) => x1 + x2) fun (x1 x2 : Div) => x1 ≤ x2] (f : F) (hf : f ≠ 0) (ω : Ω) (_hω : ω ≠ 0) (hdivΩ_max : ∀ (ω' : Ω), ω' ≠ 0 → IsDivOmegaMaximal divΩ omegaD ω') (omegaD_smul : ∀ (g : F), g ≠ 0 → ∀ (ω' : Ω) (D : Div), omegaD ω' D → omegaD (smulΩ g ω') (divF g + D)) (smul_ne_zero : ∀ (g : F) (ω' : Ω), g ≠ 0 → ω' ≠ 0 → smulΩ g ω' ≠ 0) (divF_inv : ∀ (g : F), g ≠ 0 → divF g⁻¹ = -divF g) (smul_inv_cancel : ∀ (g : F) (ω' : Ω), g ≠ 0 → smulΩ g⁻¹ (smulΩ g ω') = ω') : divΩ (smulΩ f ω) = divF f + divΩ ω

def CanonicalDivisors.LinearlyEquivalent {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] (divF : F → Div) (D₁ D₂ : Div) : Prop

theorem CanonicalDivisors.canonical_linearlyEquivalent {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] {Ω : Type u_3} [Zero Ω] (divF : F → Div) (divΩ : Ω → Div) (smulΩ : F → Ω → Ω) (omega_one_dim : ∀ (ω₁ ω₂ : Ω), ω₁ ≠ 0 → ω₂ ≠ 0 → ∃ (f : F), f ≠ 0 ∧ ω₂ = smulΩ f ω₁) (div_smul_eq : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → divΩ (smulΩ f ω) = divF f + divΩ ω) {D₁ D₂ : Div} (h₁ : IsCanonical divΩ D₁) (h₂ : IsCanonical divΩ D₂) : LinearlyEquivalent divF D₁ D₂

theorem CanonicalDivisors.isCanonical_of_linearlyEquivalent {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] {Ω : Type u_3} [Zero Ω] (divF : F → Div) (divΩ : Ω → Div) (smulΩ : F → Ω → Ω) (div_smul_eq : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → divΩ (smulΩ f ω) = divF f + divΩ ω) (smul_ne_zero : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → smulΩ f ω ≠ 0) {D₁ D₂ : Div} (h₁ : IsCanonical divΩ D₁) (h₂ : LinearlyEquivalent divF D₁ D₂) : IsCanonical divΩ D₂

theorem CanonicalDivisors.canonical_divisors_form_single_class {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] {Ω : Type u_3} [Zero Ω] (divF : F → Div) (divΩ : Ω → Div) (smulΩ : F → Ω → Ω) (omega_one_dim : ∀ (ω₁ ω₂ : Ω), ω₁ ≠ 0 → ω₂ ≠ 0 → ∃ (f : F), f ≠ 0 ∧ ω₂ = smulΩ f ω₁) (div_smul_eq : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → divΩ (smulΩ f ω) = divF f + divΩ ω) (smul_ne_zero : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → smulΩ f ω ≠ 0) {D₁ D₂ : Div} (h₁ : IsCanonical divΩ D₁) : IsCanonical divΩ D₂ ↔ LinearlyEquivalent divF D₁ D₂

theorem CanonicalDivisors.cor_22_19_weil_diff_same_div {F : Type u_1} [Field F] {Div : Type u_2} [AddCommGroup Div] {Ω : Type u_3} [Zero Ω] (divF : F → Div) (divΩ : Ω → Div) (smulΩ : F → Ω → Ω) {k : Type u_5} [Field k] [Algebra k F] (omega_one_dim : ∀ (ω₁ ω₂ : Ω), ω₁ ≠ 0 → ω₂ ≠ 0 → ∃ (f : F), f ≠ 0 ∧ ω₂ = smulΩ f ω₁) (div_smul_eq : ∀ (f : F) (ω : Ω), f ≠ 0 → ω ≠ 0 → divΩ (smulΩ f ω) = divF f + divΩ ω) (divF_zero_iff_const : ∀ (f : F), f ≠ 0 → (divF f = 0 ↔ ∃ (c : k), c ≠ 0 ∧ (algebraMap k F) c = f)) (divF_const_zero : ∀ (c : k), c ≠ 0 → divF ((algebraMap k F) c) = 0) {ω₁ ω₂ : Ω} (hω₁ : ω₁ ≠ 0) (hω₂ : ω₂ ≠ 0) : divΩ ω₁ = divΩ ω₂ ↔ ∃ (c : k), c ≠ 0 ∧ ω₂ = smulΩ ((algebraMap k F) c) ω₁