@[implicit_reducible]

instance ZariskiSheafCohomology.opensOrderTop (T : Type u_1) [TopologicalSpace T] : OrderTop (TopologicalSpace.Opens T)

The lattice of open subsets of a topological space has a top element (the whole space).

@[reducible, inline]

abbrev ZariskiSheafCohomology.commRingToAddCommGrp : CategoryTheory.Functor CommRingCat AddCommGrpCat

Forgetful functor from commutative rings to additive abelian groups, factored through the category of rings.

noncomputable def ZariskiSheafCohomology.schemeAbSheaf (X : AlgebraicGeometry.Scheme) : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat

The structure sheaf of a scheme viewed as a sheaf of additive abelian groups on the Zariski site.

def ZariskiSheafCohomology.sheafCohomology (X : AlgebraicGeometry.Scheme) (n : ℕ) : Type

The n-th Zariski sheaf cohomology of the structure sheaf of X.

@[implicit_reducible]

noncomputable instance ZariskiSheafCohomology.sheafCohomology_addCommGroup (X : AlgebraicGeometry.Scheme) (n : ℕ) : AddCommGroup (sheafCohomology X n)

The sheaf cohomology groups inherit an additive abelian group structure.

def ZariskiSheafCohomology.specCohomology (R : CommRingCat) (n : ℕ) : Type

Specialization to affine schemes: the n-th Zariski cohomology of Spec R.

@[implicit_reducible]

noncomputable instance ZariskiSheafCohomology.specCohomology_addCommGroup (R : CommRingCat) (n : ℕ) : AddCommGroup (specCohomology R n)

The affine sheaf cohomology groups carry an additive abelian group structure.

noncomputable def ZariskiSheafCohomology.h0AddEquivHom (X : AlgebraicGeometry.Scheme) : sheafCohomology X 0 ≃+ ((CategoryTheory.constantSheaf (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{0, 0} ℤ)) ⟶ schemeAbSheaf X)

Degree-zero cohomology is identified with Hom-out of the constant sheaf on ℤ, via the Ext⁰ formalism.

noncomputable def ZariskiSheafCohomology.h0EquivSections (X : AlgebraicGeometry.Scheme) : ((CategoryTheory.constantSheaf (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{0, 0} ℤ)) ⟶ schemeAbSheaf X) ≃ (AddCommGrpCat.of (ULift.{0, 0} ℤ) ⟶ ((CategoryTheory.sheafSections (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat).obj (Opposite.op ⊤)).obj (schemeAbSheaf X))

Adjunction equivalence: morphisms from the constant sheaf on ℤ to a sheaf correspond to global sections of that sheaf.

noncomputable def ZariskiSheafCohomology.zariskiCohomologyFunctor (X : AlgebraicGeometry.Scheme) (n : ℕ) : CategoryTheory.Functor (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat) AddCommGrpCat

The functor F ↦ Hⁿ(X, F) taking a sheaf to its n-th Zariski sheaf cohomology.

instance ZariskiSheafCohomology.zariskiCohomologyFunctor_additive (X : AlgebraicGeometry.Scheme) (n : ℕ) : (zariskiCohomologyFunctor X n).Additive

The Zariski cohomology functor is additive in its sheaf argument.

theorem ZariskiSheafCohomology.subsingleton_cohomology_of_isZero (X : AlgebraicGeometry.Scheme) {F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X.toTopCat) AddCommGrpCat} (h : CategoryTheory.Limits.IsZero F) (n : ℕ) : Subsingleton (F.H n)

If F is the zero sheaf, then all of its sheaf cohomology groups are trivial.

noncomputable def ZariskiSheafCohomology.specH (k : Type u_1) [Field k] (X : AlgebraicGeometry.Scheme) (n : ℕ) [Module k (sheafCohomology X n)] : ℕ

The dimension hⁿ(X) = dim_k Hⁿ(X, O_X) of sheaf cohomology when the cohomology group carries a k-vector-space structure.