The finite levels are the existing derived cohomology of the constant ℤ/ℓ^(n+1)ℤ sheaves on the small étale site. Coefficient reduction gives the transition maps. Classical integral ℓ-adic cohomology is the group of compatible families, that is, the inverse limit of these actual finite-level groups.
This construction uses no pro-étale site. It does not identify an inverse limit of cohomology groups with the cohomology of a derived inverse limit; any such comparison needs its own hypotheses and proof.
The finite cyclic coefficient group, lifted to the scheme universe.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalabbrev ellPowerCoefficients (ℓ n : ℕ) : AddCommGrpCat.{u}Reduction between consecutive finite coefficient groups.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef ellPowerReduction (ℓ n : ℕ) :
ellPowerCoefficients.{u} ℓ (n + 1) →+ ellPowerCoefficients.{u} ℓ n where
toFun a := ULift.up
(ZMod.castHom (pow_dvd_pow ℓ (Nat.le_succ (n + 1))) (ZMod (ℓ ^ (n + 1))) a.down)
map_zero' := congrArg ULift.up (map_zero _)
map_add' a b := congrArg ULift.up (map_add _ a.down b.down)Ordinary étale cohomology with finite cyclic constant coefficients, bundled with its original additive-group structure once at each level.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteLevelCohomology (X : Scheme.{u}) (ℓ n i : ℕ) : AddCommGrpCat.{u}The cohomological transition is induced by actual coefficient reduction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteLevelReduction (X : Scheme.{u}) (ℓ n i : ℕ) :
finiteLevelCohomology X ℓ (n + 1) i →+ finiteLevelCohomology X ℓ n iThe inverse limit subgroup of the finite-level cohomology groups.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef compatibleCohomology (X : Scheme.{u}) (ℓ i : ℕ) :
AddSubgroup (∀ n : ℕ, finiteLevelCohomology X ℓ n i)Classical integral ℓ-adic cohomology: the inverse limit of ordinary étale cohomology with coefficients ℤ/ℓ^(n+1)ℤ. No geometric finiteness hypothesis is imposed merely to define this group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalabbrev ellAdicCohomology (X : Scheme.{u}) (ℓ : ℕ) [Fact ℓ.Prime] (i : ℕ) : Type uEvaluation at a finite level is an additive homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef ellAdicProjection (X : Scheme.{u}) (ℓ : ℕ) [Fact ℓ.Prime] (i n : ℕ) :
ellAdicCohomology X ℓ i →+ finiteLevelCohomology X ℓ n iFinite-level projections satisfy the original cohomological transitions.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaltheorem ellAdicProjection_compatible (X : Scheme.{u}) (ℓ : ℕ) [Fact ℓ.Prime]
(i n : ℕ) (a : ellAdicCohomology X ℓ i) :
finiteLevelReduction X ℓ n i (ellAdicProjection X ℓ i (n + 1) a) =
ellAdicProjection X ℓ i n aEquality in classical ℓ-adic cohomology is detected at every finite level.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaltheorem ellAdicCohomology_ext (X : Scheme.{u}) (ℓ : ℕ) [Fact ℓ.Prime]
(i : ℕ) {a b : ellAdicCohomology X ℓ i}
(h : ∀ n, ellAdicProjection X ℓ i n a = ellAdicProjection X ℓ i n b) : a = b