NYLL
Module

RationalAdic.lean

Nyll.EtaleCohomology.Classical.RationalAdic
7 declarations indexed from sourceView source ↗

Module documentation

Rational classical ℓ-adic cohomology

The actual finite coefficients carry the action of ℤ_[ℓ] by reduction. This induces actions on their ordinary étale cohomology groups. The transition maps are linear, so the inverse limit carries the same scalar action. Rational coefficients are then obtained by tensoring with ℚ_[ℓ] over ℤ_[ℓ].

This is the classical inverse-limit and scalar-extension construction, not cohomology of a discrete constant ℚ_[ℓ] sheaf or of a pro-étale site. See Stacks Project, Section 64.18, https://stacks.math.columbia.edu/tag/03UL.

Imports6
Imported by2

Declarations

def

linearSequentialLimit

L35 ↗
EtaleCohomology.Classical.linearSequentialLimit
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
Lean source · full declaration
def linearSequentialLimit (R : Type*) [Semiring R]
    (M : ℕ → Type u) [∀ n, AddCommGroup (M n)] [∀ n, Module R (M n)]
    (r : ∀ n, M (n + 1) →ₗ[R] M n) : Submodule R (∀ n, M n) where
  carrier := {a | ∀ n, r n (a (n + 1)) = a n}
  zero_mem' := fun n => map_zero (r n)
  add_mem' ha hb n := (map_add (r n) _ _).trans (congrArg₂ (· + ·) (ha n) (hb n))
  smul_mem' c _ ha n := (map_smul (r n) c _).trans (congrArg (c • ·) (ha n))
abbrev

ellPowerPadicModule

L47 ↗
EtaleCohomology.Classical.ellPowerPadicModule
Documentation

Finite coefficients retain the scalar action given by the actual reduction map from the ℓ-adic integers.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
abbrev ellPowerPadicModule (n : ℕ) : Module ℤ_[ℓ] (ellPowerCoefficients.{u} ℓ n)
theorem

ellPowerReduction_smul

L50 ↗
EtaleCohomology.Classical.ellPowerReduction_smul
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · full declaration
theorem ellPowerReduction_smul (n : ℕ) (c : ℤ_[ℓ])
    (a : ellPowerCoefficients.{u} ℓ (n + 1)) :
    let : Module ℤ_[ℓ] (ellPowerCoefficients.{u} ℓ (n + 1)) := ellPowerPadicModule ℓ (n + 1)
    let : Module ℤ_[ℓ] (ellPowerCoefficients.{u} ℓ n) := ellPowerPadicModule ℓ n
    ellPowerReduction ℓ n (c • a) = c • ellPowerReduction ℓ n a := by
  change ULift.up ((ZMod.castHom (pow_dvd_pow ℓ (Nat.le_succ (n + 1)))
      (ZMod (ℓ ^ (n + 1)))) (PadicInt.toZModPow (n + 2) c * a.down)) =
    ULift.up (PadicInt.toZModPow (n + 1) c * (ellPowerReduction ℓ n a).down)
  apply congrArg ULift.up
  rw [map_mul]
  exact congrArg (fun b => b * (ellPowerReduction ℓ n a).down)
    (congrArg (fun f : ℤ_[ℓ] →+* ZMod (ℓ ^ (n + 1)) => f c)
      (PadicInt.zmod_cast_comp_toZModPow (n + 1) (n + 2) (Nat.le_succ (n + 1))))
instance

finiteLevelPadicModule

L65 ↗
EtaleCohomology.Classical.finiteLevelPadicModule
Documentation

The coefficient action on the actual finite-level derived étale cohomology.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
instance finiteLevelPadicModule (X : Scheme.{u}) (n i : ℕ) :
    Module ℤ_[ℓ] (finiteLevelCohomology X ℓ n i)
def

finiteLevelReductionLinear

L73 ↗
EtaleCohomology.Classical.finiteLevelReductionLinear
Documentation

The original finite-level transition is linear over the ℓ-adic integers.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · full declaration
def finiteLevelReductionLinear (X : Scheme.{u}) (n i : ℕ) :
    finiteLevelCohomology X ℓ (n + 1) i →ₗ[ℤ_[ℓ]] finiteLevelCohomology X ℓ n i where
  toAddHom := finiteLevelReduction X ℓ n i
  map_smul' c a := by
    let : Module ℤ_[ℓ] (ellPowerCoefficients.{u} ℓ (n + 1)) := ellPowerPadicModule ℓ (n + 1)
    let : Module ℤ_[ℓ] (ellPowerCoefficients.{u} ℓ n) := ellPowerPadicModule ℓ n
    exact additiveCoefficient_map_smul
      (constantSheaf X.smallEtaleTopology AddCommGrpCat.{u} ⋙
        Sheaf.functorH X.smallEtaleTopology i) ℤ_[ℓ]
      (ellPowerCoefficients ℓ (n + 1)) (ellPowerCoefficients ℓ n)
      (AddCommGrpCat.ofHom (ellPowerReduction ℓ n)) (ellPowerReduction_smul ℓ n) c a
instance

ellAdicModule

L86 ↗
EtaleCohomology.Classical.ellAdicModule
Documentation

The inverse limit carries the scalar action induced at every finite level.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
instance ellAdicModule (X : Scheme.{u}) (i : ℕ) :
    Module ℤ_[ℓ] (ellAdicCohomology X ℓ i)
def

rationalEllAdicCohomology

L94 ↗
EtaleCohomology.Classical.rationalEllAdicCohomology
Documentation

Classical rational ℓ-adic cohomology, obtained from the integral inverse limit by scalar extension to the field of ℓ-adic numbers.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classical
variable (ℓ : ℕ) [Fact ℓ.Prime]
Lean source · statement
def rationalEllAdicCohomology (X : Scheme.{u}) (i : ℕ) : ModuleCat.{u} ℚ_[ℓ]

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.