noncomputable def CohomologyAxiomsElimination.h1_O_defined (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : ℕ

Concrete definition of h^1(O) for an affine curve Spec A over k: the k-dimension of the Kähler differentials Ω_{A/k}.

theorem CohomologyAxiomsElimination.h1_O_defined_eq_genus (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [Algebra k A] : h1_O_defined k A = Module.finrank k Ω[A⁄k]

Unfolds h1_O_defined to its definition as finrank Ω_{A/k}.

theorem CohomologyAxiomsElimination.h1_O_defined_eq_h1_O (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : h1_O_defined k A = DedekindCurve.h1_O k A

On a Dedekind curve, the elimination definition of h^1(O) agrees with the official one.

def CohomologyAxiomsElimination.h1_sky_defined (_k : Type u_1) [Field _k] (_A : Type u_2) : ℕ

Concrete definition of h^1(skyscraper): zero, since the cohomology of a skyscraper sheaf vanishes in positive degree.

theorem CohomologyAxiomsElimination.h1_sky_defined_eq_zero (k : Type u_1) [Field k] (A : Type u_2) : h1_sky_defined k A = 0

h1_sky_defined is definitionally zero.

theorem CohomologyAxiomsElimination.h1_sky_defined_eq_h1_sky (k : Type u_1) [Field k] (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Algebra k A] [Module.Finite k A] : h1_sky_defined k A = DedekindCurve.h1_sky k A

On a Dedekind curve, the elimination definition of h^1(skyscraper) agrees with the official one.

noncomputable def CohomologyAxiomsElimination.h1_O_sheafH (k : Type u_1) [Field k] (R : CommRingCat) [Module k (ZariskiSheafCohomology.sheafCohomology (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) 1)] : ℕ

The h^1(O) of the affine spectrum Spec R, computed from the abstract sheaf cohomology.

noncomputable def CohomologyAxiomsElimination.h0_O_sheafH (k : Type u_1) [Field k] (R : CommRingCat) [Module k (ZariskiSheafCohomology.sheafCohomology (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) 0)] : ℕ

The h^0(O) of the affine spectrum Spec R, computed from the abstract sheaf cohomology.

noncomputable def CohomologyAxiomsElimination.groundedCohChi {k : Type u_1} [Field k] (C : DedekindCurve k) : ℤ × ℤ →+ ℤ

The "grounded" Euler characteristic homomorphism ℤ × ℤ → ℤ for a Dedekind curve, built from the concrete h1_O_defined and h1_sky_defined values.

theorem CohomologyAxiomsElimination.groundedCohChi_struct {k : Type u_1} [Field k] (C : DedekindCurve k) : (groundedCohChi C) (1, 0) = 1 - ↑C.ddGenus

groundedCohChi C (1, 0) = 1 - g, recovering the structure sheaf contribution.

theorem CohomologyAxiomsElimination.groundedCohChi_sky {k : Type u_1} [Field k] (C : DedekindCurve k) : (groundedCohChi C) (0, 1) = 1

groundedCohChi C (0, 1) = 1, the skyscraper contribution.

theorem CohomologyAxiomsElimination.groundedCohChi_eq_cohChi {k : Type u_1} [Field k] (C : DedekindCurve k) : groundedCohChi C = C.cohChi

The grounded Euler characteristic agrees with the official one on a Dedekind curve.

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

H^0 agrees with global sections (alias).

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

Global sections of O_{Spec R} are R (alias).