def uliftZHomEquiv (G : Type u_1) [AddCommGroup G] : (ULift.{u_2, 0} ℤ →+ G) ≃+ G

Additive equivalence between additive homomorphisms ULift ℤ →+ G and G, sending a hom to its value at 1.

def catUliftZHomEquiv (M : AddCommGrpCat) : (AddCommGrpCat.of (ULift.{0, 0} ℤ) ⟶ M) ≃ ↑M

Categorical version of uliftZHomEquiv: morphisms ULift ℤ ⟶ M in AddCommGrpCat correspond bijectively to elements of M.

noncomputable def h0EquivGlobalSections (X : AlgebraicGeometry.Scheme) : ZariskiSheafCohomology.sheafCohomology X 0 ≃ ↑(((CategoryTheory.sheafSections (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat).obj (Opposite.op ⊤)).obj (ZariskiSheafCohomology.schemeAbSheaf X))

Identification of the 0th sheaf cohomology of a scheme X with its group of global sections, via the composition of standard equivalences.

noncomputable def globalSections_Spec_iso (R : CommRingCat) : (AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤) ≅ R

The categorical isomorphism Γ(Spec R, ⊤) ≅ R between global sections of Spec R and the ring R.

noncomputable def globalSections_Spec_ringEquiv (R : CommRingCat) : ↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤)) ≃+* ↑R

The ring equivalence Γ(Spec R, ⊤) ≃+* R between global sections of Spec R and the ring R.

noncomputable def specGammaIdentity : AlgebraicGeometry.Scheme.Spec.rightOp.comp AlgebraicGeometry.Scheme.Γ ≅ CategoryTheory.Functor.id CommRingCat

The natural isomorphism Spec.rightOp ⋙ Γ ≅ 𝟭 CommRingCat expressing that Γ is left inverse to Spec.

theorem finrank_self_eq_one (k : Type u_1) [Field k] : Module.finrank k k = 1

A field k has dimension one as a vector space over itself.

def DedekindCurve.h0_O {k : Type u_1} [Field k] : DedekindCurve k → ℕ

For a Dedekind curve over a field k, the dimension h^0(O_C) = 1 of global sections of the structure sheaf.

theorem DedekindCurve.h0_O_eq_one {k : Type u_1} [Field k] (C : DedekindCurve k) : C.h0_O = 1

The value h^0(O_C) equals 1 for any Dedekind curve C.

theorem DedekindCurve.eulerCharO_from_h0_h1 {k : Type u_1} [Field k] (C : DedekindCurve k) : C.eulerCharO = ↑C.h0_O - ↑(h1_O k C.A)

Euler characteristic of the structure sheaf equals h^0(O_C) - h^1(O_C).

theorem DedekindCurve.cohChi_struct_decomp {k : Type u_1} [Field k] (C : DedekindCurve k) : C.cohChi (1, 0) = ↑C.h0_O - ↑(h1_O k C.A)

Decomposition: the cohomological Euler characteristic at (1, 0) agrees with h^0(O_C) - h^1(O_C).

theorem DedekindCurve.h0_plus_h1_eq {k : Type u_1} [Field k] (C : DedekindCurve k) : ↑C.h0_O + ↑(h1_O k C.A) = 1 + ↑C.ddGenus

For a Dedekind curve, h^0(O_C) + h^1(O_C) = 1 + g where g is the genus.

theorem DedekindCurve.eulerCharO_consistent {k : Type u_1} [Field k] (C : DedekindCurve k) : C.eulerCharO = ↑C.h0_O - ↑C.ddGenus

The Euler characteristic of the structure sheaf equals h^0(O_C) - g, consistent with 1 - g.