NYLL
Module

FiniteTorsionPullback.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteTorsionPullback
4 declarations indexed from sourceView source ↗

Module documentation

Actual pullback on finite-coefficient direct-limit cohomology

The map is induced level by level by the derived cohomology inverse image. Compatibility with the original finite coefficient inclusions follows from coefficient naturality, independently of fundamental-group characters.

Imports3
Imported by2

Declarations

def

finiteTorsionStagePullback

L29 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionStagePullback
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (i : ℕ)
Lean source · statement
def finiteTorsionStagePullback (n : ℕ) :
    finiteTorsionLevel Y i n →+ finiteTorsionCohomology X i
theorem

finiteTorsionStagePullback_compatible

L34 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionStagePullback_compatible
Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (i : ℕ)
Lean source · statement
theorem finiteTorsionStagePullback_compatible (m n : ℕ) (h : m ≤ n)
    (a : finiteTorsionLevel Y i m) :
    finiteTorsionStagePullback f i m a =
      finiteTorsionStagePullback f i n (finiteTorsionTransition Y i m n h a)
def

finiteTorsionCohomologyPullback

L56 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionCohomologyPullback
Documentation

Inverse image on the direct limit of actual finite-coefficient cohomology.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (i : ℕ)
Lean source · full declaration
def finiteTorsionCohomologyPullback :
    finiteTorsionCohomology Y i →+ finiteTorsionCohomology X i where
  toFun := DirectLimit.lift (finiteTorsionTransition Y i)
    (fun n => finiteTorsionStagePullback f i n)
    (finiteTorsionStagePullback_compatible f i)
  map_zero' := DirectLimit.lift_zero (fun n => finiteTorsionStagePullback f i n)
    (finiteTorsionStagePullback_compatible f i)
  map_add' := DirectLimit.lift_add (fun n => finiteTorsionStagePullback f i n)
    (finiteTorsionStagePullback_compatible f i)
theorem

finiteTorsionCohomologyPullback_class

L67 ↗
EtaleFundamentalGroups.Cohomology.finiteTorsionCohomologyPullback_class
Documentation

On an original finite stage, this is exactly the derived cohomology pullback.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory EtaleCohomology.Classical
universe u
namespace EtaleFundamentalGroups.Cohomology
variable {X Y : Scheme.{u}} (f : X ⟶ Y) (i : ℕ)
Lean source · statement
theorem finiteTorsionCohomologyPullback_class (n : ℕ) (a : finiteTorsionLevel Y i n) :
    finiteTorsionCohomologyPullback f i (finiteTorsionClass Y i n a) =
      finiteTorsionClass X i n
        (constantCohomologyPullback f (finiteTorsionCoefficients n) i a)

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