ℓ-adic cohomology of a scheme

Let X be a scheme and ℓ be a prime number. In this file we define the sheaf associated to the topological group ℤ_[ℓ] on the pro-étale site of X. Its cohomology groups are the ℓ-adic cohomology groups of X.

Main declarations

• AlgebraicGeometry.Scheme.ellAdicSheaf: The sheaf U ↦ C(U, ℤ_[ℓ]).
• AlgebraicGeometry.Scheme.EllAdicCohomology: The pro-étale cohomology groups Hⁱ(X, ℤ_[ℓ]).

Notes

The ℓ-adic cohomology groups of X : Scheme.{u} are in Type (u + 1), because the pro-étale site of X has no essentially small subcategory with the same category of sheaves. Eventually, we will be able to compare the ℓ-adic cohomology defined here with the classical definition using étale cohomology. This will show that the groups defined here are indeed u-small.

References

• Bhatt, Bhargav and Scholze, Peter, The pro-étale topology for schemes

instance AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb (X : Scheme) : CategoryTheory.IsGrothendieckAbelian.{u + 1, u + 1, u + 2} (CategoryTheory.Sheaf (ProEt.topology X) Ab)

noncomputable def AlgebraicGeometry.Scheme.ellAdicSheaf (X : Scheme) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : CategoryTheory.Sheaf (ProEt.topology X) Ab

The sheaf of continuous maps U ↦ C(U, ℤ_[ℓ]) on the pro-étale site. This the coefficient sheaf for ℓ-adic cohomology. Definition 6.8.1.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty (X : Scheme) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] [IsEmpty ↥X] : CategoryTheory.Limits.IsZero (X.ellAdicSheaf ℓ)

def AlgebraicGeometry.Scheme.EllAdicCohomology (X : Scheme) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (n : ℕ) : Type (u + 1)

ℓ-adic cohomology of a scheme in degree n.

Equations

• X.EllAdicCohomology ℓ n = ((CategoryTheory.sheafCompose (AlgebraicGeometry.Scheme.ProEt.topology X) AddCommGrpCat.uliftFunctor).obj (X.ellAdicSheaf ℓ)).H n

@[implicit_reducible]

noncomputable instance AlgebraicGeometry.Scheme.instAddCommGroupEllAdicCohomology (X : Scheme) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (n : ℕ) : AddCommGroup (X.EllAdicCohomology ℓ n)

Equations

• One or more equations did not get rendered due to their size.

instance AlgebraicGeometry.Scheme.instSubsingletonEllAdicCohomologyOfIsEmptyCarrierCarrierCommRingCat (X : Scheme) (ℓ : ℕ) [Fact (Nat.Prime ℓ)] [IsEmpty ↥X] (n : ℕ) : Subsingleton (X.EllAdicCohomology ℓ n)

ℓ-adic cohomology is trivial for the empty scheme.