We use the finite constant groups of circle elements killed by (n+1)!. Their inclusions define a cofinal system of finite cyclic coefficients. The groups below are the direct limit of the actual derived étale cohomology groups. They are not defined using fundamental-group characters.
This definition does not assert that derived cohomology commutes with this direct limit for an arbitrary scheme. Such an identification with cohomology of the infinite constant torsion sheaf requires a separate comparison.
The finite subgroup of circle elements of order dividing (n+1)!.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef factorialRoots (n : ℕ) : Subgroup CircleSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalinstance (n : ℕ) : Finite (factorialRoots n)Factorial divisibility gives the inclusions of the finite coefficient subgroups.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaltheorem factorialRoots_mono {m n : ℕ} (h : m ≤ n) : factorialRoots m ≤ factorialRoots nConstant finite torsion coefficients in the same universe as the scheme.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalabbrev finiteTorsionCoefficients (n : ℕ) : AddCommGrpCat.{u}The actual inclusion between two finite coefficient groups.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteTorsionInclusion (m n : ℕ) (h : m ≤ n) :
finiteTorsionCoefficients.{u} m →+ finiteTorsionCoefficients.{u} n where
toFun a := ULift.up (Additive.ofMul
⟨a.down.toMul.val, factorialRoots_mono h a.down.toMul.property⟩)
map_zero' := rfl
map_add' _ _ := rflDerived small-étale cohomology with the actual finite constant coefficients.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteTorsionLevel (X : Scheme.{u}) (i n : ℕ) : AddCommGrpCat.{u}The transition maps are induced by inclusions of the original constant sheaves.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteTorsionTransition (X : Scheme.{u}) (i m n : ℕ) (h : m ≤ n) :
finiteTorsionLevel X i m →+ finiteTorsionLevel X i nSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalinstance (X : Scheme.{u}) (i : ℕ) :
DirectedSystem (fun n => finiteTorsionLevel X i n)
(fun {_ _} h => finiteTorsionTransition X i _ _ h) where
map_self := by
intro n a
have he : AddCommGrpCat.ofHom (finiteTorsionInclusion.{u} n n le_rfl) =
𝟙 (finiteTorsionCoefficients n) := AddCommGrpCat.hom_ext (AddMonoidHom.ext fun _ => rfl)
change Sheaf.H.map ((constantSheaf _ AddCommGrpCat.{u}).map _) i a = a
rw [he, CategoryTheory.Functor.map_id]
exact Sheaf.H.map_id_apply a
map_map := by
intro k n m hmn hnk a
have he : AddCommGrpCat.ofHom (finiteTorsionInclusion.{u} m k (hmn.trans hnk)) =
AddCommGrpCat.ofHom (finiteTorsionInclusion m n hmn) ≫
AddCommGrpCat.ofHom (finiteTorsionInclusion n k hnk) :=
AddCommGrpCat.hom_ext (AddMonoidHom.ext fun _ => rfl)
change Sheaf.H.map _ i (Sheaf.H.map _ i a) =
Sheaf.H.map ((constantSheaf _ AddCommGrpCat.{u}).map _) i a
rw [he, CategoryTheory.Functor.map_comp]
exact (Sheaf.H.map_comp_apply _ _ a).symmThe finite-coefficient direct limit of ordinary étale cohomology.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicalabbrev finiteTorsionCohomology (X : Scheme.{u}) (i : ℕ) : Type uA finite-level cohomology class defines a class in the direct limit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef directLimitInclusion (G : ℕ → Type u) [∀ n, AddCommGroup (G n)]
(f : ∀ m n, m ≤ n → G m →+ G n) [DirectedSystem G (f · · ·)] (n : ℕ) :
G n →+ DirectLimit G f where
toFun a := ⟦⟨n, a⟩⟧
map_zero' := (DirectLimit.zero_def n).symm
map_add' a b := (DirectLimit.add_def n a b).symmA finite-level cohomology class defines a class in the direct limit.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology.Classicaldef finiteTorsionClass (X : Scheme.{u}) (i n : ℕ) :
finiteTorsionLevel X i n →+ finiteTorsionCohomology X i