64.3 Frobenii to 64.29 Cohomology of curves…

Section64.3 Frobenii#

Section 64.3 of the Stacks Project, Tag 03SL. 10 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03SO, an exercise

Tag 03SO in the Stacks Project.

cohomologyPullbackMap_eq_id_of_preimageEq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Pullback/IdOfPreimageEq.lean, line 99. The attribute's comment: “g induces the identity on cohomology, for any coefficients”.

Stacks tag 03SO. Let X be a topological space and g : X ⟶ X a continuous map such that g ⁻¹' U = U for every open U of X. Then the map g induces on sheaf cohomology, followed by the canonical comparison of the pullback sheaf with the original one, is the identity, in every degree n and for every abelian sheaf F: g induces the identity on cohomology, for any coefficients.

See Stacks Project, Tag 03SO.

theorem cohomologyPullbackMap_eq_id_of_preimageEq
    [HasExt.{w} (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u})]
    (F : Sheaf (Opens.grothendieckTopology X) AddCommGrpCat.{u}) (n : ℕ) :
    (Sheaf.H.map ((Adjunction.leftAdjointIdIso (sheafAdjunctionOpensMap g)
          (sheafPushforwardIdOfPreimageEq g h)).hom.app F) n).comp
        (Stacks.Cohomology.cohomologyPullbackMap.{w} (sheafAdjunctionOpensMap g)
          (sheafPushforwardIdOfPreimageEq g h) F n) =
      AddMonoidHom.id (Sheaf.H.{w} F n)
Tag 03SP, a lemma

Tag 03SP in the Stacks Project.

Stacks.EtaleCohomology.etaleCohomologyPullbackMap_comp_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/BafflingTheorem.lean, line 207. The attribute's comment: “g induces the identity on cohomology, for any sheaf”.

Stacks Project, Tag 03SP. Let X be a scheme and g : X ⟶ X a morphism such that every étale X-scheme U is isomorphic over X to its base change U ×_{g} X, functorially in U. Then g induces the identity on cohomology, for any abelian sheaf F and in every degree n: the map H^n(X, F) ⟶ H^n(X, g^{-1}F) induced by g, followed by the canonical comparison H^n(X, g^{-1}F) ≅ H^n(X, F), is the identity of H^n(X, F).

See Stacks Project, Tag 03SP.

public theorem etaleCohomologyPullbackMap_comp_comparison (X : Scheme.{u}) (g : X ⟶ X)
    (e : 𝟭 X.Etale ≅ smallEtaleBaseChange g)
    [HasWeakSheafify (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v}]
    [∀ F : X.Etaleᵒᵖ ⥤ AddCommGrpCat.{max (u + 1) v},
      (smallEtaleBaseChange g).op.HasLeftKanExtension F]
    [HasSheafify (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v}]
    [HasExt.{w} (Sheaf (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v})]
    (F : Sheaf (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v}) (n : ℕ) :
    (Sheaf.H.map ((etaleSheafPullbackComparison.{u, v} X g e).hom.app F) n).comp
        (etaleCohomologyPullbackMap.{u, v, w} X g e F n) =
      AddMonoidHom.id (Sheaf.H.{w} F n)
Tag 03SN, a theorem

Tag 03SN in the Stacks Project.

Stacks.EtaleCohomology.absoluteFrobeniusCohomologyFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/BafflingTheorem.lean, line 302. The attribute's comment: “pullback along the absolute Frobenius is identified with the identity functor”.

On a scheme X of characteristic p, pullback along the absolute Frobenius is identified with the identity functor on abelian étale sheaves, so composing it with cohomology in degree j gives back cohomology in degree j, naturally in the sheaf.

See Stacks Project, Tag 03SN.

public def absoluteFrobeniusCohomologyFunctorIso
    [HasWeakSheafify (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v}]
    [∀ F : X.Etaleᵒᵖ ⥤ AddCommGrpCat.{max (u + 1) v},
      (smallEtaleBaseChange (absoluteFrobenius X p hX)).op.HasLeftKanExtension F]
    [HasSheafify (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v}]
    [HasExt.{w} (Sheaf (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v})] (j : ℕ) :
    Functor.sheafPullbackConstruction.sheafPullback
          (smallEtaleBaseChange (absoluteFrobenius X p hX)) AddCommGrpCat.{max (u + 1) v}
          (smallEtaleTopology X) (smallEtaleTopology X) ⋙
        Sheaf.functorH (smallEtaleTopology X) j ≅
      Sheaf.functorH (smallEtaleTopology X) j

Stacks.EtaleCohomology.absoluteFrobenius_etaleCohomologyRestrictionMap_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/BafflingTheoremIdentity.lean, line 110. The attribute's comment: “the induced map on H^j(X, Z/nZ) is the identity”. References: SGA 5 XV (2.Proposition2), “special case”.

The Baffling Theorem: on a scheme X of characteristic p the absolute Frobenius induces the identity on H^j(X, ℤ/nℤ). The canonical pullback map on étale cohomology, followed by the canonical identification of the inverse image of the constant sheaf ℤ/nℤ with ℤ/nℤ, sends every class to itself, in every degree j.

public theorem absoluteFrobenius_etaleCohomologyRestrictionMap_eq_id
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})] (n j : ℕ)
    (x : Sheaf.H.{w}
      ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
        (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod n)))) j) :
    Sheaf.H.map
        ((etaleAbelianInverseImageConstantIso.{u, v} (absoluteFrobenius X p hX)).hom.app
          (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod n)))) j
        (etaleCohomologyRestrictionMap.{u, v, w} (absoluteFrobenius X p hX)
          ((constantSheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).obj
            (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod n)))) j x) = x
Tag 03SQ, a definition

Tag 03SQ in the Stacks Project.

Stacks.Frobenius.geometricFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Frobenius.lean, line 276. References: SGA 4½ Rapport (1.1).

Stacks Project, Tag 03SQ. The geometric Frobenius of a scheme over a finite field of characteristic p and cardinality p ^ f. It is the f-fold absolute Frobenius, bundled with its canonical structure as a morphism over the field.

noncomputable def geometricFrobenius {k : Type u} [Field k] [Fintype k]
    (X : Over (Spec (.of k))) (p f : ℕ) [Fact p.Prime] [CharP k p]
    (hcard : Fintype.card k = p ^ f) : X ⟶ X
Tag 03SR, a lemma

Tag 03SR in the Stacks Project.

Stacks.EtaleCohomology.geometricFrobeniusPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FrobeniusDescent.lean, line 305. The attribute's comment: “direct image”. References: SGA 5 XII (7.3), “more general”.

Let k be a finite field with p ^ f elements, let X be a scheme over k and let π_X be the geometric Frobenius of X. Then a sheaf ℱ on the small étale site of X is canonically isomorphic to its direct image (π_X)_* ℱ, naturally in ℱ. On sections over an étale φ : U ⟶ X the isomorphism ℱ(U) ⟶ (π_X)_* ℱ(U) = ℱ(U ×_{φ, X, π_X} X) is restriction along the inverse of γ_U = (F_U^f, φ).

public def geometricFrobeniusPushforwardIso :
    𝟭 (Sheaf (smallEtaleTopology X.left) A) ≅
      (smallEtaleBaseChange
          (Stacks.Frobenius.geometricFrobenius X p f hcard).left).sheafPushforwardContinuous A
        (smallEtaleTopology X.left) (smallEtaleTopology X.left)

Stacks.EtaleCohomology.geometricFrobeniusInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FrobeniusDescent.lean, line 330. The attribute's comment: “inverse image, for coefficients admitting sheafification and left Kan extensions”.

Let k be a finite field with p ^ f elements, let X be a scheme over k and let π_X be the geometric Frobenius of X. Then the inverse image π_X^{-1} ℱ of a sheaf ℱ on the small étale site of X is canonically isomorphic to ℱ, naturally in ℱ. The isomorphism is the left-adjoint mate of geometricFrobeniusPushforwardIso.

public def geometricFrobeniusInverseImageIso
    [HasWeakSheafify (smallEtaleTopology X.left) A]
    [∀ F : X.left.Etaleᵒᵖ ⥤ A,
      (smallEtaleBaseChange
        (Stacks.Frobenius.geometricFrobenius X p f hcard).left).op.HasLeftKanExtension F] :
    Functor.sheafPullbackConstruction.sheafPullback
        (smallEtaleBaseChange (Stacks.Frobenius.geometricFrobenius X p f hcard).left) A
        (smallEtaleTopology X.left) (smallEtaleTopology X.left) ≅
      𝟭 (Sheaf (smallEtaleTopology X.left) A)

Stacks.EtaleCohomology.geometricFrobeniusDescentIsos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FrobeniusInverseImage.lean, line 157. References: SGA 4½ Rapport (1.2); SGA 5 XII (7.3), “more general”.

Stacks Project, Tag 03SR. Let k be a finite field with q = p ^ f elements, let X be a scheme over k with geometric Frobenius π_X = F_X^f, and let ℱ be a sheaf on the small étale site X_étale, with values in any category (sets, abelian groups, Λ-modules, ...). Then there are canonical isomorphisms π_X^{-1} ℱ ≅ ℱ and ℱ ≅ (π_X)_* ℱ, natural in ℱ.

Here (π_X)_* is precomposition with base change along π_X, and the inverse image π_X^{-1} is the left adjoint of (π_X)_*; its existence is proved, not assumed, since (π_X)_* is an equivalence. Where the coefficients admit sheafification it agrees with the sheafified left Kan extension (CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackIso), whose Kan extensions exist by hasLeftKanExtension_smallEtaleBaseChange_geometricFrobenius_op. On sections over an étale φ : U ⟶ X the second isomorphism is restriction along the inverse of γ_U = (F_U^f, φ) : U ⟶ U ×_{φ, X, π_X} X (geometricFrobeniusPushforwardIso_hom_app_hom_app), and the first is its left-adjoint mate (sheafAdjunctionContinuous_unit_comp_geometricFrobeniusSheafPullbackIso).

public def geometricFrobeniusDescentIsos :
    (Functor.sheafPullback
        (smallEtaleBaseChange (Stacks.Frobenius.geometricFrobenius X p f hcard).left) A
        (smallEtaleTopology X.left) (smallEtaleTopology X.left) ≅
      𝟭 (Sheaf (smallEtaleTopology X.left) A)) ×
    (𝟭 (Sheaf (smallEtaleTopology X.left) A) ≅
      (smallEtaleBaseChange
          (Stacks.Frobenius.geometricFrobenius X p f hcard).left).sheafPushforwardContinuous A
        (smallEtaleTopology X.left) (smallEtaleTopology X.left))
Tag 03SS, a remark

Tag 03SS in the Stacks Project.

Stacks.Frobenius.geometricFrobenius_left_eq_absoluteFrobenius_pow_and_exists_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Frobenius.lean, line 382.

Stacks Project, Tag 03SS. The geometric Frobenius of a scheme over a finite field with p ^ f elements is the f-fold absolute Frobenius. The exponent is read off from the base field, so a scheme over two finite fields k and k' can have two distinct geometric Frobenius endomorphisms, as does the spectrum of a field with p ^ 2 elements over the prime field and over itself.

theorem geometricFrobenius_left_eq_absoluteFrobenius_pow_and_exists_ne :
    (∀ (k : Type u) [Field k] [Fintype k] (p f : ℕ) [Fact p.Prime] [CharP k p]
        (hcard : Fintype.card k = p ^ f) (U : Over (Spec (.of k))),
        (geometricFrobenius U p f hcard).left =
          End.asHom (End.of (absoluteFrobenius U.left p (isInCharacteristic_of_over U)) ^ f)) ∧
      ∃ (p f f' : ℕ) (_ : Fact p.Prime) (k k' : Type u) (_ : Field k) (_ : Fintype k)
        (_ : CharP k p) (_ : Field k') (_ : Fintype k') (_ : CharP k' p)
        (hcard : Fintype.card k = p ^ f) (hcard' : Fintype.card k' = p ^ f') (U : Scheme.{u})
        (g : U ⟶ Spec (.of k)) (g' : U ⟶ Spec (.of k')),
        (geometricFrobenius (Over.mk g) p f hcard).left ≠
          (geometricFrobenius (Over.mk g') p f' hcard').left
Tag 03ST, a lemma

Tag 03ST in the Stacks Project.

Stacks.Frobenius.fibreComparison_galoisStalkAction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GaloisActionFibreCohomology.lean, line 395. The attribute's comment: “Galois equivariance of the Theorem 03Q9 comparison in degree zero: unconditional in α, in the sheaf and in the algebraically closed extension, stated on the germ at an arbitrary étale neighbourhood of the geometric point. That the comparison is an isomorphism is Tag 03Q9, available in this library only over a strictly henselian base, and the equivariance in degree j > 0 needs transitivity of restriction of sections in the scheme over the base; neither is assumed here”.

Stacks Project, Tag 03ST, Galois equivariance in degree zero. The comparison of Étale Cohomology, Theorem 03Q9 carries the Galois action of Étale Cohomology Section 03QW on the stalk (α_* ℱ)_{Spec k̄} to restriction along the automorphism id_X × Spec σ of the geometric fibre X_{k̄}: on the germ at an étale neighbourhood W of the geometric point, acting by σ and then comparing is restricting along (id_X × Spec σ) ∘ (X_{k̄} ⟶ X_W).

Since the germs are jointly surjective onto the stalk, this determines the induced map on the whole stalk, and it is the statement that the identification of Tag 03Q9 is a map of G_k-modules.

public theorem fibreComparison_galoisStalkAction (σ : K ≃ₐ[k] K)
    (W : (Spec (.of k)).Etale)
    (u : (Scheme.pointSmallEtale (specAlgebraMap k K)).fiber.obj W) :
    (Scheme.pointSmallEtale (specAlgebraMap k K)).toPresheafFiber W u
          ((sheafToPresheaf _ _).obj ((smallEtalePushforwardAb X.hom).obj F)) ≫
        (galoisStalkAction Ab.{u + 1} K σ (𝟙 (Spec (.of k)))).app
          ((smallEtalePushforwardAb X.hom).obj F) ≫
        fibreComparison K X F =
      (smallEtaleSectionsPullbackAb (pullback.fst X.hom (specAlgebraMap k K))
        ((smallEtaleBaseChange X.hom).obj W)
        (galoisBaseChange X K σ ≫ fibreLift K X W u)
        ((congrArg (fun z => z ≫ ((smallEtaleBaseChange X.hom).obj W).hom)
            (galoisBaseChange_comp_fibreLift K X σ W u).symm).trans
          (fibreLift_comp_hom K X W (galoisLift K σ W u)))).app F

Stacks.Frobenius.higherDirectImageFibreMap_isIso_galoisEquivariant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GaloisModuleHigherDirectImageStalk.lean, line 245. References: SGA 4½ Arcata (2.3.3), “special case”; SGA 4½ Rapport (1.4), “special case”; SGA 7 XXII (2.2), “more general”.

Stacks Project, Tag 03ST. Let k be a finite field, K an algebraic closure of k, G_k = Gal(K/k), α : X ⟶ Spec k quasi-compact and quasi-separated, and ℱ an abelian sheaf on X_étale. For every j, the identification (R^j α_* ℱ)_{Spec K} ≅ H^j(X_K, ℱ|_{X_K}) of Étale Cohomology, Theorem 03Q9 is an isomorphism of G_k-modules:

  • it is an isomorphism;
  • it carries the Galois action of Étale Cohomology Section 03QW on the stalk at Spec K of the j-th higher direct image (Stacks.Frobenius.fieldGaloisStalkAction, which is the base's Stacks.Frobenius.galoisStalkAction at the rational point 𝟙 (Spec k)) to the action σ ↦ (Spec σ × id_X)^* on cohomology (Stacks.Frobenius.galoisCohomologyAction);
  • the latter is a left action of G_k, as the former is (fieldGaloisStalkAction_one, fieldGaloisStalkAction_mul).

The identification is Stacks.Frobenius.higherDirectImageFibreMap: the degree-zero comparison of 03Q9 — restriction of the germ of a section of α_* ℱ over an étale neighbourhood of Spec K to the geometric fibre X_K — passed to right derived functors; the strict henselization of Spec k at Spec K is Spec K, the finite field k being perfect. The hypothesis on α is that of Theorem 03Q9, whose identification exists only then; see the module docstring.

In the language of modules: Stacks.Frobenius.higherDirectImageFibreAddEquiv is an additive equivalence which is G_k-equivariant (Stacks.Frobenius.higherDirectImageFibreAddEquiv_smul) for the G_k-module structures Stacks.Frobenius.galoisHigherDirectImageStalkDistribMulAction and Stacks.Frobenius.galoisCohomologyDistribMulAction.

theorem higherDirectImageFibreMap_isIso_galoisEquivariant [Finite k] [Algebra.IsAlgebraic k K]
    [QuasiCompact X.hom] [QuasiSeparated X.hom] (j : ℕ)
    (F : Sheaf (smallEtaleTopology X.left) Ab.{u + 1}) :
    IsIso (higherDirectImageFibreMap K X (acyclic_fieldBaseChangePullbackAb_of_injective K X) j F) ∧
      (∀ σ : K ≃ₐ[k] K,
        (fieldGaloisStalkAction K σ).app (((smallEtalePushforwardAb X.hom).rightDerived j).obj F) ≫
            higherDirectImageFibreMap K X (acyclic_fieldBaseChangePullbackAb_of_injective K X) j F =
          higherDirectImageFibreMap K X (acyclic_fieldBaseChangePullbackAb_of_injective K X) j F ≫
            galoisCohomologyAction K X σ j F) ∧
      galoisCohomologyAction K X (1 : K ≃ₐ[k] K) j F = 𝟙 _ ∧
      ∀ σ τ : K ≃ₐ[k] K, galoisCohomologyAction K X (σ * τ) j F =
        galoisCohomologyAction K X τ j F ≫ galoisCohomologyAction K X σ j F
Tag 03SU, a definition

Tag 03SU in the Stacks Project.

Stacks.Frobenius.arithmeticFrobenius, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Frobenius.lean, line 304. References: SGA 7 XXI (5.0).

Stacks Project, Tag 03SU. The arithmetic Frobenius x ↦ x ^ q of a finite field k with q = p ^ f elements, acting on a perfect extension field K of exponential characteristic p. It is the f-fold Frobenius automorphism of K, and it fixes k pointwise because every element of a field with q elements satisfies x ^ q = x.

noncomputable def arithmeticFrobenius (hcard : Fintype.card k = p ^ f) : K ≃ₐ[k] K
Tag 03SV, a theorem

Tag 03SV in the Stacks Project.

Stacks.Frobenius.galoisRestrictionEndo_comp_geometricFrobeniusRestrictionEndo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ArithmeticFrobeniusInverse.lean, line 434. The attribute's comment: “the Galois action of frob_k after the map induced by the geometric Frobenius is the identity”.

Let k be a finite field with q = p ^ f elements, let X be a scheme over k, let K/k be an extension and let σ be the arithmetic Frobenius x ↦ x ^ q of K. For an abelian sheaf ℱ on X_étale and every degree j, the endomorphism of H^j(X_K, ℱ|_{X_K}) induced by the Galois action id_X × Spec(σ) undoes the one induced by π_X × id: the arithmetic Frobenius acts as the inverse of π_X^*.

Each endomorphism restricts along the morphism of X_K and then identifies the coefficients again: along X for the Galois action (galoisRestrictionCoeff), and through the Frobenius descent on X for the geometric Frobenius (geometricFrobeniusRestrictionCoeff).

public theorem galoisRestrictionEndo_comp_geometricFrobeniusRestrictionEndo (n : ℕ)
    (F : Sheaf X.left.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
    (etaleCohomologyEndo.{u, v, w} (galoisBaseChange X K σ)
          ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F)
          (galoisRestrictionCoeff.{u, v} X K σ F) n).comp
        (etaleCohomologyEndo.{u, v, w} (geometricFrobeniusBaseChange X K p f hcard)
          ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F)
          (geometricFrobeniusRestrictionCoeff.{u, v} X K p f hcard F) n) =
      AddMonoidHom.id (Sheaf.H.{w}
        ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F) n)

Stacks.Frobenius.geometricFrobeniusRestrictionEndo_comp_galoisRestrictionEndo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ArithmeticFrobeniusInverse.lean, line 471. The attribute's comment: “the map induced by the geometric Frobenius after the Galois action of frob_k is the identity”.

With the data of galoisRestrictionEndo_comp_geometricFrobeniusRestrictionEndo, the endomorphism of H^j(X_K, ℱ|_{X_K}) induced by π_X × id undoes the one induced by the Galois action id_X × Spec(σ); so the two endomorphisms are mutually inverse.

public theorem geometricFrobeniusRestrictionEndo_comp_galoisRestrictionEndo (n : ℕ)
    (F : Sheaf X.left.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
    (etaleCohomologyEndo.{u, v, w} (geometricFrobeniusBaseChange X K p f hcard)
          ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F)
          (geometricFrobeniusRestrictionCoeff.{u, v} X K p f hcard F) n).comp
        (etaleCohomologyEndo.{u, v, w} (galoisBaseChange X K σ)
          ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F)
          (galoisRestrictionCoeff.{u, v} X K σ F) n) =
      AddMonoidHom.id (Sheaf.H.{w}
        ((etaleAbelianInverseImage.{u, v} (fieldBaseChangeProj X K)).obj F) n)
Tag 03SW, a definition

Tag 03SW in the Stacks Project.

Stacks.Frobenius.geometricFrobeniusStalkFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricFrobeniusStalk.lean, line 183. The attribute's comment: “on the stalk functor”. References: SGA 7 XXI (5.0), “F_x acts on G_x̄”; SGA 7 I (6.3); SGA 7 XXII (2.2.4), “The element φ_q”.

Stacks Project, Tag 03SW. The geometric Frobenius at a rational point x of a scheme over a finite field k with p ^ f elements, as an endomorphism of the étale stalk functor at the geometric point over x: it is the action of the inverse of the arithmetic Frobenius.

def geometricFrobeniusStalkFunctor (hcard : Fintype.card k = p ^ f) (x : Spec (.of k) ⟶ X) :
    (Scheme.pointSmallEtale (rationalGeometricPoint K x).hom).sheafFiber (A := A) ⟶
      (Scheme.pointSmallEtale (rationalGeometricPoint K x).hom).sheafFiber

Stacks.Frobenius.geometricFrobeniusStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricFrobeniusStalk.lean, line 191. References: SGA 7 XXI (5.0), “F_x acts on G_x̄”.

Stacks Project, Tag 03SW. The geometric Frobenius at a rational point x, acting on the étale stalk of a sheaf F at the geometric point over x.

def geometricFrobeniusStalk (hcard : Fintype.card k = p ^ f) (x : Spec (.of k) ⟶ X)
    (F : Sheaf X.smallEtaleTopology A) :
    (Scheme.pointSmallEtale (rationalGeometricPoint K x).hom).sheafFiber.obj F ⟶
      (Scheme.pointSmallEtale (rationalGeometricPoint K x).hom).sheafFiber.obj F
Sources
LeancohomologyPullbackMap_eq_id_of_preimageEq · Stacks.EtaleCohomology.etaleCohomologyPullbackMap_comp_comparison · Stacks.EtaleCohomology.absoluteFrobeniusCohomologyFunctorIso · Stacks.EtaleCohomology.absoluteFrobenius_etaleCohomologyRestrictionMap_eq_id · Stacks.Frobenius.geometricFrobenius · Stacks.EtaleCohomology.geometricFrobeniusPushforwardIso · Stacks.EtaleCohomology.geometricFrobeniusInverseImageIso · Stacks.EtaleCohomology.geometricFrobeniusDescentIsos

Section64.4 Traces#

Section 64.4 of the Stacks Project, Tag 03SZ. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03T0, a definition

Tag 03T0 in the Stacks Project.

CategoryTheory.FilteredDerived.freeModuleTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/FreeModuleTrace.lean, line 77. References: SGA 4½ Rapport (4.2), “free module tr”; SGA 5 IIIB (5.7), “5.7.1-5.7.2”.

Stacks Project, Tag 03T0. The trace of an endomorphism of a finite free left module, valued in the additive commutator quotient of the coefficient ring.

noncomputable def freeModuleTrace (ι : Type v) [Fintype ι] :
    Module.End R (ι → R) →+ AdditiveCommutatorQuotient R
Tag 03T1, an exercise

Tag 03T1 in the Stacks Project.

Stacks.TraceFormula.freeTrace_comp_comm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/NumberTheory/TraceFormula/NaturalTrace.lean, line 122. The attribute's comment: “Tr(ab) = Tr(ba) in Λ^♮ for a : Λ^⊕m → Λ^⊕n and b : Λ^⊕n → Λ^⊕m, where Λ is a ring that is not assumed commutative and Λ^♮ is Λ modulo the additive subgroup generated by the commutators”.

Stacks Project, Tag 03T1. Given Λ-linear maps a : Λ^⊕m → Λ^⊕n and b : Λ^⊕n → Λ^⊕m over a ring Λ, the traces of ab and of ba agree in Λ^♮.

public theorem freeTrace_comp_comm {m n : ℕ} (a : (Fin m → Λ) →ₗ[Λ] (Fin n → Λ))
    (b : (Fin n → Λ) →ₗ[Λ] (Fin m → Λ)) :
    freeTrace (b ∘ₗ a) = freeTrace (a ∘ₗ b)
Sources
LeanCategoryTheory.FilteredDerived.freeModuleTrace · Stacks.TraceFormula.freeTrace_comp_comm

Section64.6 Derived categories#

Section 64.6 of the Stacks Project, Tag 03T3. 3 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03T5, a lemma

Tag 03T5 in the Stacks Project.

Declarations registered for the tag:

Tag 03T6, a lemma

Tag 03T6 in the Stacks Project.

CategoryTheory.HomotopyCategory.PlusInjective.isEquivalence_toDerivedPlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/BoundedBelowInjectiveEquivalence.lean, line 120. The attribute's comment: “injective_equivalence”. References: SGA 4½ Etat 0 (3.2.3), “(3)”; SGA 4½ Etat 0 (3.1.4).

Stacks 03T6, part (3). If A has enough injectives and I ⊆ A is the additive subcategory of injectives, then D⁺(A) ≅ K⁺(I): the canonical functor from the bounded below homotopy category of complexes of injective objects to the bounded below derived category is an equivalence.

theorem isEquivalence_toDerivedPlus [EnoughInjectives A] :
    (toDerivedPlus A).IsEquivalence

CochainComplex.Qh_map_bijective_of_projective_of_minus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/MorphismsFromBoundedAboveProjectives.lean, line 49. The attribute's comment: “projective_hom”. References: SGA 4½ Etat 0 (3.2.3), “(4) proj. analogue”.

Stacks 03T6, part (2). A bounded above complex of projective objects computes morphisms from it in the derived category already in the homotopy category.

theorem Qh_map_bijective_of_projective_of_minus [HasDerivedCategory.{w} A]
    (P : CochainComplex A ℤ) (K : HomotopyCategory A (ComplexShape.up ℤ))
    (hP : CochainComplex.minus A P) [∀ n, Projective (P.X n)] :
    Function.Bijective (DerivedCategory.Qh.map :
      ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj P ⟶ K) → _)

CochainComplex.Qh_map_bijective_of_injective_of_plus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/MorphismsIntoBoundedBelowInjectives.lean, line 49. The attribute's comment: “injective_hom”.

Stacks 03T6, part (1). A bounded below complex of injective objects computes morphisms into it in the derived category already in the homotopy category.

theorem Qh_map_bijective_of_injective_of_plus [HasDerivedCategory.{w} A]
    (K : HomotopyCategory A (ComplexShape.up ℤ)) (I : CochainComplex A ℤ)
    (hI : CochainComplex.plus A I) [∀ n, Injective (I.X n)] :
    Function.Bijective (DerivedCategory.Qh.map :
      (K ⟶ (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj I) → _)

CategoryTheory.HomotopyCategory.MinusProjective.isEquivalence_toDerivedMinus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 155. The attribute's comment: “projective_equivalence”. References: SGA 4½ Etat 0 (3.2.3), “(4) proj. analogue”.

Stacks 03T6, part (4). If A has enough projectives and P ⊆ A is the additive subcategory of projectives, then D⁻(A) ≅ K⁻(P): the canonical functor from the bounded above homotopy category of complexes of projective objects to the bounded above derived category is an equivalence.

theorem isEquivalence_toDerivedMinus [EnoughProjectives A] :
    (toDerivedMinus A).IsEquivalence
Tag 03T7, a definition

Tag 03T7 in the Stacks Project.

CategoryTheory.Functor.mapMinusProjectiveToDerivedMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 192. The attribute's comment: “the projective-complex route for the left derived functor”.

The lower route in the diagram defining the total left derived functor: apply the additive functor termwise to a bounded above complex of projectives, then pass to the bounded above derived category.

def mapMinusProjectiveToDerivedMinus (G : A ⥤ B) [G.Additive] :
    HomotopyCategory.MinusProjective A ⥤ DerivedCategory.Minus B

CategoryTheory.Functor.leftDerivedFunctorMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 213. The attribute's comment: “the total left derived functor”. References: SGA 4½ Etat 0 (4.1.2), “left derived functor”; SGA 4½ Etat 0 (4.1.4), “LF”; SGA 4½ Etat 0 (4.1.5), “L^- f”; SGA 4 XVII (1.2.5), “(ii), single functor”; SGA 4½ Etat 0 (4.1.3), “L⁻ f”.

The total left derived functor on the bounded above derived category, constructed using bounded above complexes of projective objects.

def leftDerivedFunctorMinus (G : A ⥤ B) [G.Additive] [EnoughProjectives A] :
    DerivedCategory.Minus A ⥤ DerivedCategory.Minus B

CategoryTheory.Functor.leftDerivedFunctorMinusIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 223. The attribute's comment: “the comparison isomorphism for the total left derived functor”.

The natural commuting isomorphism in the projective-resolution diagram defining the total left derived functor.

def leftDerivedFunctorMinusIso (G : A ⥤ B) [G.Additive] [EnoughProjectives A] :
    HomotopyCategory.MinusProjective.toDerivedMinus A ⋙ leftDerivedFunctorMinus G ≅
      mapMinusProjectiveToDerivedMinus G

CategoryTheory.Functor.mapPlusInjectiveToDerivedPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 236. The attribute's comment: “the injective-complex route for the right derived functor”.

The lower route in the diagram defining the total right derived functor: apply the additive functor termwise to a bounded below complex of injectives, then pass to the bounded below derived category.

def mapPlusInjectiveToDerivedPlus (F : A ⥤ B) [F.Additive] :
    HomotopyCategory.PlusInjective A ⥤ DerivedCategory.Plus B

CategoryTheory.Functor.rightDerivedFunctorPlusOfInjectives, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 255. The attribute's comment: “the total right derived functor”. References: SGA 4½ Etat 0 (4.1.2), “right derived functor”; SGA 4½ Etat 0 (4.1.4), “RF”; SGA 4 XVII (1.2.5), “(ii), single functor”.

The total right derived functor on the bounded below derived category, constructed using bounded below complexes of injective objects.

def rightDerivedFunctorPlusOfInjectives (F : A ⥤ B) [F.Additive] [EnoughInjectives A] :
    DerivedCategory.Plus A ⥤ DerivedCategory.Plus B

CategoryTheory.Functor.rightDerivedFunctorPlusOfInjectivesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 265. The attribute's comment: “the comparison isomorphism for the total right derived functor”.

The natural commuting isomorphism in the injective-resolution diagram defining the total right derived functor.

def rightDerivedFunctorPlusOfInjectivesIso (F : A ⥤ B) [F.Additive] [EnoughInjectives A] :
    HomotopyCategory.PlusInjective.toDerivedPlus A ⋙ rightDerivedFunctorPlusOfInjectives F ≅
      mapPlusInjectiveToDerivedPlus F

CategoryTheory.Functor.rightDerivedFunctorPlusOfInjectivesUnit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TotalDerivedFunctors.lean, line 304. The attribute's comment: “the comparison map for the total right derived functor”.

The comparison map for the total right derived functor: the natural transformation from "apply F termwise, then localize" to the composite of the localization functor with RF.

def rightDerivedFunctorPlusOfInjectivesUnit (F : A ⥤ B) [F.Additive] [EnoughInjectives A] :
    F.mapHomotopyCategoryPlus ⋙ DerivedCategory.Plus.Qh ⟶
      DerivedCategory.Plus.Qh ⋙ rightDerivedFunctorPlusOfInjectives F
Sources
LeanDerivedCategory.isGE_iff · CategoryTheory.Triangulated.TStructure.plus · DerivedCategory.isLE_iff · CategoryTheory.Triangulated.TStructure.minus · CategoryTheory.Triangulated.TStructure.bounded · CategoryTheory.HomotopyCategory.PlusInjective.isEquivalence_toDerivedPlus · CochainComplex.Qh_map_bijective_of_projective_of_minus · CochainComplex.Qh_map_bijective_of_injective_of_plus

Section64.7 Filtered derived category#

Section 64.7 of the Stacks Project, Tag 03T9. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier) and 16 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TA, a definition

Tag 03TA in the Stacks Project.

CategoryTheory.FilteredDerived.filteredDerivedPlus, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/DerivedCategory.lean, line 86. The attribute's comment: “filtered_derived_plus”. References: SGA 4 Vbis (2.5.1), “D^+F(A)”.

The localisation of K⁺(Fil^f(A)) at filtered quasi-isomorphisms.

abbrev filteredDerivedPlus (A : Type u) [Category.{v} A] [Abelian A]

CategoryTheory.FiniteFilteredObject.hasFiniteBiproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/Objects.lean, line 90. The attribute's comment: “finite_filtered_additive”.

The category of finite filtered objects has finite biproducts.

noncomputable instance hasFiniteBiproducts (C : Type u) [Category.{v} C]
    [Preadditive C] [HasZeroObject C] [HasBinaryBiproducts C] :
    HasFiniteBiproducts (FiniteFilteredObject C)

CategoryTheory.FilteredDerived.IsFilteredProjective, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/Projective.lean, line 62. The attribute's comment: “filtered_projective”.

A finite filtered object is filtered projective if all its graded pieces are projective.

abbrev IsFilteredProjective {C : Type u} [Category.{v} C] [Abelian C]
    (I : FiniteFilteredObject C) : Prop

Declarations registered for the tag:

Tag 03TB, a lemma

Tag 03TB in the Stacks Project.

CategoryTheory.FilteredDerived.filteredProjectiveMinusToDerivedMinus_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/BoundedEquivalence.lean, line 510. The attribute's comment: “projective case”.

The bounded-above filtered derived category is equivalent to the bounded-above homotopy category of filtered projective objects.

theorem filteredProjectiveMinusToDerivedMinus_isEquivalence [EnoughProjectives A] :
    (filteredProjectiveMinusToDerivedMinus A).IsEquivalence

Declarations registered for the tag:

Sources
LeanCategoryTheory.FilteredDerived.filteredDerivedPlus · CategoryTheory.FiniteFilteredObject.hasFiniteBiproducts · CategoryTheory.FilteredDerived.IsFilteredProjective · CochainComplex · CochainComplex.Plus · HomotopyCategory · HomotopyCategory.Plus · CochainComplex.filteredQuasiIsoC

Section64.8 Filtered derived functors#

Section 64.8 of the Stacks Project, Tag 03TC. 2 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TD, a definition

Tag 03TD in the Stacks Project.

CategoryTheory.FilteredDerived.filteredProjectiveMinusMapToDerivedMinus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/LeftDerivedFunctor.lean, line 133. The attribute's comment: “filtered_left_derived_functor”.

The lower route in the defining diagram: apply G termwise to a bounded-above complex of filtered projective objects, then pass to the bounded-above filtered derived category.

noncomputable def filteredProjectiveMinusMapToDerivedMinus
    (G : A ⥤ B) [G.Additive] :
    (filteredProjectiveMinus A).FullSubcategory ⥤
      (CochainComplex.FilteredDerivedCategory.minus B).FullSubcategory

CategoryTheory.FilteredDerived.filteredLeftDerivedFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/LeftDerivedFunctor.lean, line 162. The attribute's comment: “filtered_left_derived_functor”.

The filtered left derived functor on bounded-above filtered derived categories.

noncomputable def filteredLeftDerivedFunctor
    (G : A ⥤ B) [G.Additive] [EnoughProjectives A] :
    (CochainComplex.FilteredDerivedCategory.minus A).FullSubcategory ⥤
      (CochainComplex.FilteredDerivedCategory.minus B).FullSubcategory

CategoryTheory.FilteredDerived.filteredLeftDerivedFunctorComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/LeftDerivedFunctor.lean, line 173. The attribute's comment: “filtered_left_derived_functor”.

The natural isomorphism making the projective-resolution diagram commute.

noncomputable def filteredLeftDerivedFunctorComparison
    (G : A ⥤ B) [G.Additive] [EnoughProjectives A] :
    filteredProjectiveMinusToDerivedMinus A ⋙ filteredLeftDerivedFunctor G ≅
      filteredProjectiveMinusMapToDerivedMinus G

CategoryTheory.FilteredDerived.filteredInjectivePlusMapToDerivedPlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/RightDerivedFunctor.lean, line 58. The attribute's comment: “filtered_right_derived_functor”.

The lower route in the defining diagram of the filtered right derived functor: apply T termwise to a bounded-below complex of filtered injective objects, then pass to the bounded-below filtered derived category.

noncomputable def filteredInjectivePlusMapToDerivedPlus (T : A ⥤ B) [T.Additive] :
    (CochainComplex.FilteredDerivedCategory.filteredInjectivePlus A).FullSubcategory ⥤
      (CochainComplex.FilteredDerivedCategory.plus B).FullSubcategory

CategoryTheory.FilteredDerived.filteredRightDerivedFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/RightDerivedFunctor.lean, line 80. The attribute's comment: “filtered_right_derived_functor”.

The filtered right derived functor RT : DF⁺(A) ⥤ DF⁺(B) of an additive functor T : A ⥤ B, defined when A has enough injectives.

noncomputable def filteredRightDerivedFunctor (T : A ⥤ B) [T.Additive] [EnoughInjectives A] :
    (CochainComplex.FilteredDerivedCategory.plus A).FullSubcategory ⥤
      (CochainComplex.FilteredDerivedCategory.plus B).FullSubcategory

CategoryTheory.FilteredDerived.filteredRightDerivedFunctorComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/RightDerivedFunctor.lean, line 89. The attribute's comment: “filtered_right_derived_functor”.

The natural isomorphism making the injective-resolution diagram for the filtered right derived functor commute.

noncomputable def filteredRightDerivedFunctorComparison (T : A ⥤ B) [T.Additive]
    [EnoughInjectives A] :
    CochainComplex.FilteredDerivedCategory.toPlus A ⋙ filteredRightDerivedFunctor T ≅
      filteredInjectivePlusMapToDerivedPlus T
Tag 03TE, a proposition

Tag 03TE in the Stacks Project.

CategoryTheory.FilteredDerived.filteredRightDerivedFunctorGrPIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Category/GradedRightDerivedFunctor.lean, line 271.

Taking the p-th graded piece commutes with the filtered right derived functor: for an additive functor T : A ⥤ B out of an abelian category with enough injectives, there is a natural isomorphism RT ⋙ gr^p ≅ gr^p ⋙ RT of functors DF⁺(A) ⥤ D⁺(B).

See Stacks Project, Tag 03TE.

noncomputable def filteredRightDerivedFunctorGrPIso (T : A ⥤ B) [T.Additive]
    [EnoughInjectives A] (p : ℤ) :
    filteredRightDerivedFunctor T ⋙
        CochainComplex.FilteredDerivedCategory.liftDFPlus (FiniteFilteredObject.grP p)
          (CochainComplex.FilteredDerivedCategory.grP_inverts p) ≅
      CochainComplex.FilteredDerivedCategory.liftDFPlus (FiniteFilteredObject.grP p)
          (CochainComplex.FilteredDerivedCategory.grP_inverts p) ⋙
        T.rightDerivedFunctorPlus
Sources
LeanCategoryTheory.FilteredDerived.filteredProjectiveMinusMapToDerivedMinus · CategoryTheory.FilteredDerived.filteredLeftDerivedFunctor · CategoryTheory.FilteredDerived.filteredLeftDerivedFunctorComparison · CategoryTheory.FilteredDerived.filteredInjectivePlusMapToDerivedPlus · CategoryTheory.FilteredDerived.filteredRightDerivedFunctor · CategoryTheory.FilteredDerived.filteredRightDerivedFunctorComparison · CategoryTheory.FilteredDerived.filteredRightDerivedFunctorGrPIso

Section64.10 Perfectness#

Section 64.10 of the Stacks Project, Tag 03TG. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TH, a definition

Tag 03TH in the Stacks Project.

CategoryTheory.FilteredDerived.PerfectHomotopyCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Basic.lean, line 73. The attribute's comment: “the category K_perf”. References: SGA 4½ Rapport (4.3), “K_parf(Λ)”.

The category K_perf(R) of bounded complexes of finite projective R-modules, with morphisms up to homotopy.

public abbrev PerfectHomotopyCategory (R : Type u) [Ring R]

CategoryTheory.FilteredDerived.perfectComplexFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Basic.lean, line 78. The attribute's comment: “the functor to D(R)”.

The canonical functor from K_perf(R) to D(R).

public def perfectComplexFunctor (R : Type u) [Ring R] :
    PerfectHomotopyCategory.{u, v} R ⥤ DerivedCategory (ModuleCat.{v} R)

CategoryTheory.FilteredDerived.perfectComplexFunctorFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Basic.lean, line 111. The attribute's comment: “full faithfulness”. References: SGA 4 XVII (5.5.6.3), “more general”; SGA 4½ Rapport (4.3); SGA 6 I (4.10), “Clause (i), special case”; SGA 6 I (4.12.2), “Case C = R-modules”; SGA 6 II (1.1), “c), special case”.

The canonical functor from perfect complexes up to homotopy to the derived category is fully faithful.

public def perfectComplexFunctorFullyFaithful (R : Type u) [Ring R] :
    (perfectComplexFunctor.{u, v} R).FullyFaithful

CategoryTheory.FilteredDerived.isPerfect_iff, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Basic.lean, line 142. The attribute's comment: “perfect objects”. References: SGA 4½ Rapport (4.3), “D_parf(Λ)”.

A derived object is perfect exactly when it is isomorphic to the image of a bounded complex of finite projective modules.

public lemma isPerfect_iff (R : Type u) [Ring R]
    (X : DerivedCategory (ModuleCat.{v} R)) :
    StacksDraft.Perfect.IsPerfect X ↔
      ∃ K : CochainComplex (ModuleCat.{v} R) ℤ,
        finiteProjectiveComplex.{u, v} R K ∧ Nonempty (DerivedCategory.Q.obj K ≅ X)

CategoryTheory.FilteredDerived.PerfectDerivedCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Basic.lean, line 178. The attribute's comment: “the category D_perf”. References: SGA 4½ Rapport (4.3), “D_parf(Λ)”.

The full subcategory D_perf(R) of perfect derived objects.

public abbrev PerfectDerivedCategory (R : Type u) [Ring R]
Tag 03TI, a proposition

Tag 03TI in the Stacks Project.

CategoryTheory.FilteredDerived.perfectDerivedTrace_eq_alternatingTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/Trace.lean, line 276.

The trace of an endomorphism of a perfect derived object is computed on any bounded finite-projective representative, and hence is independent of the representative, the chosen isomorphism, and the cochain map representing the endomorphism.

public theorem perfectDerivedTrace_eq_alternatingTrace (R : Type u) [Ring R]
    (K : PerfectDerivedCategory.{u, v} R) (f : K.obj ⟶ K.obj)
    (P : CochainComplex (ModuleCat.{v} R) ℤ)
    (hP : finiteProjectiveComplex R P)
    (e : DerivedCategory.Q.obj P ≅ K.obj) (g : P ⟶ P)
    (hg : DerivedCategory.Q.map g = e.hom ≫ f ≫ e.inv) :
    perfectDerivedTrace R K f = alternatingTrace R P hP g
Sources
LeanCategoryTheory.FilteredDerived.PerfectHomotopyCategory · CategoryTheory.FilteredDerived.perfectComplexFunctor · CategoryTheory.FilteredDerived.perfectComplexFunctorFullyFaithful · CategoryTheory.FilteredDerived.isPerfect_iff · CategoryTheory.FilteredDerived.PerfectDerivedCategory · CategoryTheory.FilteredDerived.perfectDerivedTrace_eq_alternatingTrace

Section64.11 Filtrations and perfect complexes#

Section 64.11 of the Stacks Project, Tag 03TJ. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TK, a lemma

Tag 03TK in the Stacks Project.

CategoryTheory.FilteredDerived.perfectDerivedTrace_eq_sum_grDF, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/FilteredTrace.lean, line 507. References: SGA 4½ Rapport (4.4), “(4.4.1)”; SGA 5 IIIB (5.6), “(5.6.5), F = A”.

Stacks 03TK. Trace is additive along the filtration of a perfect filtered derived complex.

public theorem perfectDerivedTrace_eq_sum_grDF (R : Type u) [Ring R]
    (K : FilteredPerfectData.{u, v} R) (f : K.obj ⟶ K.obj) :
    perfectDerivedTrace R
      ⟨(CochainComplex.FilteredDerivedCategory.forgetDF).obj K.obj,
        K.forgetPerfect R⟩
      ((CochainComplex.FilteredDerivedCategory.forgetDF).map f) =
      ∑ᶠ p : ℤ, perfectDerivedTrace R
        ⟨(CochainComplex.FilteredDerivedCategory.grDF p).obj K.obj,
          K.gradedPerfect R p⟩
        ((CochainComplex.FilteredDerivedCategory.grDF p).map f)
Tag 03TL, a lemma

Tag 03TL in the Stacks Project.

CategoryTheory.FilteredDerived.projectiveModuleTrace_eq_sum_grP, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FilteredDerived/Perfectness/FilteredModuleTrace.lean, line 132. References: SGA 4½ Rapport (4.2), “(4.2.2) ungraded”; SGA 5 IIIB (5.6), “special case”.

The trace of a filtered endomorphism of a finite projective module is the sum of the traces on its associated graded pieces.

public theorem projectiveModuleTrace_eq_sum_grP (R : Type u) [Ring R]
    (P : FiniteFilteredObject (ModuleCat.{max u v} R))
    (hP : IsFilteredFiniteProjective P)
    (f : P ⟶ P) :
    (letI : Module.Finite R ((FiniteFilteredObject.forget
          (𝒜 := ModuleCat.{max u v} R)).obj P) :=
        hP.finite_projective_forget.1;
      letI : Module.Projective R ((FiniteFilteredObject.forget
          (𝒜 := ModuleCat.{max u v} R)).obj P) :=
        hP.finite_projective_forget.2;
      Stacks.Trace.projectiveModuleTrace R
        ((FiniteFilteredObject.forget (𝒜 := ModuleCat.{max u v} R)).obj P)
        ((FiniteFilteredObject.forget (𝒜 := ModuleCat.{max u v} R)).map f).hom) =
      ∑ᶠ p : ℤ,
        (letI : Projective ((FiniteFilteredObject.grP
            (𝒜 := ModuleCat.{max u v} R) p).obj P) := (hP p).2;
          letI : Module.Finite R ((FiniteFilteredObject.grP
              (𝒜 := ModuleCat.{max u v} R) p).obj P) := (hP p).1;
          letI : Module.Projective R ((FiniteFilteredObject.grP
              (𝒜 := ModuleCat.{max u v} R) p).obj P) := inferInstance;
          Stacks.Trace.projectiveModuleTrace R
            ((FiniteFilteredObject.grP (𝒜 := ModuleCat.{max u v} R) p).obj P)
            ((FiniteFilteredObject.grP (𝒜 := ModuleCat.{max u v} R) p).map f).hom)
Sources
LeanCategoryTheory.FilteredDerived.perfectDerivedTrace_eq_sum_grDF · CategoryTheory.FilteredDerived.projectiveModuleTrace_eq_sum_grP

Section64.12 Characterizing perfect objects#

Section 64.12 of the Stacks Project, Tag 03TM. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TN, a definition

Tag 03TN in the Stacks Project.

StacksDraft.Perfect.HasFiniteTorDimensionCanonical, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/BalancedDerivedTensor.lean, line 627. References: SGA 4½ Rapport (4.5), “finite tor dimension”.

An object K of D(Λ) has finite Tor dimension if there are integers a, b such that Hⁱ(N ⊗ᴸ[Λ] K) = 0 for every right Λ-module N and every i ∉ [a, b]. This is the definition at the balanced derived tensor product constructed here, so it takes no parameter; by hasFiniteTorDimensionCanonical_iff it is the same condition as StacksDraft.Perfect.HasFiniteTorDimension at any term of BalancedDerivedTensoring Λ.

def HasFiniteTorDimensionCanonical [Small.{v} Λ] (K : DerivedCategory (ModuleCat.{v} Λ)) : Prop

StacksDraft.Perfect.HasFiniteTorDimension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/FiniteTorDimension.lean, line 109. References: SGA 4½ Rapport (4.5), “finite tor dimension”.

An object K of D(Λ) has finite Tor dimension if there are integers a, b such that Hⁱ(N ⊗ᴸ[Λ] K) = 0 for every right Λ-module N and every i ∉ [a, b].

def HasFiniteTorDimension {Λ : Type u} [Ring Λ] (D : BalancedDerivedTensoring.{u, v} Λ)
    (K : DerivedCategory (ModuleCat.{v} Λ)) : Prop
Tag 03TO, a lemma

Tag 03TO in the Stacks Project.

StacksDraft.Perfect.isPerfect_iff_hasFiniteTorDimension_balancedDerivedTensoring, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/BalancedDerivedTensor.lean, line 642. References: SGA 5 VIII (8.1), “Noetherian case”; SGA 4½ Rapport (4.5.1).

Let Λ be a left Noetherian ring and let K be an object of D(Λ). Then K is perfect if and only if K has finite Tor dimension and Hⁱ(K) is a finite Λ-module for every i. This is StacksDraft.Perfect.isPerfect_iff_hasFiniteTorDimension_and_finite_homology with its parameter supplied by balancedDerivedTensoring, so no datum is assumed.

theorem isPerfect_iff_hasFiniteTorDimension_balancedDerivedTensoring
    [IsNoetherianRing Λ] [Small.{v} Λ] (K : DerivedCategory (ModuleCat.{v} Λ)) :
    IsPerfect K ↔
      (HasFiniteTorDimensionCanonical Λ K ∧
        ∀ i : ℤ,
          Module.Finite Λ ((DerivedCategory.homologyFunctor (ModuleCat.{v} Λ) i).obj K))

StacksDraft.Perfect.isPerfect_iff_hasFiniteTorDimension_and_finite_homology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/Perfect/FiniteTorDimension.lean, line 707. References: SGA 5 VIII (8.1), “Noetherian case”; SGA 4½ Rapport (4.5.1).

Let Λ be a left Noetherian ring and let K be an object of D(Λ). Then K is perfect if and only if K has finite Tor dimension and Hⁱ(K) is a finite Λ-module for every i.

theorem isPerfect_iff_hasFiniteTorDimension_and_finite_homology
    {Λ : Type u} [Ring Λ] [IsNoetherianRing Λ] [Small.{v} Λ]
    (D : BalancedDerivedTensoring.{u, v} Λ) (K : DerivedCategory (ModuleCat.{v} Λ)) :
    IsPerfect K ↔
      (HasFiniteTorDimension D K ∧
        ∀ i : ℤ,
          Module.Finite Λ ((DerivedCategory.homologyFunctor (ModuleCat.{v} Λ) i).obj K))
Sources
LeanStacksDraft.Perfect.HasFiniteTorDimensionCanonical · StacksDraft.Perfect.HasFiniteTorDimension · StacksDraft.Perfect.isPerfect_iff_hasFiniteTorDimension_balancedDerivedTensoring · StacksDraft.Perfect.isPerfect_iff_hasFiniteTorDimension_and_finite_homology

Section64.13 Cohomology of nice complexes#

Section 64.13 of the Stacks Project, Tag 0964. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TV, a proposition

Tag 03TV in the Stacks Project.

Stacks.EtaleCohomology.CurveGlobalSections.isPerfect, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveGlobalSections.lean, line 742. The attribute's comment: “from the hypercohomology spectral sequences hSS and hSSZ, the finiteness hFin of the étale cohomology of a constructible sheaf, the cohomological dimension hDimZ, the constructibility hPullback of a derived inverse image, and the projection formula with the Tor window hTwisting”.

Stacks 03TV. Let k be a field, let X be a projective curve over k, let Λ be a finite commutative ring and let K be an object of D_ctf(X_étale, Λ). Then the derived global sections RΓ(X_k̄, K) of the restriction of K to the geometric fibre X_k̄ = X ×_{Spec k} Spec k̄ form a perfect complex of Λ-modules.

The geometric fibre is the object Y of the big étale site, pinned down by _hbase, and the restriction of K to it is the bounded below complex Kbar, pinned down by eKbar. The proof is the one of the source: the hypercohomology spectral sequence hSS together with the finiteness hFin of the étale cohomology of a constructible sheaf gives finiteness of the cohomology modules, the projection formula contained in hTwisting together with the hypercohomology spectral sequence hSSZ and the cohomological dimension hDimZ gives finite Tor dimension, and the criterion of Tag 03TO concludes.

theorem isPerfect (Y : B.Scheme) (f : Y ⟶ X)
    (Dt : StacksDraft.Perfect.BalancedDerivedTensoring.{r, w} Λ)
    (hSS : HasHypercohomologySpectralSequence.{u, w, r} B Λ Y)
    (hSSZ : HasHypercohomologySpectralSequence.{u, w, 0} B ℤ Y)
    (hFin : HasFiniteConstructibleCohomology.{u, w, r} B Λ Y)
    (hDimZ : HasFiniteEtaleCohomologicalDimension.{u, w, 0} B ℤ Y)
    (hPullback : HasConstructibleDerivedPullback.{u, w, r} B Λ)
    (hTwisting : HasGeometricTwisting.{u, w, r, d} B X Λ T Y f Dt)
    {k : Type u} [Field k] (gk : X.obj ⟶ Spec (CommRingCat.of k))
    (_hcurve : IsCurve k gk) (_hprojective : IsProjective gk)
    (_hbase : ∃ e : Y.obj ≅ Stacks.Frobenius.fieldBaseChange (Over.mk gk) (AlgebraicClosure k),
      B.inclusion.map f = e.hom ≫ pullback.fst gk
        (Stacks.Frobenius.specAlgebraMap k (AlgebraicClosure k)))
    (K : ConstructibleFiniteTorDerivedCategory.{u, w, r, d} B X Λ T)
    (Kbar : DerivedCategory.Plus (SmallEtaleModuleSheaf.{u, w, r} B Λ Y))
    (eKbar : Nonempty (DerivedCategory.Plus.ι.obj Kbar ≅
      (smallEtaleModulePullback.{u, w, r} B Λ f).mapDerivedCategory.obj K.obj.obj)) :
    StacksDraft.Perfect.IsPerfect
      (DerivedCategory.Plus.ι.obj
        ((smallEtaleModuleDerivedGlobalSections.{u, w, r} B Λ Y).obj Kbar))

Declarations registered for the tag:

Sources
LeanStacks.EtaleCohomology.CurveGlobalSections.isPerfect · Stacks.EtaleCohomology.isPerfect_etaleModuleDerivedGlobalSections_fieldBaseChange_of_isCtf

Section64.14 Lefschetz numbers#

Section 64.14 of the Stacks Project, Tag 03TW. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03TX, a definition

Tag 03TX in the Stacks Project.

Stacks.EtaleCohomology.globalLefschetzNumber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GlobalLefschetzNumber.lean, line 72.

The global Lefschetz number of K: the trace of the action π_X^* on the perfect complex RΓ(X_k̄, K|_{X_k̄}), an element of the additive commutator quotient Λ^natural.

See Stacks Project, Tag 03TX.

public def globalLefschetzNumber (Λ : Type u) [Ring Λ] [Finite Λ]
    (D : FrobeniusActionOnCohomology.{u, v} Λ) :
    CategoryTheory.FilteredDerived.AdditiveCommutatorQuotient Λ

Stacks.EtaleCohomology.globalLefschetzNumberOfCtf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GlobalLefschetzNumberOfCtfTrace.lean, line 110.

Stacks, Tag 03TX: the global Lefschetz number of K. Let Λ be a finite, possibly noncommutative, ring, X a projective curve over a finite field k with p ^ q elements, k̄ an algebraic closure of k and K ∈ D_ctf(X, Λ). The base change c_K|_{X_k̄} of the canonical map c_K : π_X^{-1} K ⟶ K induces an action π_X^* on the perfect complex RΓ(X_k̄, K|_{X_k̄}); the global Lefschetz number of K is its trace Tr(π_X^* | RΓ(X_k̄, K|_{X_k̄})), an element of Λ^natural.

D_ctf(X, Λ) is Stacks.EtaleCohomology.IsCtf, which makes sense for a noncommutative Λ; an object of it is bounded, so it is taken in the bounded below derived category, on which RΓ(X_k̄, -) is defined. Perfectness of RΓ(X_k̄, K|_{X_k̄}) is [Stacks, Tag 03TV], proved, not assumed.

public def globalLefschetzNumberOfCtf (hcurve : IsCurve k gk)
    (hproj : IsProjective gk) (K : DerivedCategory.Plus (EtaleModules.{u, r} Λ X.obj))
    (hK : IsCtf.{u, r} B X Λ (DerivedCategory.Plus.ι.obj K)) :
    CategoryTheory.FilteredDerived.AdditiveCommutatorQuotient Λ
Tag 03TY, a definition

Tag 03TY in the Stacks Project.

Stacks.EtaleCohomology.localLefschetzNumberOfCtf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LocalLefschetzNumberConstructibleFlat.lean, line 265. The attribute's comment: “the local Lefschetz number of an object K of D_ctf(X_étale, Λ) on a scheme X over a finite field k: the sum over the k-rational points x of X of the traces of the geometric Frobenius π_x of 03SW on the stalk K_x̄, an element of the additive commutator quotient Λ^natural. Λ is the arbitrary finite, possibly noncommutative, ring of 03TX and 03SZ. X(k), the stalks K_x̄ and the actions π_x are all computed from K and X — K_x̄ is the derived étale stalk of K at the geometric point above x and π_x is the induced action of the geometric Frobenius — and perfection of each K_x̄ is derived from membership of D_ctf, as in the source. Membership of D_ctf(X_étale, Λ) is written as condition (2) of 03TT, that K be represented by a bounded complex of constructible flat sheaves of Λ-modules, which is also how SGA 4½ Rapport 4.6 defines D_ctf”. References: SGA 4½ Rapport (4.6), “D_ctf(X, Λ)”.

Stacks, Tag 03TY: the local Lefschetz number of K. For a finite field k with p ^ q elements, an algebraically closed extension k̄ of k, a scheme X over k with structure morphism f and finitely many k-rational points, an arbitrary finite — possibly noncommutative — coefficient ring Λ, and an object K of D_ctf(X_étale, Λ), this is the sum

∑_{x ∈ X(k)} Tr(π_x | K_x̄)

over the k-rational points of X of the traces of the geometric Frobenius π_x of [Stacks, Tag 03SW] on the derived stalk K_x̄ of K at the geometric point above x, an element of the additive commutator quotient Λ^natural.

Perfection of each stalk K_x̄, which the source reads off K ∈ D_ctf(X, Λ) through [Stacks, Tag 03TT], is proved here rather than supplied: it is AlgebraicGeometry.derivedEtaleModuleStalk_isPerfect_of_isRepresentedByConstructibleFlatComplex. Membership of D_ctf(X, Λ) is written as condition (2) of [Stacks, Tag 03TT], the condition that K be represented by a bounded complex of constructible flat sheaves of Λ-modules, which is also how [SGA 4½, Rapport 4.6] defines D_ctf; see the implementation notes of this file for why that is the formulation the source's generality on Λ calls for.

public def localLefschetzNumberOfCtf (hcard : Fintype.card k = p ^ q)
    (f : X.obj ⟶ Spec (.of k)) [Fintype (rationalPoints f)]
    (K : DerivedCategory
      (Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{w} Λ)))
    (hK : IsRepresentedByConstructibleFlatComplex.{u, w, r} B X Λ K) :
    CategoryTheory.FilteredDerived.AdditiveCommutatorQuotient Λ
Tag 03TZ, a theorem

Tag 03TZ in the Stacks Project.

Stacks.EtaleCohomology.LefschetzGaloisDescent.globalLefschetzNumber_eq_localLefschetzNumber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LefschetzTraceFormula.lean, line 989. The attribute's comment: “the global and local Lefschetz numbers agree, with the Galois decomposition of the trace on the open complement (Stacks 03UC and 03UD) and the annihilation of each coefficient trace by the order of its stabiliser (Stacks 03UB, and Weil's formula Stacks 03U1 through the absence of fixed points on the Galois cover) as hypotheses; the reductions of Steps 3 to 6 of Stacks 03UG are not formalized”.

The Lefschetz trace formula (Stacks 03TZ). Let X be a projective curve over a finite field k, let Λ be a finite ring and let K be an object of D_ctf(X, Λ). Then the global and local Lefschetz numbers of K are equal:

Tr(π_X^* | RΓ(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄)

in Λ^natural. The dévissage of RΓ(X_k̄, K) along the rational points of X splits the left hand side into the trace on the open complement of X(k) plus the right hand side, and the Galois descent of Stacks.EtaleCohomology.LefschetzGaloisDescent makes the trace on the open complement vanish.

public theorem globalLefschetzNumber_eq_localLefschetzNumber [Fintype points] :
    globalLefschetzNumber Λ D.globalDatum = localLefschetzNumber Λ points D.stalkDatum

Stacks.EtaleCohomology.globalLefschetzNumberOfCtf_eq_sum_rationalPointStalkTrace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ProjectiveCurveLefschetzTraceFormula.lean, line 93. The attribute's comment: “the Lefschetz trace formula for a projective curve over a finite field: global Lefschetz number (03TX) = sum over X(k) of the traces of the geometric Frobenius on the stalks, in Λ^natural, with K in D_ctf(X, Λ) given by a bounded below complex. Λ is a finite ring of cardinality prime to p, the standing hypothesis of the chapter fixed in 03SZ (trace.tex:386: 'Fix a finite ring Λ with cardinality prime to p'); the literal reading with an arbitrary finite Λ is false (k = F_5, E : y^2 = x^3 + 1 supersingular, Λ = Z/25, K = Λ: global number 1, local number #E(F_5) = 6). Λ : Type as in the formalization of 03UG”. References: SGA 4½ Rapport (3.2), “partial”; SGA 5 IIIB (1.3), “special case”.

Stacks, Tag 03TZ: the Lefschetz trace formula. Let X be a projective curve over a finite field k with p ^ q elements, k̄ an algebraic closure of k, Λ a finite, possibly noncommutative, ring of cardinality prime to p (the standing hypothesis of the chapter, fixed in [Stacks, Tag 03SZ]), and K ∈ D_ctf(X, Λ), given as a bounded below complex of sheaves of Λ-modules on X_étale whose class lies in D_ctf(X, Λ). Then the stalks K_x̄ at the rational points are perfect, and the global and local Lefschetz numbers of K are equal:

Tr(π_X^* | RΓ(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄) in Λ^natural.

The left hand side is the global Lefschetz number of [Stacks, Tag 03TX] (Stacks.EtaleCohomology.globalLefschetzNumberOfCtf); on the right K_x̄ is the stalk at the geometric point over x and π_x the geometric Frobenius of [Stacks, Tag 03SW] acting on it. Without the hypothesis #Λ prime to p the statement fails (see the module documentation).

theorem globalLefschetzNumberOfCtf_eq_sum_rationalPointStalkTrace (B : BigEtaleSite.{u})
    (X : B.Scheme) (Λ : Type) [Ring Λ] [Finite Λ] {k : Type u} [Field k] [Fintype k]
    (gk : X.obj ⟶ Spec (.of k)) (kbar : Type u) [Field kbar] [IsAlgClosed kbar] [Algebra k kbar]
    [Algebra.IsAlgebraic k kbar] (p q : ℕ) [Fact p.Prime] [CharP k p]
    (hcard : Fintype.card k = p ^ q) (hcop : Nat.Coprime (Nat.card Λ) p)
    (hcurve : IsCurve k gk) (hproj : IsProjective gk)
    (K : CochainComplex.Plus (EtaleModules.{u, 0} Λ X.obj))
    (hK : IsCtf.{u, 0} B X Λ (DerivedCategory.Plus.ι.obj (DerivedCategory.Plus.Q.obj K))) :
    letI : CharP kbar p := charP_of_injective_algebraMap (algebraMap k kbar).injective p
    ∃ hs : ∀ x : rationalPoints gk, StacksDraft.Perfect.IsPerfect
        (DerivedCategory.Q.obj (rationalPointStalkComplex.{u, 0} Λ kbar x.1 K)),
      globalLefschetzNumberOfCtf.{u, 0} B X Λ gk kbar p q hcard hcurve hproj
          (DerivedCategory.Plus.Q.obj K) hK =
        ∑ᶠ x : rationalPoints gk, perfectDerivedTrace Λ ⟨_, hs x⟩
          (DerivedCategory.Q.map (rationalPointStalkFrobenius.{u, 0} Λ kbar p q hcard x.1 K))
Tag 03U1, a theorem

Tag 03U1 in the Stacks Project.

Stacks.EtaleCohomology.JacobianCorrespondence.fixedPointNumber_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilTraceFormula.lean, line 187.

Weil's trace formula (Stacks 03U1). Let C be a nonsingular projective curve over an algebraically closed field k and φ : C → C a k-endomorphism of C distinct from the identity. Let V(φ) = Δ_C · Γ_φ, the intersection number on C × C of the diagonal with the graph of φ, let J = Pic⁰_{C/k} be the jacobian of C and φ^* : J → J the action induced by φ by taking pullbacks. Then V(φ) = 1 - Tr_J(φ^*) + deg φ.

public theorem fixedPointNumber_eq (D : W.EndomorphismData) :
    W.fixedPointNumber D = 1 - W.trace D.pullback + D.degree

AlgebraicGeometry.CurveGraph.fixedPointIntersection_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilTraceFormulaCurve.lean, line 124.

Stacks Project, Tag 03U1 (Weil). Let C be a smooth projective curve over an algebraically closed field k and φ : C ⟶ C a k-endomorphism distinct from the identity. Let V(φ) = (Δ · Γ_φ) be the intersection number of the diagonal and the graph of φ on C ×_k C. Then V(φ) = 1 - Tr_J(φ^*) + deg φ, where φ^* is the endomorphism of the Jacobian J = Pic⁰_{C/k} induced by pullback and Tr_J(φ^*) is its trace on the ℓ-adic Tate module of J, for any prime ℓ invertible in k (an integer independent of ℓ, see AlgebraicGeometry.CurveGraph.existsUnique_jacobianTrace).

theorem fixedPointIntersection_eq {k : Type u} [Field k] [IsAlgClosed k] {C : Scheme.{u}}
    (f : C ⟶ Spec (.of k)) [IsCurve k f] [Smooth f] [IsProper f]
    (hdim : topologicalKrullDim C ≤ 1) (φ : C ⟶ C) (w : φ ≫ f = f) (hφ : φ ≠ 𝟙 C)
    (ℓ : ℕ) [Fact ℓ.Prime] (hℓ : IsUnit (ℓ : k)) :
    ((fixedPointIntersection f hdim φ w : ℤ) : ℤ_[ℓ]) =
      1 - jacobianTateTrace f hdim φ w ℓ + (curveMapDegree f φ w : ℤ_[ℓ])
Tag 03U3, a lemma

Tag 03U3 in the Stacks Project.

Stacks.EtaleCohomology.sum_trace_etaleConstantCohomologyPullback_eq_fixedPointIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilFormulaEtaleCohomologyCurve.lean, line 56.

Weil's trace formula modulo ℓ^n (Stacks 03U3). Let C be a nonsingular projective curve over an algebraically closed field k, let φ : C → C be a k-endomorphism of C distinct from the identity, and let ℓ be a prime invertible in k. Then every étale cohomology module H^i(C, ℤ/ℓ^n) of the constant sheaf is free of finite rank over ℤ/ℓ^n, and

∑_{i=0}^{2} (-1)^i Tr(φ^* | H^i(C, ℤ/ℓ^n)) = V(φ) mod ℓ^n,

with V(φ) = Δ_C · Γ_φ the intersection number on C ×_k C (AlgebraicGeometry.CurveGraph.fixedPointIntersection), and φ^* the pullback on étale cohomology: restriction along φ followed by the canonical identification φ^{-1}(ℤ/ℓ^n) ≅ ℤ/ℓ^n.

The degreewise traces are 1, Tr_J(φ^*) mod ℓ^n and deg φ (Stacks.EtaleCohomology.sum_trace_etaleConstantCohomologyPullback_eq_toZModPow), and Weil's formula V(φ) = 1 - Tr_J(φ^*) + deg φ ([Stacks, Tag 03U1], AlgebraicGeometry.CurveGraph.fixedPointIntersection_eq) concludes.

theorem sum_trace_etaleConstantCohomologyPullback_eq_fixedPointIntersection
    {k : Type u} [Field k] [IsAlgClosed k] {C : Scheme.{u}} (f : C ⟶ Spec (.of k))
    [IsCurve k f] [Smooth f] [IsProper f] (φ : C ⟶ C) (w : φ ≫ f = f) (hφ : φ ≠ 𝟙 C)
    (ℓ : ℕ) [Fact ℓ.Prime] (hℓ : IsUnit (ℓ : k)) (n : ℕ) :
    (∀ i : ℕ, Module.Free (ZMod (ℓ ^ n))
        (Sheaf.H.{u + 1} (etaleConstantSheaf.{u, 0} C (ZMod (ℓ ^ n))) i) ∧
      Module.Finite (ZMod (ℓ ^ n))
        (Sheaf.H.{u + 1} (etaleConstantSheaf.{u, 0} C (ZMod (ℓ ^ n))) i)) ∧
    ∑ i ∈ Finset.range 3, (-1 : ZMod (ℓ ^ n)) ^ i * LinearMap.trace (ZMod (ℓ ^ n)) _
        ((etaleConstantCohomologyPullback φ (ZMod (ℓ ^ n)) i).toZModLinearMap (ℓ ^ n)) =
      (CurveGraph.fixedPointIntersection f (IsCurve.topologicalKrullDim_eq_one (f := f)).le φ w :
        ZMod (ℓ ^ n))

Stacks.EtaleCohomology.JacobianCorrespondence.EtaleFrobeniusAction.alternatingTrace_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilFormulaModPrimePower.lean, line 157. The attribute's comment: “the alternating sum of the traces on the étale cohomology of the curve is the fixed point number V(φ) modulo ℓ^n, with the three degreewise traces — 1 in degree zero, Tr_J(φ^*) in degree one and deg φ in degree two — as hypotheses, the situation of Stacks 03U1 being the JacobianCorrespondence datum”.

Weil's trace formula modulo ℓ^n (Stacks 03U3). In the situation of Weil's theorem, Tag 03U1, let ℓ be a prime invertible in k. Then

∑_{i=0}^{2} (-1)^i Tr(φ^* | H^i(C, Z/ℓ^n Z)) = V(φ) mod ℓ^n,

the alternating sum of the traces of φ^* on the étale cohomology of C with coefficients in Z/ℓ^n Z being 1 - Tr_J(φ^*) + deg φ by the three degreewise computations carried by Stacks.EtaleCohomology.JacobianCorrespondence.EtaleFrobeniusAction, and that being V(φ) by Weil's formula.

public theorem alternatingTrace_eq :
    T.alternatingTrace = (W.fixedPointNumber D : ZMod (ℓ ^ n))
Sources
LeanStacks.EtaleCohomology.globalLefschetzNumber · Stacks.EtaleCohomology.globalLefschetzNumberOfCtf · Stacks.EtaleCohomology.localLefschetzNumberOfCtf · Stacks.EtaleCohomology.LefschetzGaloisDescent.globalLefschetzNumber_eq_localLefschetzNumber · Stacks.EtaleCohomology.globalLefschetzNumberOfCtf_eq_sum_rationalPointStalkTrace · Stacks.EtaleCohomology.JacobianCorrespondence.fixedPointNumber_eq · AlgebraicGeometry.CurveGraph.fixedPointIntersection_eq · Stacks.EtaleCohomology.sum_trace_etaleConstantCohomologyPullback_eq_fixedPointIntersection

Section64.15 Preliminaries and sorites#

Section 64.15 of the Stacks Project, Tag 03U4. 10 tags here are carried by 15 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03U5, a lemma

Tag 03U5 in the Stacks Project.

Stacks.Trace.epsilon_comp_mk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/GroupTrace.lean, line 119. References: SGA 4½ Rapport (5.5), “ε factorization”.

The chosen coefficient-of-the-identity map factors the map on the group ring.

theorem epsilon_comp_mk (R : Type u) (G : Type v) [Ring R] [Group G] :
    (epsilon R G).comp (additiveCommutatorQuotientMk R[G]) =
      coeffOneToAdditiveCommutatorQuotient R G
Tag 03U6, a definition

Tag 03U6 in the Stacks Project.

Stacks.Trace.groupTrace, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/GroupTrace.lean, line 143. References: SGA 4½ Rapport (5.5), “tr_Λ^H definition”.

The group trace of an endomorphism of a finite projective group-ring module.

noncomputable abbrev groupTrace (R : Type u) (G : Type v) [Ring R] [Group G]
    (P : Type w) [AddCommGroup P] [Module R[G] P] [Module.Finite R[G] P]
    [Module.Projective R[G] P] (f : Module.End R[G] P) :
    AdditiveCommutatorQuotient R
Tag 03U7, a lemma

Tag 03U7 in the Stacks Project.

Stacks.Trace.projectiveModuleTrace_restrictScalars_groupAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/RestrictScalars.lean, line 200. References: SGA 4½ Rapport (5.6); SGA 5 IIIB (5.10.11), “A = K = R”; SGA 5 IIIB (5.13), “(1), special case”; SGA 5 IIIB (6.7), “special case”.

Stacks Project, Tag 03U7. The coefficient-ring trace of an endomorphism of a finite projective module over the group algebra of a finite group is the order of the group times its group trace.

theorem projectiveModuleTrace_restrictScalars_groupAlgebra
    (R : Type u) (G : Type v) (P : Type w) [Ring R] [Group G] [Finite G]
    [AddCommGroup P] [Module R[G] P]
    [Module.Finite R[G] P] [Module.Projective R[G] P]
    (f : Module.End R[G] P) :
    letI : Module R P := Module.compHom P
      (MonoidAlgebra.singleOneRingHom (R := R) (M := G))
    letI : Module.Finite R P := finite_restrictScalars_groupAlgebra R G P
    letI : Module.Projective R P := projective_restrictScalars_groupAlgebra R G P
    let fR : Module.End R P :=
      { f with
        map_smul' := by
          intro r p
          exact f.map_smul (MonoidAlgebra.singleOneRingHom (R := R) (M := G) r) p }
    projectiveModuleTrace R P fR =
      (Nat.card G) • groupTrace R G P f
Tag 03U8, a lemma

Tag 03U8 in the Stacks Project.

Stacks.Trace.inducedAdditiveCommutatorQuotientModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/QuotientModule.lean, line 67.

A central map A → Λ induces an A-module structure on the additive commutator quotient of Λ.

noncomputable def inducedAdditiveCommutatorQuotientModule
    (A Λ : Type*) [CommRing A] [Ring Λ] [Algebra A Λ] :
    InducedAdditiveCommutatorQuotientModule A Λ
Tag 03U9, a lemma

Tag 03U9 in the Stacks Project.

Stacks.Trace.diagonalAction_module_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/DiagonalAction.lean, line 403. The attribute's comment: “finiteness”.

A tensor product with diagonal action is finite over the group algebra when both input modules are finite over their respective rings.

lemma diagonalAction_module_finite
    {A : Type uA} {Λ : Type uΛ} {G : Type uG} {P : Type uP} {M : Type uM}
    [CommRing A] [Ring Λ] [Algebra A Λ] [Group G]
    [AddCommGroup P] [Module A P]
    [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower A Λ M]
    (ρ : _root_.Representation A G P) (σ : _root_.Representation Λ G M)
    [Module.Finite A[G] (Representation.asModuleNC ρ)] [Module.Finite Λ M] :
    Module.Finite Λ[G] (Representation.asModuleNC (Representation.tprodAlgebra ρ σ))

Stacks.Trace.diagonalAction_module_projective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Preliminaries/DiagonalAction.lean, line 972. The attribute's comment: “projectivity”. References: SGA 4½ Rapport (5.7), “more general”; SGA 4½ Rapport (5.9), “P⊗M projective”.

A tensor product with diagonal action is projective over the group algebra when the first input is projective over its group algebra and the second is projective over the coefficient ring.

lemma diagonalAction_module_projective
    {A : Type uA} {Λ : Type uΛ} {G : Type uG} {P : Type uP} {M : Type uM}
    [CommRing A] [Ring Λ] [Algebra A Λ] [Group G]
    [AddCommGroup P] [Module A P]
    [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower A Λ M]
    (ρ : _root_.Representation A G P) (σ : _root_.Representation Λ G M)
    [Module.Projective A[G] (Representation.asModuleNC ρ)] [Module.Projective Λ M] :
    Module.Projective Λ[G]
      (Representation.asModuleNC (Representation.tprodAlgebra ρ σ))
Tag 03UA, a lemma

Tag 03UA in the Stacks Project.

Stacks.Trace.groupTrace_diagonalTensorEndomorphism, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Multiplicativity.lean, line 546. References: SGA 4½ Rapport (5.8); SGA 5 IIIB (5.12), “special case”; SGA 6 I (8.6), “Punctual (affine) case”.

The group trace is multiplicative for the diagonal tensor product action.

lemma groupTrace_diagonalTensorEndomorphism
    {A : Type uA} {Λ : Type uΛ} {G : Type uG} {P : Type uP} {M : Type uM}
    [CommRing A] [Ring Λ] [Algebra A Λ] [Group G]
    [AddCommGroup P] [Module A P]
    [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower A Λ M]
    (ρ : _root_.Representation A G P) (σ : _root_.Representation Λ G M)
    [Module.Finite A[G] (asModuleNC ρ)] [Module.Projective A[G] (asModuleNC ρ)]
    [Module.Finite Λ M] [Module.Projective Λ M]
    (u : Module.End A[G] (asModuleNC ρ))
    (v : Module.End Λ[G] (asModuleNC σ)) :
    diagonalTensorGroupTrace ρ σ u v =
      commutativeAdditiveCommutatorQuotientEval A
          (groupTrace A G (asModuleNC ρ) u) •
      projectiveModuleTrace Λ M
          (groupAlgebraEnd_restrictScalars σ v)
Tag 03UB, a lemma

Tag 03UB in the Stacks Project.

Stacks.Trace.trace_eq_card_centralizer_nsmul_groupTrace, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Centralizer.lean, line 331. References: SGA 4½ Rapport (5.9), “(5.9.1)”.

The ordinary trace is the centralizer order times the centralizer trace.

lemma trace_eq_card_centralizer_nsmul_groupTrace (i : G →* Γ)
    [Module.Finite Λ[G] (restrictedModule Λ P i)]
    [Module.Projective Λ[G] (restrictedModule Λ P i)]
    (γ : Γ) :
    letI : Module.Finite Λ (coefficientModule Λ Γ P) :=
      finite_over_coefficients (P := P) i
    letI : Module.Projective Λ (coefficientModule Λ Γ P) :=
      projective_over_coefficients (P := P) i
    projectiveModuleTrace Λ (coefficientModule Λ Γ P)
      (coefficientEndomorphism (P := P) γ).val =
      Nat.card (centralizer i γ) • centralizerTrace (P := P) i γ
Tag 03UC, a lemma

Tag 03UC in the Stacks Project.

Stacks.Trace.MonoidExtensionByNat.diagonalTensorCentralizerTrace_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/CentralizerMultiplicativity.lean, line 79. References: SGA 4½ Rapport (5.9), “(5.9.2)”; SGA 5 IIIB (5.12), “special case”; SGA 6 I (8.6), “Punctual (affine) case”.

The centralizer trace is multiplicative for the diagonal action on a tensor product.

theorem MonoidExtensionByNat.diagonalTensorCentralizerTrace_eq
    {A : Type uA} {Λ : Type uΛ} {G : Type uG} {Γ : Type uΓ} {P : Type uP} {M : Type uM}
    [CommRing A] [Ring Λ] [Algebra A Λ] [Group G] [Finite G] [Monoid Γ]
    [AddCommGroup P] [Module A P]
    [AddCommGroup M] [Module A M] [Module Λ M] [IsScalarTower A Λ M]
    (E : MonoidExtensionByNat G Γ)
    (ρ : _root_.Representation A Γ P) (σ : _root_.Representation Λ Γ M)
    [Module.Finite A[G] (asModuleNC (restrictedRepresentation E ρ))]
    [Module.Projective A[G] (asModuleNC (restrictedRepresentation E ρ))]
    [Module.Finite Λ M] [Module.Projective Λ M]
    (γ : Γ) :
    E.diagonalTensorCentralizerTrace ρ σ γ =
      commutativeAdditiveCommutatorQuotientEval A (E.centralizerTrace ρ γ) •
        projectiveModuleTrace Λ M (σ γ)
Tag 03UD, a lemma

Tag 03UD in the Stacks Project.

Stacks.Trace.coinvariantRepresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Coinvariants.lean, line 157. The attribute's comment: “the action on coinvariants”. References: SGA 4½ Rapport (5.10), “action of G^+ on P_H”.

The canonical action of the quotient monoid ℕ on the coinvariants. Its specification records compatibility with every lift in Γ.

noncomputable def coinvariantRepresentation (E : MonoidExtensionByNat G Γ)
    [AddCommGroup P] [Module Λ P] (ρ : _root_.Representation Λ Γ P) :
    { σ : _root_.Representation Λ (Multiplicative ℕ)
        (coinvariants (restrictedRepresentation E ρ)) //
      ∀ (γ : Γ) (p : P),
        σ (E.degree γ) (coinvariantsMk (restrictedRepresentation E ρ) p) =
          coinvariantsMk (restrictedRepresentation E ρ) (ρ γ p) }

Stacks.Trace.coinvariants_module_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Coinvariants.lean, line 471. The attribute's comment: “finiteness of the coinvariants”.

The coinvariants of a finite Λ[G]-projective representation are finite over Λ.

lemma coinvariants_module_finite
    [AddCommGroup P] [Module Λ P] (σ : _root_.Representation Λ G P)
    [Module.Finite Λ[G] (Representation.asModuleNC
      σ)] :
    Module.Finite Λ (coinvariants σ)

Stacks.Trace.coinvariants_module_projective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Coinvariants.lean, line 535. The attribute's comment: “projectivity of the coinvariants”. References: SGA 4½ Rapport (5.10), “P_H projective over Λ”.

The coinvariants of a finite Λ[G]-projective representation are projective over Λ.

lemma coinvariants_module_projective
    [AddCommGroup P] [Module Λ P] (σ : _root_.Representation Λ G P)
    [Module.Projective Λ[G] (Representation.asModuleNC
      σ)] :
    Module.Projective Λ (coinvariants σ)

Stacks.Trace.trace_degreeOne_on_coinvariants, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/Coinvariants.lean, line 927. The attribute's comment: “the trace identity”. References: SGA 4½ Rapport (5.11).

The trace of degree one on the coinvariants is the sum of the centralizer traces over the G-conjugacy classes of degree-one elements.

lemma trace_degreeOne_on_coinvariants [Finite G] (E : MonoidExtensionByNat G Γ)
    [AddCommGroup P] [Module Λ P] (ρ : _root_.Representation Λ Γ P)
    [Module.Finite Λ[G] (Representation.asModuleNC
      (restrictedRepresentation E ρ))]
    [Module.Projective Λ[G] (Representation.asModuleNC
      (restrictedRepresentation E ρ))]
    (S : Finset Γ) (hS : IsConjugacyClassRepresentatives E (.ofAdd 1) S) :
    letI := coinvariants_module_finite (restrictedRepresentation E ρ)
    letI := coinvariants_module_projective (restrictedRepresentation E ρ)
    projectiveModuleTrace Λ (coinvariants (restrictedRepresentation E ρ))
        ((coinvariantRepresentation E ρ).val (.ofAdd 1)) =
      ∑ γ ∈ S, MonoidExtensionByNat.centralizerTrace E ρ γ
Tag 03UE, a remark

Tag 03UE in the Stacks Project.

Stacks.Trace.isZero_groupHomology_trivial_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/TrivialTraceFormula.lean, line 55. The attribute's comment: “the vanishing of the homology of G in positive degrees”.

The homology of a finite group with coefficients in the trivial module given by a field in which the order of the group is invertible vanishes in positive degrees.

theorem isZero_groupHomology_trivial_succ (Λ : Type u) (G : Type u) [Field Λ] [Group G]
    [Finite G] [NeZero (Nat.card G : Λ)] (n : ℕ) :
    Limits.IsZero (groupHomology (Rep.trivial Λ G Λ) (n + 1))

Stacks.Trace.sum_inv_card_centralizer_degreeOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Trace/Sorites/TrivialTraceFormula.lean, line 68. The attribute's comment: “the trivial trace formula”.

The reciprocals of the orders of the centralizers of the degree-one elements of the extension monoid, summed over their G-conjugacy classes, add up to 1 in any field in which the order of G is invertible.

theorem sum_inv_card_centralizer_degreeOne {Λ : Type u} {G : Type v} {Γ : Type w} [Field Λ]
    [Group G] [Finite G] [Monoid Γ] [NeZero (Nat.card G : Λ)] (E : MonoidExtensionByNat G Γ)
    (S : Finset Γ) (hS : IsConjugacyClassRepresentatives E (.ofAdd 1) S) :
    ∑ γ ∈ S, (Nat.card (centralizer E.inclusion γ) : Λ)⁻¹ = 1

Declarations registered for the tag:

Sources
LeanStacks.Trace.epsilon_comp_mk · Stacks.Trace.groupTrace · Stacks.Trace.projectiveModuleTrace_restrictScalars_groupAlgebra · Stacks.Trace.inducedAdditiveCommutatorQuotientModule · Stacks.Trace.diagonalAction_module_finite · Stacks.Trace.diagonalAction_module_projective · Stacks.Trace.groupTrace_diagonalTensorEndomorphism · Stacks.Trace.trace_eq_card_centralizer_nsmul_groupTrace

Section64.16 Proof of the trace formula#

Section 64.16 of the Stacks Project, Tag 03UF. 3 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03UG, a theorem

Tag 03UG in the Stacks Project.

Stacks.EtaleCohomology.exists_compactification_and_traceFormulaUpToDim_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaCtf.lean, line 78.

[Stacks, Tag 03UG]: the trace formula for curves. Let k be a finite field with #k = p ^ q, k̄ an algebraic closure of k, and Λ a finite ring whose cardinality is prime to that of k. Every separated scheme X of finite type over k of dimension at most one has a compactification over k, and for every compactification j of X and every K ∈ D_ctf(X, Λ), RΓ_c(X_k̄, K) (computed through j) and the stalks K_x̄ at the rational points are perfect and

Tr(π_X^* | RΓ_c(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄)

in Λ^♮.

theorem exists_compactification_and_traceFormulaUpToDim_one (B : BigEtaleSite.{u}) (Λ : Type)
    [Ring Λ] [Finite Λ] {k : Type u} [Field k] [Fintype k] (kbar : Type u) [Field kbar]
    [IsAlgClosed kbar] [Algebra k kbar] [Algebra.IsAlgebraic k kbar] (p q : ℕ) [Fact p.Prime]
    [CharP k p] [CharP kbar p] (hcard : Fintype.card k = p ^ q)
    (hcop : Nat.Coprime (Nat.card Λ) (Fintype.card k)) :
    (∀ (X : B.Scheme) (f : X.obj ⟶ Spec (.of k)) [QuasiCompact f] [LocallyOfFiniteType f]
      [IsSeparated f], topologicalKrullDim X.obj ≤ ((1 : ℕ) : WithBot ℕ∞) →
      Nonempty (CompactificationOf (Over.mk f))) ∧
    TraceFormulaUpToDim B Λ kbar p q hcard 1

Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_localLefschetzNumber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaDimensionOne.lean, line 313. The attribute's comment: “RESTRICTED: 03UH with both sides built from the scheme; the extra hypotheses are 03TV as hperf and hstalkPerfect (K is a bounded below complex of étale sheaves of modules rather than an object of the D_ctf of 03TQ: the two small étale sites are identified by SmallEtale.sheafEquiv, but the transport of finite Tor dimension across it and the direction (1) => (2) of 03TT are missing), finiteness of X(k), the Step 1 dévissage with the identification of its pieces (devissage, hglobal, hstalk), and the Steps 7 to 9 Galois decomposition feeding 03TZ (hdecomposition, hdivisible, hannihilate, hlevel); Steps 3 to 6 are not formalized”.

The trace formula in dimension at most one (Stacks 03UG). Let k be a finite field with p ^ q elements, let k̄ be an algebraically closed extension of k, let X be a separated scheme of finite type over k of dimension at most one, let Λ be a finite ring whose cardinality is prime to that of k, and let K be a bounded below complex of sheaves of Λ-modules on the small étale site of X. Then

Tr(π_X^* | RΓ_c(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄)

in Λ^natural, the left hand side being the trace of the action induced on RΓ_c(X_k̄, K|_{X_k̄}) by an extension of the geometric Frobenius π_X × id of [Stacks, Tag 03SQ] to a compactification of X_k̄ over Spec k̄, and the right hand side the sum over the rational points of the traces of the geometric Frobenius of [Stacks, Tag 03SW] on the stalks of K at the geometric points above them.

Perfectness of RΓ_c(X_k̄, K|_{X_k̄}) and of each stalk, finiteness of X(k), the dévissage of Step 1 of the source with the identification of its graded pieces, and the Galois decomposition of Steps 7 to 9 are hypotheses; the implementation notes of this file record what each of them is and what remains unformalized.

public theorem compactSupportLefschetzNumber_eq_localLefschetzNumber
    {k : Type u} [Field k] [Fintype k] {p q : ℕ} [Fact p.Prime] [CharP k p]
    (hcard : Fintype.card k = p ^ q) (Y : Over (Spec (.of k)))
    [IsSeparated Y.hom] [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom]
    (_hdim : topologicalKrullDim Y.left ≤ 1)
    (kbar : Type u) [Field kbar] [IsAlgClosed kbar] [Algebra k kbar] [CharP kbar p]
    (Λ : Type r) [Ring Λ] [Finite Λ]
    (_hcoprime : Nat.Coprime (Nat.card Λ) (Fintype.card k))
    (K : CochainComplex.Plus (EtaleModules.{u, r} Λ Y.left))
    [Fintype (rationalPoints Y.hom)]
    (j : CompactificationOf
      (Over.mk (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar))))
    (E : CompactificationEndomorphism j
      (Stacks.Frobenius.geometricFrobeniusBaseChange Y kbar p q hcard))
    (γ : 𝟭 (DerivedCategory.Plus (EtaleModules.{u, r} Λ j.space)) ⟶
      etaleModuleDerivedDirectImage.{u, r} Λ E.hom)
    (hperf : StacksDraft.Perfect.IsPerfect (DerivedCategory.Plus.ι.obj
      ((compactlySupportedCohomology.{u, r} kbar
          (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar)) j Λ).obj
        (baseChangeCoefficients.{u, r} Λ Y kbar K))))
    (hstalkPerfect : ∀ x : rationalPoints Y.hom, StacksDraft.Perfect.IsPerfect
      (DerivedCategory.Q.obj (rationalPointStalkComplex.{u, r} Λ kbar x.1 K)))
    (devissage : LefschetzDevissage.{r, max (u + 1) r, u} Λ (rationalPoints Y.hom))
    (hglobal : devissage.globalDatum =
      frobeniusActionOnCompactSupport.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf)
    (hstalk : devissage.stalkDatum =
      geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect)
    (group : Type t) [Fintype group] (prime exponent level : ℕ)
    (stabilizerExponent : group → ℕ) (coefficientTrace : group → ℤ)
    (moduleTrace : group → AdditiveCommutatorQuotient Λ)
    (hprime : Nat.Prime prime)
    (hannihilate : ∀ y : AdditiveCommutatorQuotient Λ, ((prime : ℤ) ^ exponent) • y = 0)
    (hlevel : ∀ g : group, stabilizerExponent g + exponent ≤ level)
    (hdecomposition : globalLefschetzNumber Λ devissage.openDatum =
      ∑ g : group, coefficientTrace g • moduleTrace g)
    (hdivisible : ∀ g : group, ((prime : ℤ) ^ level) ∣
      ((prime : ℤ) ^ stabilizerExponent g) * coefficientTrace g) :
    compactSupportLefschetzNumber.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf =
      localLefschetzNumber Λ (rationalPoints Y.hom)
        (geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect)
Tag 03UI, a remark

Tag 03UI in the Stacks Project.

Stacks.EtaleCohomology.compactificationFieldBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCompactification.lean, line 133. The attribute's comment: “item (2): the base change X̄_k̄ of a compactification X̄ of X over k is a compactification of X_k̄ over k̄, which is where RΓ_c(X_k̄, -) is formed”.

The base change X̄_k̄ of a compactification of X over k, as a compactification of X_k̄ over k̄: the fibre product X̄ ×_{Spec k} Spec k̄ is proper over Spec k̄ because X̄ is proper over Spec k, and X_k̄ ⟶ X̄_k̄ is an open immersion because X ⟶ X̄ is one. This is the ambient scheme the source takes RΓ_c(X_k̄, -) on.

public def compactificationFieldBaseChange :
    CompactificationOf (Over.mk (pullback.snd f (Stacks.Frobenius.specAlgebraMap k kbar)))

Stacks.EtaleCohomology.geometricCompactSupportCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCompactification.lean, line 159. The attribute's comment: “item (2): RΓ_c(X_k̄, K) := RΓ(X̄_k̄, j_! K) for a chosen compactification j of X over k, taken through its base change”.

The complex RΓ_c(X_k̄, K) = RΓ(X̄_k̄, j_! K) of the source: cohomology with compact support of a bounded below complex of sheaves of Λ-modules on the small étale site of the base change X_k̄, formed through the base change X̄_k̄ of a compactification X̄ of X over k. The compactification is an argument, not a choice.

public abbrev geometricCompactSupportCohomology :
    DerivedCategory.Plus
        (EtaleModules.{u, r} Λ (pullback f (Stacks.Frobenius.specAlgebraMap k kbar))) ⥤
      DerivedCategory.Plus (ModuleCat.{max (u + 1) r} Λ)

Stacks.EtaleCohomology.geometricCompactSupportCohomologyGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCompactification.lean, line 169. The attribute's comment: “item (2): H^i_c(X_k̄, K) is the i-th cohomology of RΓ_c(X_k̄, K)”.

The module H^i_c(X_k̄, K): the i-th cohomology of RΓ_c(X_k̄, K).

public abbrev geometricCompactSupportCohomologyGroup (i : ℤ) :
    DerivedCategory.Plus
        (EtaleModules.{u, r} Λ (pullback f (Stacks.Frobenius.specAlgebraMap k kbar))) ⥤
      ModuleCat.{max (u + 1) r} Λ

Stacks.EtaleCohomology.geometricCompactSupportComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCompactification.lean, line 201. The attribute's comment: “item (2): RΓ_c(X_k̄, -) is independent of the compactification, reduced to the independence of Rf_! of 0F7I, which is a hypothesis here”.

Independence of the compactification. An isomorphism of the derived lower shriek functors attached to two compactifications of X over k, which is [Stacks, Tag 0F7I], induces an isomorphism of the complexes RΓ_c(X_k̄, -) they present, natural in the coefficient complex.

public def geometricCompactSupportComparison
    (e : geometricLowerShriek.{u, r} f j₁ kbar Λ ≅ geometricLowerShriek.{u, r} f j₂ kbar Λ) :
    geometricCompactSupportCohomology.{u, r} f j₁ kbar Λ ≅
      geometricCompactSupportCohomology.{u, r} f j₂ kbar Λ

Stacks.EtaleCohomology.geometricCompactSupportGroupComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCompactification.lean, line 233. The attribute's comment: “item (2): H^i_c(X_k̄, -) is independent of the compactification, induced by the comparison of the complexes”.

Independence of the compactification for H^i_c. The comparison of the complexes induces an isomorphism of the modules H^i_c(X_k̄, -) in every degree, natural in the coefficient complex.

public def geometricCompactSupportGroupComparison
    (e : geometricLowerShriek.{u, r} f j₁ kbar Λ ≅ geometricLowerShriek.{u, r} f j₂ kbar Λ)
    (i : ℤ) :
    geometricCompactSupportCohomologyGroup.{u, r} f j₁ kbar Λ i ≅
      geometricCompactSupportCohomologyGroup.{u, r} f j₂ kbar Λ i

Stacks.EtaleCohomology.geometricCompactSupportCanonicalComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricCompactSupportCanonicalComparison.lean, line 217. The attribute's comment: “(2): independence of the compactification -- RΓ_c(X_k̄, -) = RΓ(X̄_k̄, j_! -) does not depend on the compactification X̄ of X over k of dimension at most one (proper, which a projective X̄ is): canonical isomorphism through the closure of X in X̄₁ ×_k X̄₂”.

Remark 03UI (2): RΓ_c(X_k̄, -) is independent of the compactification. Let k be a field, X a separated scheme of finite type over k, k̄ an extension field of k and Λ a ring. For any two compactifications X ⟶ X̄₁ and X ⟶ X̄₂ of X over k (open immersions into proper k-schemes, which projective ones are) of dimension at most one, the complexes RΓ(X̄₁_k̄, j₁! K) and RΓ(X̄₂_k̄, j₂! K) are canonically isomorphic, naturally in the bounded below complex K of sheaves of Λ-modules on X_k̄. The isomorphism is induced by the canonical isomorphism geometricLowerShriekCanonicalIso of the derived lower shriek functors, through the closure of X in X̄₁ ×_k X̄₂.

The coefficient ring is taken in Type (universe 0), as in the companion results of Tags 03VK and 03VL: integral base change for sheaves of modules, through which the finite projections of the dominating compactification are handled, is available at that universe. A finite ring, the coefficient ring of the source, is isomorphic to one in Type.

def geometricCompactSupportCanonicalComparison :
    geometricCompactSupportCohomology.{u, 0} f c₁ kbar Λ ≅
      geometricCompactSupportCohomology.{u, 0} f c₂ kbar Λ

Stacks.EtaleCohomology.geometricCompactSupportGroupCanonicalComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricCompactSupportCanonicalComparison.lean, line 229. The attribute's comment: “(2): independence of the compactification -- H^i_c(X_k̄, -) does not depend on the compactification X̄ of X over k of dimension at most one, in every degree”.

Remark 03UI (2): H^i_c(X_k̄, -) is independent of the compactification, in every degree, naturally in the coefficient complex: the isomorphism induced on cohomology by geometricCompactSupportCanonicalComparison. The coefficient ring is taken in Type, as in geometricCompactSupportCanonicalComparison.

def geometricCompactSupportGroupCanonicalComparison (i : ℤ) :
    geometricCompactSupportCohomologyGroup.{u, 0} f c₁ kbar Λ i ≅
      geometricCompactSupportCohomologyGroup.{u, 0} f c₂ kbar Λ i

Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_localLefschetzNumber_of_galoisDescent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaAnyDimension.lean, line 84. The attribute's comment: “item (1) RESTRICTED: the 03UG identity with no bound on the dimension of X, from the Step 1 devissage with its identifications (devissage, hglobal, hstalk) and the Steps 7 to 9 Galois descent of 03TZ; the source's reduction of the general case to dimension one is not here”.

The trace formula in any dimension (Stacks 03UI, item (1)). Let k be a finite field with p ^ q elements, let k̄ be an algebraically closed extension of k, let X be a separated scheme of finite type over k — of arbitrary dimension — let Λ be a finite ring whose cardinality is prime to that of k, and let K be a bounded below complex of sheaves of Λ-modules on the small étale site of X. Then

Tr(π_X^* | RΓ_c(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄)

in Λ^natural, given the dévissage of RΓ_c(X_k̄, K) along the rational points with the identification of its graded pieces and the Galois descent of Steps 7 to 9 of the source. The bound topologicalKrullDim X ≤ 1 of Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_localLefschetzNumber plays no part in the deduction and is absent here.

public theorem compactSupportLefschetzNumber_eq_localLefschetzNumber_of_galoisDescent
    {k : Type u} [Field k] [Fintype k] {p q : ℕ} [Fact p.Prime] [CharP k p]
    (hcard : Fintype.card k = p ^ q) (Y : Over (Spec (.of k)))
    [IsSeparated Y.hom] [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom]
    (kbar : Type u) [Field kbar] [IsAlgClosed kbar] [Algebra k kbar] [CharP kbar p]
    (Λ : Type r) [Ring Λ] [Finite Λ]
    (_hcoprime : Nat.Coprime (Nat.card Λ) (Fintype.card k))
    (K : CochainComplex.Plus (EtaleModules.{u, r} Λ Y.left))
    [Fintype (rationalPoints Y.hom)]
    (j : CompactificationOf
      (Over.mk (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar))))
    (E : CompactificationEndomorphism j
      (Stacks.Frobenius.geometricFrobeniusBaseChange Y kbar p q hcard))
    (γ : 𝟭 (DerivedCategory.Plus (EtaleModules.{u, r} Λ j.space)) ⟶
      etaleModuleDerivedDirectImage.{u, r} Λ E.hom)
    (hperf : StacksDraft.Perfect.IsPerfect (DerivedCategory.Plus.ι.obj
      ((compactlySupportedCohomology.{u, r} kbar
          (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar)) j Λ).obj
        (baseChangeCoefficients.{u, r} Λ Y kbar K))))
    (hstalkPerfect : ∀ x : rationalPoints Y.hom, StacksDraft.Perfect.IsPerfect
      (DerivedCategory.Q.obj (rationalPointStalkComplex.{u, r} Λ kbar x.1 K)))
    (devissage : LefschetzDevissage.{r, max (u + 1) r, u} Λ (rationalPoints Y.hom))
    (hglobal : devissage.globalDatum =
      frobeniusActionOnCompactSupport.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf)
    (hstalk : devissage.stalkDatum =
      geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect)
    (group : Type t) [Fintype group]
    (descent : LefschetzGaloisDescent.{r, max (u + 1) r, u, t} Λ devissage group) :
    compactSupportLefschetzNumber.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf =
      localLefschetzNumber Λ (rationalPoints Y.hom)
        (geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect)

Stacks.EtaleCohomology.canonicalTraceFormula_of_isCtf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaAnyDimensionCtf.lean, line 52. The attribute's comment: “(1): the trace formula in any dimension: Tag 03UG for X separated of finite type over k with no bound on its dimension, through every compactification. Λ : Type (universe 0), see the module docstring.”.

The trace formula in any dimension ([Stacks, Tag 03UI] (1)). Let k be a finite field with p ^ q elements and k̄ an algebraic closure, X a separated scheme of finite type over k of any dimension, Λ a finite ring whose cardinality is prime to that of k, and K ∈ D_ctf(X, Λ). Then for every compactification j : X ⟶ X̄ over k, the complex RΓ_c(X_k̄, K) = RΓ(X̄_k̄, (j_! K)|_{X̄_k̄}) and the stalks K_x̄ at the rational points are perfect, and Tr(π_X^* | RΓ_c(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄) in Λ^natural, for the canonical Frobenius actions (Stacks.EtaleCohomology.CanonicalTraceFormula). The coefficient ring is in Type (see the module docstring).

theorem canonicalTraceFormula_of_isCtf (B : BigEtaleSite.{u}) (Λ : Type) [Ring Λ] [Finite Λ]
    {k : Type u} [Field k] [Fintype k] (kbar : Type u) [Field kbar] [IsAlgClosed kbar]
    [Algebra k kbar] [Algebra.IsAlgebraic k kbar] (p q : ℕ) [Fact p.Prime] [CharP k p]
    [CharP kbar p] (hcard : Fintype.card k = p ^ q)
    (hcop : Nat.Coprime (Nat.card Λ) (Fintype.card k))
    (X : B.Scheme) (f : X.obj ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] (K : CochainComplex.Plus (EtaleModules.{u, 0} Λ X.obj))
    (hK : IsCtf B X Λ (DerivedCategory.Q.obj K.obj)) (j : CompactificationOf (Over.mk f)) :
    CanonicalTraceFormula Λ kbar p q hcard f j K
Tag 03UJ, a remark

Tag 03UJ in the Stacks Project.

Stacks.EtaleCohomology.localLefschetzNumber_constantStalkDatum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantCoefficientTraceFormula.lean, line 102. The attribute's comment: “with constant coefficients the right hand side of 03UG collapses to #X(k) times the trace at one rational point, which is the point count Weil's formula 03U1 computes”.

With constant coefficients the local Lefschetz number is a point count. The sum ∑_{x ∈ X(k)} Tr(π_x | K_x̄) of [Stacks, Tag 03TY] has equal terms when the coefficient system is constant, so it is #X(k) times the trace at a single rational point.

public theorem localLefschetzNumber_constantStalkDatum (Λ : Type u) [Ring Λ] [Finite Λ]
    (points : Type w) [Fintype points] (S : PerfectDerivedCategory.{u, r} Λ)
    (g : S.obj ⟶ S.obj) :
    localLefschetzNumber Λ points (constantStalkDatum.{u, r, w} Λ points S g) =
      (Fintype.card points : ℤ) • perfectDerivedTrace Λ S g

Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_weil_of_constantCoefficients, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantCoefficientTraceFormula.lean, line 126. The attribute's comment: “RESTRICTED: 03UG specialised to constant coefficients computes #X(k), and 03U1 evaluates that count as 1 - Tr_J + deg; the hypotheses of the library's 03UG are carried unchanged, and the constancy of the stalks and the fixed point count are hypotheses”.

The trace formula with constant coefficients is Weil's formula (Stacks 03UJ). In the situation of Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_localLefschetzNumber, suppose the coefficient system is constant, so that the stalk of K at every rational point is one perfect complex S with one endomorphism g on it, and suppose the number of rational points of X is the intersection number V(π_X) = Δ_C · Γ_{π_X} of Weil's formula for the geometric Frobenius. Then

Tr(π_X^* | RΓ_c(X_k̄, K)) = (1 - Tr_J(π_X^*) + deg π_X) · Tr(π_x | K_x̄)

in Λ^natural: the right hand side of the trace formula is the point count, and Weil's formula [Stacks, Tag 03U1] evaluates it on the jacobian of the curve.

public theorem compactSupportLefschetzNumber_eq_weil_of_constantCoefficients
    {k : Type u} [Field k] [Fintype k] {p q : ℕ} [Fact p.Prime] [CharP k p]
    (hcard : Fintype.card k = p ^ q) (Y : Over (Spec (.of k)))
    [IsSeparated Y.hom] [LocallyOfFiniteType Y.hom] [QuasiCompact Y.hom]
    (hdim : topologicalKrullDim Y.left ≤ 1)
    (kbar : Type u) [Field kbar] [IsAlgClosed kbar] [Algebra k kbar] [CharP kbar p]
    (Λ : Type r) [Ring Λ] [Finite Λ]
    (hcoprime : Nat.Coprime (Nat.card Λ) (Fintype.card k))
    (K : CochainComplex.Plus (EtaleModules.{u, r} Λ Y.left))
    [Fintype (rationalPoints Y.hom)]
    (j : CompactificationOf
      (Over.mk (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar))))
    (E : CompactificationEndomorphism j
      (Stacks.Frobenius.geometricFrobeniusBaseChange Y kbar p q hcard))
    (γ : 𝟭 (DerivedCategory.Plus (EtaleModules.{u, r} Λ j.space)) ⟶
      etaleModuleDerivedDirectImage.{u, r} Λ E.hom)
    (hperf : StacksDraft.Perfect.IsPerfect (DerivedCategory.Plus.ι.obj
      ((compactlySupportedCohomology.{u, r} kbar
          (pullback.snd Y.hom (Stacks.Frobenius.specAlgebraMap k kbar)) j Λ).obj
        (baseChangeCoefficients.{u, r} Λ Y kbar K))))
    (hstalkPerfect : ∀ x : rationalPoints Y.hom, StacksDraft.Perfect.IsPerfect
      (DerivedCategory.Q.obj (rationalPointStalkComplex.{u, r} Λ kbar x.1 K)))
    (devissage : LefschetzDevissage.{r, max (u + 1) r, u} Λ (rationalPoints Y.hom))
    (hglobal : devissage.globalDatum =
      frobeniusActionOnCompactSupport.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf)
    (hstalk : devissage.stalkDatum =
      geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect)
    (group : Type t) [Fintype group] (prime exponent level : ℕ)
    (stabilizerExponent : group → ℕ) (coefficientTrace : group → ℤ)
    (moduleTrace : group → AdditiveCommutatorQuotient Λ)
    (hprime : Nat.Prime prime)
    (hannihilate : ∀ y : AdditiveCommutatorQuotient Λ, ((prime : ℤ) ^ exponent) • y = 0)
    (hlevel : ∀ g : group, stabilizerExponent g + exponent ≤ level)
    (hdecomposition : globalLefschetzNumber Λ devissage.openDatum =
      ∑ g : group, coefficientTrace g • moduleTrace g)
    (hdivisible : ∀ g : group, ((prime : ℤ) ^ level) ∣
      ((prime : ℤ) ^ stabilizerExponent g) * coefficientTrace g)
    (S : PerfectDerivedCategory.{r, max (u + 1) r} Λ) (g : S.obj ⟶ S.obj)
    (hconstant : geometricFrobeniusStalkDatum.{u, r} Λ kbar p q hcard Y.hom K hstalkPerfect =
      constantStalkDatum.{r, max (u + 1) r, u} Λ (rationalPoints Y.hom) S g)
    {Adiv : Type w} [AddCommGroup Adiv] {EndJ : Type z} [Ring EndJ]
    (W : JacobianCorrespondence Adiv EndJ) (frobenius : W.EndomorphismData)
    (hfixedPoints : (Fintype.card (rationalPoints Y.hom) : ℤ) =
      W.fixedPointNumber frobenius) :
    compactSupportLefschetzNumber.{u, r} Λ E γ
        (baseChangeCoefficients.{u, r} Λ Y kbar K) hperf =
      (1 - W.trace frobenius.pullback + frobenius.degree) • perfectDerivedTrace Λ S g

Stacks.EtaleCohomology.traceFormula_constantCoefficients_eq_weil, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilComparisonTraceFormula.lean, line 74. References: SGA 4½ Rapport (3.2), “special case”.

[Stacks, Tag 03UJ]: the trace formula with constant coefficients recovers Weil's formula. Let X be a smooth projective curve over a finite field k with #k = p ^ q, which stays a curve over an algebraic closure k̄ (the setting of Weil's formula, Tag 03U1, on X_k̄), and let ℓ ≠ p be a prime. Let π̄ = π_X × id be the geometric Frobenius of X_k̄. Then

  • the trace formula (Tag 03UG) for Λ = ℤ/ℓⁿ gives Tr(π_X^* | RΓ(X_k̄, ℤ/ℓⁿ)) = #X(k);
  • this Lefschetz number is ∑ᵢ (-1)ⁱ Tr(π̄^* | Hⁱ(X_k̄, ℤ/ℓⁿ));
  • the intersection number V(π̄) = (Δ · Γ_π̄) is #X(k) (the fixed points of π̄ are simple);
  • hence Weil's formula (Tag 03U1) for π̄ reads #X(k) = 1 - Tr(π̄ | T_ℓ J) + deg π̄ in ℤ_ℓ.

So both formulas count the same number #X(k).

theorem traceFormula_constantCoefficients_eq_weil
    [IsCurve kbar (pullback.snd f (specAlgebraMap k kbar))] (hℓ : ℓ ≠ p) :
    canonicalCompactSupportLefschetzNumber.{u, 0} (ZMod (ℓ ^ n)) f (CompactificationOf.ofProper f)
        kbar p q hcard (constantCoefficients (ZMod (ℓ ^ n)) X.obj)
        (isPerfect_compactSupportFrobeniusCohomology_constantCoefficients B (ZMod (ℓ ^ n)) f
          (isProjective_of_isProper_of_isCurve f) kbar) =
      (Nat.card (rationalPoints f) : ℤ) • additiveCommutatorQuotientMk (ZMod (ℓ ^ n)) 1 ∧
    canonicalCompactSupportLefschetzNumber.{u, 0} (ZMod (ℓ ^ n)) f (CompactificationOf.ofProper f)
        kbar p q hcard (constantCoefficients (ZMod (ℓ ^ n)) X.obj)
        (isPerfect_compactSupportFrobeniusCohomology_constantCoefficients B (ZMod (ℓ ^ n)) f
          (isProjective_of_isProper_of_isCurve f) kbar) =
      additiveCommutatorQuotientMk (ZMod (ℓ ^ n))
        (∑ i ∈ Finset.range 3, (-1 : ZMod (ℓ ^ n)) ^ i * LinearMap.trace (ZMod (ℓ ^ n)) _
          ((etaleConstantCohomologyPullback
            (geometricFrobeniusBaseChange (Over.mk f) kbar p q hcard)
            (ZMod (ℓ ^ n)) i).toZModLinearMap (ℓ ^ n))) ∧
    AlgebraicGeometry.CurveGraph.fixedPointIntersection (pullback.snd f (specAlgebraMap k kbar))
        (IsCurve.topologicalKrullDim_eq_one (k := kbar)
          (f := pullback.snd f (specAlgebraMap k kbar))).le
        (geometricFrobeniusBaseChange (Over.mk f) kbar p q hcard)
          (geometricFrobeniusBaseChange_comp_toBase (Over.mk f) kbar p q hcard) =
      Nat.card (rationalPoints f) ∧
    (((Nat.card (rationalPoints f) : ℤ)) : ℤ_[ℓ]) =
      1 - AlgebraicGeometry.CurveGraph.jacobianTateTrace (pullback.snd f (specAlgebraMap k kbar))
        (IsCurve.topologicalKrullDim_eq_one (k := kbar)
          (f := pullback.snd f (specAlgebraMap k kbar))).le
        (geometricFrobeniusBaseChange (Over.mk f) kbar p q hcard)
          (geometricFrobeniusBaseChange_comp_toBase (Over.mk f) kbar p q hcard) ℓ +
        (AlgebraicGeometry.CurveGraph.curveMapDegree (pullback.snd f (specAlgebraMap k kbar))
          (geometricFrobeniusBaseChange (Over.mk f) kbar p q hcard)
          (geometricFrobeniusBaseChange_comp_toBase (Over.mk f) kbar p q hcard) : ℤ_[ℓ])
Sources
LeanStacks.EtaleCohomology.exists_compactification_and_traceFormulaUpToDim_one · Stacks.EtaleCohomology.compactSupportLefschetzNumber_eq_localLefschetzNumber · Stacks.EtaleCohomology.compactificationFieldBaseChange · Stacks.EtaleCohomology.geometricCompactSupportCohomology · Stacks.EtaleCohomology.geometricCompactSupportCohomologyGroup · Stacks.EtaleCohomology.geometricCompactSupportComparison · Stacks.EtaleCohomology.geometricCompactSupportGroupComparison · Stacks.EtaleCohomology.geometricCompactSupportCanonicalComparison

Section64.18 On l-adic sheaves#

Section 64.18 of the Stacks Project, Tag 03UL. 6 tags here are carried by 33 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03UM, a definition

Tag 03UM in the Stacks Project.

AlgebraicGeometry.SmallEtale.LAdicSheaf, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LAdicSheaves.lean, line 134. The attribute's comment: “objects”. References: SGA 5 V (3.1), “ℓ-adic étale case”; SGA 4½ Rapport (2.1), “Z_ℓ-sheaf definition”; SGA 5 V (3.1.1), “A=Z_ℓ, J=(ℓ), étale site”; SGA 5 VI (1.1.1); SGA 5 VI (1.2), “Z_ℓ-sheaf definition”.

Stacks 03UM. An ℓ-adic sheaf is an inverse system of constructible ℤ/ℓⁿℤ-module sheaves whose successive scalar reductions are isomorphisms.

public structure LAdicSheaf [IsNoetherian X.obj] [Fact ℓ.Prime]

AlgebraicGeometry.SmallEtale.LAdicSheaf.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LAdicSheaves.lean, line 152. The attribute's comment: “morphisms”. References: SGA 5 V (3.1), “morphisms, ℓ-adic case”; SGA 5 VI (1.1.1), “morphisms”; SGA 5 VI (1.2), “morphisms”; SGA 4½ Rapport (2.6), “hom(F,G)”.

Stacks 03UM. A morphism of ℓ-adic sheaves is a compatible family of morphisms at the finite levels.

public structure LAdicSheaf.Hom [IsNoetherian X.obj] [Fact ℓ.Prime]
    (F G : LAdicSheaf.{u, m} B X ℓ)

AlgebraicGeometry.SmallEtale.LAdicSheaf.IsLisse, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LAdicSheaves.lean, line 188. The attribute's comment: “lisse”.

Stacks 03UM. A lisse ℓ-adic sheaf has locally constant sheaves at every finite level.

public abbrev LAdicSheaf.IsLisse [IsNoetherian X.obj] [Fact ℓ.Prime]
    (F : LAdicSheaf.{u, m} B X ℓ) : Prop
Tag 03UN, a lemma

Tag 03UN in the Stacks Project.

AlgebraicGeometry.SmallEtale.exists_lAdicSheaf_of_eventuallyConstant_reductions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LAdicEventuallyConstant.lean, line 1018. References: SGA 4½ Rapport (2.6), “ess.const ⇒ Zℓ-sheaf”.

Stacks 03UN. Eventually constant reductions of a constructible inverse system give an ℓ-adic sheaf whose levels are the stable values of those reductions.

public theorem exists_lAdicSheaf_of_eventuallyConstant_reductions
    [IsNoetherian X.obj] [Fact ℓ.Prime]
    (G : ∀ n, FiniteLevelSheaf.{u, m} B X ℓ n)
    (t : ∀ n, G (n + 1) ⟶ (G n).restrictScalars B X ℓ n)
    (hG : ∀ n, IsConstructibleModuleSheaf B X (ZMod (ℓ ^ (n + 1))) (G n))
    (heventually : ∀ (k : ℕ), ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → (h : k ≤ n) →
      IsIso ((Sheaf.composeAndSheafify
        (SmallEtale.topology B X.obj X.property)
        (ModuleCat.extendScalars.{0, 0, m}
          (ZMod.castHom (pow_dvd_pow ℓ (by omega : k + 1 ≤ n + 2)) _ :
            ZMod (ℓ ^ (n + 2)) →+* ZMod (ℓ ^ (k + 1))))).map (t n))) :
    ∃ F : LAdicSheaf.{u, m} B X ℓ, ∃ N : ℕ → ℕ,
      ∃ e : ∀ (k n : ℕ), N k ≤ n → (h : k ≤ n) →
        F.level k ≅ FiniteLevelSheaf.reduceTo B X ℓ n k h (G n),
      (∀ (k n : ℕ) (hn : N k ≤ n) (h : k ≤ n),
        (e k (n + 1) (by omega) (by omega)).hom ≫
          ((Sheaf.composeAndSheafify
            (SmallEtale.topology B X.obj X.property)
            (ModuleCat.extendScalars.{0, 0, m}
              (ZMod.castHom (pow_dvd_pow ℓ (by omega : k + 1 ≤ n + 2)) _ :
                ZMod (ℓ ^ (n + 2)) →+* ZMod (ℓ ^ (k + 1))))).map (t n)) ≫
          (FiniteLevelSheaf.canonicalRestrictionComparison B X ℓ n k h (G n)) =
          (e k n hn h).hom) ∧
      (∀ (k n : ℕ) (hn₁ : N k ≤ n) (hn₂ : N (k + 1) ≤ n)
          (h : k + 1 ≤ n),
        F.transition k ≫
          (sheafCompose (SmallEtale.topology B X.obj X.property)
            (ModuleCat.restrictScalars.{m, 0, 0}
              (finiteLevelRingHom ℓ k))).map
            ((e k n hn₁ (by omega)).hom) =
        (e (k + 1) n hn₂ h).hom ≫
          (FiniteLevelSheaf.canonicalReductionTransition B X ℓ n k h (G n)))
Tag 03UO, a lemma

Tag 03UO in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.normalEpiCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Abelian.lean, line 214. The attribute's comment: “every epimorphism is a cokernel”.

Stacks 03UO, normality of epimorphisms: every epimorphism of ℓ-adic sheaves is a cokernel.

public instance normalEpiCategory : IsNormalEpiCategory (LAdicSheaf.{u, u + 1} B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.hasKernels, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Abelian.lean, line 278. The attribute's comment: “kernels”.

Stacks 03UO, the kernel part: the category of ℓ-adic sheaves on a Noetherian scheme has kernels. The kernel of a morphism is the kernel of the epimorphism in its image factorisation.

public instance hasKernels : HasKernels (LAdicSheaf.{u, u + 1} B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.normalMonoCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Abelian.lean, line 291. The attribute's comment: “every monomorphism is a kernel”.

Stacks 03UO, normality of monomorphisms: every monomorphism of ℓ-adic sheaves is a kernel. In the image factorisation of a monomorphism the epimorphic half is also a monomorphism, hence an isomorphism, so the monomorphism is the kernel the factorisation provides.

public instance normalMonoCategory : IsNormalMonoCategory (LAdicSheaf.{u, u + 1} B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.abelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Abelian.lean, line 311. References: SGA 5 V (3.2), “abelian”; SGA 4½ Rapport (2.6), “abelian”; SGA 5 VI (1.1.3), “special case”.

Stacks 03UO. The category of ℤ_ℓ-sheaves on a Noetherian scheme is abelian: it is preadditive with finite biproducts, has kernels and cokernels, and every monomorphism is a kernel while every epimorphism is a cokernel.

public instance abelian : Abelian (LAdicSheaf.{u, u + 1} B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.hasZeroObject, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Additive.lean, line 278. The attribute's comment: “zero object”.

The category of ℓ-adic sheaves has a zero object.

public instance LAdicSheaf.hasZeroObject : HasZeroObject (LAdicSheaf B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.hasFiniteBiproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Additive.lean, line 399. The attribute's comment: “additive: finite biproducts, formed levelwise”.

Stacks 03UO, the additive part: the category of ℓ-adic sheaves on a Noetherian scheme has finite biproducts, the biproduct being formed levelwise.

public instance hasFiniteBiproducts : HasFiniteBiproducts (LAdicSheaf B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.hasCokernels, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Additive.lean, line 476. The attribute's comment: “cokernels, formed levelwise”.

Stacks 03UO, the cokernel part: the category of ℓ-adic sheaves on a Noetherian scheme has cokernels, formed levelwise.

public instance hasCokernels : HasCokernels (LAdicSheaf B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.normalMono_of_app_mono, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Normality.lean, line 153. The attribute's comment: “monomorphisms with monomorphic components are kernels, of the levelwise cokernel”.

A morphism of ℓ-adic sheaves whose components are monomorphisms is the kernel of its levelwise cokernel.

public def normalMono_of_app_mono {F G : LAdicSheaf.{u, u + 1} B X ℓ} (f : F ⟶ G)
    (hf : ∀ n, Mono (f.app n)) : NormalMono f

Stacks.EtaleCohomology.LAdicSheaf.normalEpi_of_epi_kernelLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Normality.lean, line 196. The attribute's comment: “epimorphisms whose levelwise kernel comparisons are epimorphisms are cokernels, of the morphism those comparisons compare to”.

An epimorphism of ℓ-adic sheaves is the cokernel of a morphism killed by it whose levelwise kernel comparisons are epimorphisms.

public def normalEpi_of_epi_kernelLift {K F G : LAdicSheaf.{u, u + 1} B X ℓ} (i : K ⟶ F)
    (f : F ⟶ G) [Epi f] (w : i ≫ f = 0)
    (hi : ∀ n, Epi (kernel.lift (f.app n) (i.app n) (comp_eq_zero_app i f w n))) :
    NormalEpi f

AlgebraicGeometry.SmallEtale.LAdicSheaf.preadditive, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/Etale/LAdicSheafPreadditive.lean, line 147. The attribute's comment: “preadditive”.

Stacks 03UO. ℓ-adic sheaves form a preadditive category: morphisms add levelwise and composition is bilinear.

public instance LAdicSheaf.preadditive : Preadditive (LAdicSheaf.{u, m} B X ℓ)
Tag 03UQ, a remark

Tag 03UQ in the Stacks Project.

Stacks.EtaleCohomology.finite_finiteLevelStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/FiniteLevelStalk.lean, line 385. The attribute's comment: “finite_level_stalks”.

Every finite-level stalk of an ℓ-adic sheaf at a geometric point is finite.

public theorem finite_finiteLevelStalk (F : LAdicSheaf B X ℓ) (s : GeometricPoint X.1) (n : ℕ) :
    Finite (finiteLevelStalk B X ℓ F s n)

Stacks.EtaleCohomology.finiteLevelStalkTransition_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/FiniteLevelStalk.lean, line 404. The attribute's comment: “finite_level_stalks”.

Each transition between consecutive finite-level stalks is surjective.

public theorem finiteLevelStalkTransition_surjective (F : LAdicSheaf B X ℓ)
    (s : GeometricPoint X.1) (n : ℕ) :
    Function.Surjective (finiteLevelStalkTransition B X ℓ F s n).hom

Stacks.EtaleCohomology.finiteLevelStalkTransition_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/FiniteLevelStalk.lean, line 427. The attribute's comment: “finite_level_stalks”.

The transition identifies the quotient of the level-n+1 stalk by ℓⁿ⁺¹ with the level-n stalk.

public theorem finiteLevelStalkTransition_quotient (F : LAdicSheaf B X ℓ)
    (s : GeometricPoint X.1) (n : ℕ) :
    ∃ e : (finiteLevelStalk B X ℓ F s (n + 1) ⧸
        (Ideal.span ({(ℓ ^ (n + 1) : ZMod (ℓ ^ (n + 2)))} : Set (ZMod (ℓ ^ (n + 2))))) •
          (⊤ : Submodule (ZMod (ℓ ^ (n + 2))) (finiteLevelStalk B X ℓ F s (n + 1))))
        ≃ₗ[ZMod (ℓ ^ (n + 2))]
          (ModuleCat.restrictScalars (finiteLevelRingHom ℓ n)).obj
            (finiteLevelStalk B X ℓ F s n),
      ∀ x, e (Submodule.Quotient.mk x) = (finiteLevelStalkTransition B X ℓ F s n).hom x

Stacks.EtaleCohomology.LAdicSheaf.stalk, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Stalk.lean, line 87. The attribute's comment: “stalk_of_a_sheaf”. References: SGA 4½ Rapport (2.2), “fiber definition”.

The stalk of an ℓ-adic sheaf at a geometric point: the inverse limit of its finite-level stalks, as a ℤ_[ℓ]-module.

public abbrev LAdicSheaf.stalk (F : LAdicSheaf B X ℓ) (x : GeometricPoint X.1) :
    Type (u + 1)

Stacks.EtaleCohomology.LAdicSheaf.finite_stalk, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/StalkFiniteness.lean, line 163. The attribute's comment: “finite_limit_stalk”.

The stalk of an ℓ-adic sheaf is finite over the ℓ-adic integers.

public instance LAdicSheaf.finite_stalk
    (F : LAdicSheaf B X ℓ) (x : GeometricPoint X.1) :
    Module.Finite (PadicInt ℓ)
      (LAdicSheaf.stalk B X ℓ F x)

Stacks.EtaleCohomology.LAdicSheaf.stalk_equiv_free_prod_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/StalkFiniteness.lean, line 189. The attribute's comment: “stalk_structure”.

A stalk of an ℓ-adic sheaf is a sum of free and prime-power cyclic modules.

public theorem LAdicSheaf.stalk_equiv_free_prod_torsion
    (F : LAdicSheaf B X ℓ) (x : GeometricPoint X.1) :
    ∃ (r t : ℕ) (e : Fin t → ℕ),
      (∀ i, 1 ≤ e i) ∧
      Nonempty (LAdicSheaf.stalk B X ℓ F x ≃ₗ[PadicInt ℓ]
        (Fin r →₀ PadicInt ℓ) ×
          DirectSum (Fin t)
            (fun i => PadicInt ℓ ⧸ (PadicInt ℓ) ∙ ((ℓ : PadicInt ℓ) ^ e i)))
Tag 03UR, a definition

Tag 03UR in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.IsTorsion, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Basic.lean, line 78. The attribute's comment: “torsion_sheaf”.

A torsion ℓ-adic sheaf is annihilated by a single power of ℓ, uniformly at all finite levels.

public abbrev LAdicSheaf.IsTorsion [IsNoetherian X.1] [Fact ℓ.Prime]
    (F : LAdicSheaf B X ℓ) : Prop

Stacks.EtaleCohomology.torsionSheaves, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Rational.lean, line 93. The attribute's comment: “the subcategory of torsion sheaves”.

Stacks 03UR. The torsion ℤ_ℓ-sheaves, as a property of objects of the abelian category of ℤ_ℓ-sheaves.

public abbrev torsionSheaves : ObjectProperty (LAdicSheaf.{u, u + 1} B X ℓ)

Stacks.EtaleCohomology.RationalSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Rational.lean, line 107. The attribute's comment: “the category of Q_ℓ-sheaves as the quotient by the torsion sheaves”. References: SGA 4½ Rapport (2.9).

Stacks 03UR. The abelian category of ℚ_ℓ-sheaves on X: the quotient of the abelian category of ℤ_ℓ-sheaves by the Serre subcategory of torsion sheaves. Its objects are the ℤ_ℓ-sheaves on X.

public abbrev RationalSheaf

Stacks.EtaleCohomology.rationalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Rational.lean, line 111. The attribute's comment: “the quotient functor F ↦ F ⊗ Q_ℓ”.

Stacks 03UR. The quotient functor F ↦ F ⊗ ℚ_ℓ from ℤ_ℓ-sheaves to ℚ_ℓ-sheaves.

public abbrev rationalization : LAdicSheaf.{u, u + 1} B X ℓ ⥤ RationalSheaf B X ℓ

Stacks.EtaleCohomology.RationalSheaf.abelian, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Rational.lean, line 116. The attribute's comment: “Q_ℓ-sheaves form an abelian category”.

Stacks 03UR. The category of ℚ_ℓ-sheaves on X is abelian.

public instance RationalSheaf.abelian : Abelian (RationalSheaf B X ℓ)

Stacks.EtaleCohomology.LAdicSheaf.rationalStalk, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Rational.lean, line 123. The attribute's comment: “the stalk of F ⊗ Q_l is the stalk of F tensored with Q_l”.

Stacks 03UR. The stalk at a geometric point x of the ℚ_ℓ-sheaf F ⊗ ℚ_ℓ, for F a ℤ_ℓ-sheaf: the ℤ_ℓ-module stalk of F (Tag 03UQ) tensored up to ℚ_ℓ. Every ℚ_ℓ-sheaf is of this shape, the objects of the quotient category being the ℤ_ℓ-sheaves themselves.

public abbrev LAdicSheaf.rationalStalk (F : LAdicSheaf.{u, u + 1} B X ℓ)
    (x : GeometricPoint X.1) : Type (u + 1)

Stacks.CategoryTheory.isTorsionObject_isSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/SerreClass/BoundedTorsion.lean, line 140. The attribute's comment: “torsion sheaves are a Serre subcategory”. References: SGA 4½ Rapport (2.9), “more general”.

The ℓ-power torsion objects of an abelian category form a Serre class: they contain the zero object and are closed under subobjects, quotients and extensions. For ℤ_ℓ-sheaves this is the Serre subcategory of torsion sheaves of Stacks 03UR.

public instance isTorsionObject_isSerreClass (ℓ : ℕ) :
    (isTorsionObject (C := C) ℓ).IsSerreClass

Stacks.CategoryTheory.isLocalizedModule_mapIntLinearMap, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Abelian/SerreClass/BoundedTorsion.lean, line 277. The attribute's comment: “Hom_{Q_l}(F,G) = Hom_{Z_l}(F,G) localized at the powers of l”. References: SGA 4½ Rapport (2.9), “more general”.

The hom-groups of a Serre quotient at the ℓ-power torsion objects. The localization functor exhibits Hom (L.obj X) (L.obj Y) as the localization of the abelian group Hom X Y at the powers of ℓ: multiplication by ℓ is invertible on the target, every element of the target is a power of ℓ away from the image, and two morphisms have the same image exactly when a power of ℓ equalizes them. For ℤ_ℓ-sheaves this is the formula Hom_{ℚ_ℓ}(F, G) = Hom_{ℤ_ℓ}(F, G) ⊗_{ℤ_ℓ} ℚ_ℓ of Stacks 03UR, since every integer prime to ℓ is already a unit of ℤ_ℓ.

public instance isLocalizedModule_mapIntLinearMap (X Y : C) :
    IsLocalizedModule (Submonoid.powers (ℓ : ℤ)) (mapIntLinearMap L X Y)
Tag 03UT, a definition

Tag 03UT in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.cohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/Cohomology.lean, line 145. The attribute's comment: “ℓ-adic cohomology”. References: SGA 7 I (0.1), “b)”; SGA 5 VI (3.1), “def of H^i(X,F)”.

The ℓ-adic cohomology of an ℓ-adic sheaf. For an ℓ-adic sheaf F = {Fₙ} on X and a degree i, this is Hⁱ(X, F) = limₙ Hⁱ(X, Fₙ).

public def LAdicSheaf.cohomology (F : LAdicSheaf B X ℓ) (i : ℕ) : AddCommGrpCat.{u + 1}

Stacks.EtaleCohomology.LAdicSheaf.compactlySupportedCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/CompactlySupportedCohomology.lean, line 195. The attribute's comment: “H^i_c(X, F) = lim_n H^i_c(X, F_n)”.

The compactly supported ℓ-adic cohomology of an ℓ-adic sheaf. For an ℓ-adic sheaf F = {Fₙ} on X and a degree i, this is Hⁱ_c(X, F) = limₙ Hⁱ_c(X, Fₙ).

public def LAdicSheaf.compactlySupportedCohomology (F : LAdicSheaf B X ℓ) (i : ℤ) :
    ModuleCat.{u + 1} ℤ_[ℓ]

Stacks.EtaleCohomology.LAdicSheaf.rationalCompactlySupportedCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LAdicSheaves/CompactlySupportedCohomology.lean, line 215. The attribute's comment: “H^i_c(X, F' ⊗ Q_ell) = H^i_c(X, F') ⊗_{Z_ell} Q_ell”. References: SGA 4½ Rapport (2.10); SGA 7 I (0.1), “more general”.

The compactly supported ℓ-adic cohomology with ℚ_[ℓ]-coefficients. For the rational ℓ-adic sheaf F ⊗ Q_ℓ attached to an ℓ-adic sheaf F, this is the extension of scalars of Hⁱ_c(X, F) along ℤ_[ℓ] → ℚ_[ℓ], that is Hⁱ_c(X, F ⊗ Q_ℓ) = Hⁱ_c(X, F) ⊗_{ℤ_[ℓ]} ℚ_[ℓ].

public def LAdicSheaf.rationalCompactlySupportedCohomology (F : LAdicSheaf B X ℓ) (i : ℤ) :
    ModuleCat.{u + 1} ℚ_[ℓ]

Stacks.EtaleCohomology.LAdicSheaf.geometricCompactlySupportedCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricLAdicCompactSupport.lean, line 210. The attribute's comment: “H^i_c(X_kbar, F) = lim_n H^i_c(X_kbar, F_n), on the geometric fibre”.

The compactly supported ℓ-adic cohomology of the geometric fibre, Hⁱ_c(X_k̄, F) = limₙ Hⁱ_c(X_k̄, Fₙ), as in Tag 03UT for the restriction of F to X_k̄.

public def LAdicSheaf.geometricCompactlySupportedCohomology (F : LAdicSheaf B X ℓ) (i : ℤ) :
    ModuleCat.{u + 1} ℤ_[ℓ]

Stacks.EtaleCohomology.LAdicSheaf.rationalGeometricCompactlySupportedCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricLAdicCompactSupport.lean, line 226. The attribute's comment: “H^i_c(X_kbar, F' ⊗ Q_ell) = H^i_c(X_kbar, F') ⊗_{Z_ell} Q_ell, on the geometric fibre”. References: SGA 4½ Rapport (2.10); SGA 7 XXI (2.0), “more general”.

Hⁱ_c(X_k̄, F ⊗ Q_ℓ) = Hⁱ_c(X_k̄, F) ⊗_{ℤ_[ℓ]} ℚ_[ℓ], the cohomology of the rational ℓ-adic sheaf F ⊗ Q_ℓ that Tag 03V2 is about.

public def LAdicSheaf.rationalGeometricCompactlySupportedCohomology (F : LAdicSheaf B X ℓ)
    (i : ℤ) : ModuleCat.{u + 1} ℚ_[ℓ]
Sources
LeanAlgebraicGeometry.SmallEtale.LAdicSheaf · AlgebraicGeometry.SmallEtale.LAdicSheaf.Hom · AlgebraicGeometry.SmallEtale.LAdicSheaf.IsLisse · AlgebraicGeometry.SmallEtale.exists_lAdicSheaf_of_eventuallyConstant_reductions · Stacks.EtaleCohomology.LAdicSheaf.normalEpiCategory · Stacks.EtaleCohomology.LAdicSheaf.hasKernels · Stacks.EtaleCohomology.LAdicSheaf.normalMonoCategory · Stacks.EtaleCohomology.LAdicSheaf.abelian

Section64.19 L-functions#

Section 64.19 of the Stacks Project, Tag 03UU. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03UV, a definition

Tag 03UV in the Stacks Project.

Stacks.EtaleCohomology.lFunctionOfConstructibleFlat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstructibleFlatLFunction.lean, line 131. The attribute's comment: “the definition of L(X, F) for a constructible flat Λ-module F: the local factors are the local factors of the geometric Frobenius on the stalks of F, whose finiteness and projectivity are derived from constructible flatness rather than supplied”. References: SGA 4½ Rapport (1.6), “L-function of a sheaf”.

The L-function of a constructible flat Λ-module. It is the Euler product over the closed points of X of the inverse local factors det(1 - π_x^* T ^ (deg x) |_{ℱ_x̄}) ⁻¹ of the geometric Frobenius acting on the stalks of ℱ.

public def lFunctionOfConstructibleFlat [QuasiCompact f] : PowerSeries Λ

Stacks.EtaleCohomology.constructibleFlatLFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FiniteCoefficientLFunction.lean, line 152. The attribute's comment: “the definition of L(X, F) for a constructible flat Λ-module F over an arbitrary finite (indeed commutative) coefficient ring Λ, not necessarily local: the local factors are the projective determinants of the geometric Frobenius on the finite projective stalks”. References: SGA 4½ Rapport (1.6), “partial”.

The L-function L(X, ℱ) = ∏_{x ∈ |X|} det(1 - π_x^* T ^ (deg x) |_{ℱ_x̄}) ⁻¹ ∈ Λ⟦T⟧ of a constructible flat Λ-module on X_étale, for a scheme of finite type over a finite field and an arbitrary commutative coefficient ring Λ, in particular any finite ring. Its local factors are the projective determinants of the geometric Frobenius on the finite projective stalks.

public def constructibleFlatLFunction [QuasiCompact f]
    (hF : IsConstructibleFlatModuleSheaf B X Λ F) : PowerSeries Λ

Stacks.EtaleCohomology.FrobeniusMatrices.lFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LFunctionEulerProduct.lean, line 342. The attribute's comment: “the Euler product over the closed points of a scheme of finite type over a finite field, for a given family of Frobenius matrices rather than one derived from a constructible flat sheaf; the positivity of the residue degrees and the finiteness of the closed points of bounded degree are proved, not assumed”. References: SGA 4½ Rapport (1.6), “Euler product”.

The L-function ∏_{x ∈ |X|} det(1 - π_x^* T ^ (deg x)) ⁻¹ of a family of Frobenius matrices on a scheme X over k, as an element of Λ⟦T⟧.

public def lFunction [Finite k] [LocallyOfFiniteType f] [QuasiCompact f] : PowerSeries Λ
Tag 03UX, a definition

Tag 03UX in the Stacks Project.

Stacks.EtaleCohomology.EulerSystem.coeff_eulerProduct_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LFunctionEulerProduct.lean, line 280. The attribute's comment: “the convergence of the Euler product: it is stated for an arbitrary coefficient ring, so it specializes to the Q_ell case of this tag”.

The Euler product converges: the coefficient of T ^ j of the Euler product is the coefficient of T ^ j of the product over any finite set of indices that contains all the indices of degree at most j.

public theorem coeff_eulerProduct_eq {j : ℕ} {t : Finset ι} (ht : E.support j ⊆ t) :
    PowerSeries.coeff j E.eulerProduct = PowerSeries.coeff j (∏ i ∈ t, E.factor i)

Stacks.EtaleCohomology.LAdicSheaf.rationalLFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LFunctionRationalSheaf.lean, line 150. The attribute's comment: “the definition of L(X, F) for a Q_ell-sheaf F, as the Euler product over the closed points of the inverse characteristic series of the geometric Frobenius on the rational stalks”. References: SGA 4½ Rapport (1.6), “adic coefficients”.

The L-function of a ℚ_ℓ-sheaf F on a scheme X of finite type over a finite field k:

L(X, F) = ∏_{x ∈ |X|} det(1 - π_x^* T ^ (deg x) | F_x̄) ⁻¹ ∈ ℚ_ℓ⟦T⟧,

the product over the closed points |X| of X of the inverse characteristic series of the geometric Frobenius π_x^* acting on the rational stalk F_x̄ at a geometric point over x, where deg x = [κ(x) : k]. The factor at x is identified with det(1 - π_x^* T ^ (deg x) | F_x̄) ⁻¹ by localFactor_frobeniusMatrices, and the product converges in the sense of coeff_rationalLFunction_eq: there are finitely many closed points of any given degree, so each coefficient is already computed by a finite subproduct.

public def LAdicSheaf.rationalLFunction (F : LAdicSheaf B X ℓ) (f : X.1 ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] : PowerSeries (Padic ℓ)

Stacks.EtaleCohomology.LAdicSheaf.coeff_rationalLFunction_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LFunctionRationalSheaf.lean, line 158. The attribute's comment: “the product converges since there are finitely many points of a given degree”.

The convergence of the defining product: the coefficient of T ^ j of L(X, F) is computed by the product of the local factors over any finite set of closed points containing all those of degree at most j.

public theorem LAdicSheaf.coeff_rationalLFunction_eq (F : LAdicSheaf B X ℓ)
    (f : X.1 ⟶ Spec (.of k)) [LocallyOfFiniteType f] [QuasiCompact f]
    {j : ℕ} {t : Finset (closedPoints X.1)}
    (ht : (LAdicSheaf.frobeniusMatrices B X ℓ F f).eulerSystem.support j ⊆ t) :
    PowerSeries.coeff j (LAdicSheaf.rationalLFunction B X ℓ F f) =
      PowerSeries.coeff j
        (∏ x ∈ t, (LAdicSheaf.frobeniusMatrices B X ℓ F f).localFactor x)
Sources
LeanStacks.EtaleCohomology.lFunctionOfConstructibleFlat · Stacks.EtaleCohomology.constructibleFlatLFunction · Stacks.EtaleCohomology.FrobeniusMatrices.lFunction · Stacks.EtaleCohomology.EulerSystem.coeff_eulerProduct_eq · Stacks.EtaleCohomology.LAdicSheaf.rationalLFunction · Stacks.EtaleCohomology.LAdicSheaf.coeff_rationalLFunction_eq

Section64.20 Cohomological interpretation#

Section 64.20 of the Stacks Project, Tag 03UY. 6 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03UZ, a theorem

Tag 03UZ in the Stacks Project.

Stacks.EtaleCohomology.lFunction_eq_inv_charSeries_compactSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FiniteCoefficientCohomologicalInterpretation.lean, line 169. References: SGA 4½ Fonctions L (2.2), “Theorem 2.2 case a)”.

The cohomological interpretation of the L-function with finite coefficients. Let X be a separated scheme of finite type over a finite field k, k̄ an algebraic closure of k, Λ a finite commutative ring of order prime to the characteristic of k, and F a constructible flat Λ-module on X_étale. Then X has a compactification, and for every compactification j (through which RΓ_c(X_k̄, -) and π_X^* are computed) and every presentation #k = p ^ q, RΓ_c(X_k̄, F) is perfect and L(X, F) = det(1 - π_X^* T | RΓ_c(X_k̄, F))⁻¹ in Λ⟦T⟧.

theorem lFunction_eq_inv_charSeries_compactSupport
    [Algebra.IsAlgebraic k kbar] (Λ : Type) [CommRing Λ] [Finite Λ]
    (hΛ : ((Nat.card Λ : ℕ) : k) ≠ 0)
    (F : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{u + 1} Λ))
    (hF : IsConstructibleFlatModuleSheaf B X Λ F) :
    Nonempty (CompactificationOf (Over.mk f)) ∧
      ∀ (j : CompactificationOf (Over.mk f)) (p q : ℕ) [Fact p.Prime] [CharP k p]
        (hcard : Fintype.card k = p ^ q),
        LFunctionCharSeriesIdentity B X Λ f kbar F hF j p q hcard
Tag 03V0, a theorem

Tag 03V0 in the Stacks Project.

Stacks.EtaleCohomology.FrobeniusMatrices.lFunction_eq_alternatingCharSeries, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CohomologicalInterpretation.lean, line 188. The attribute's comment: “the determinant identity, with the trace formula of Tag 03V2 over the finite extensions of k carried as the explicit hypothesis TraceFormula”.

Stacks Project, Tag 03V0, Theorem 64.20.2 (Adic sheaves). The L-function is the alternating product of the characteristic series of geometric Frobenius on compactly supported cohomology, L(X, ℱ) = ∏_i det(1 - π_X^* T |_{H_c^i(X_k̄, ℱ)}) ^ ((-1) ^ (i + 1)). The coefficient ring is only required to have torsion-free additive group, which holds for ℚ_ℓ; this is the hypothesis behind the source's "since ℚ_ℓ has characteristic 0, it suffices to prove the equality after taking logarithmic derivatives".

public theorem lFunction_eq_alternatingCharSeries [IsAddTorsionFree Λ] {ι : Type w} [Fintype ι]
    (deg : ι → ℤ) (rk : ι → ℕ) (B : ∀ a : ι, Matrix (Fin (rk a)) (Fin (rk a)) Λ)
    (htrace : D.TraceFormula deg rk B) :
    D.lFunction = alternatingCharSeries deg rk B

Stacks.EtaleCohomology.FrobeniusMatrices.lFunction_eq_alternatingCharSeries_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CohomologicalInterpretationCriterion.lean, line 186. The attribute's comment: “the determinant identity, equivalent to the trace identity in the proof”.

The cohomological interpretation of the L-function, as a criterion. Over a coefficient ring with torsion-free additive group the determinant identity L(X, ℱ) = ∏_i det(1 - π_X^* T |_{H_c^i(X_k̄, ℱ)}) ^ ((-1) ^ (i + 1)) holds if and only if the trace identity ∑_{d ∣ n} d ∑_{deg x = d} tr((π_x^{n / d})^* |_{ℱ_x̄}) = ∑_i (-1) ^ i tr((π_X^n)^* |_{H_c^i}) holds for every n ≥ 1.

public theorem lFunction_eq_alternatingCharSeries_iff [IsAddTorsionFree Λ] :
    D.lFunction = alternatingCharSeries deg rk B ↔ D.TraceFormula deg rk B

Stacks.EtaleCohomology.LAdicSheaf.rationalLFunction_eq_gradedCharSeries_compactSupportFrobenius, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LAdicTraceFormulaFinal.lean, line 135. The attribute's comment: “the determinant identity for a Q_l-sheaf, l invertible in k”.

The L-function of a ℚ_ℓ-sheaf. Let X be a separated scheme of finite type over a finite field k with p ^ q elements, k̄ an algebraic closure of k, ℓ a prime with ℓ ≠ p and F a ℚ_ℓ-sheaf on X. Then L(X, F) = ∏ᵢ det(1 - π_X^* T | Hⁱ_c(X_k̄, F))^{(-1)^{i+1}} in ℚ_ℓ[[T]].

X is separated because Hⁱ_c is defined for separated schemes only (Definition 03UT). ℓ ≠ p is the chapter's standing convention; the statement is false for ℓ = p (L(𝔸¹_k, ℚ_p) = 1/(1 - p ^ q T) while the alternating product is 1).

theorem LAdicSheaf.rationalLFunction_eq_gradedCharSeries_compactSupportFrobenius (hℓp : ℓ ≠ p)
    (F : LAdicSheaf.{u, u + 1} B X ℓ) :
    LAdicSheaf.rationalLFunction B X ℓ F f =
      gradedCharSeries
        (fun i => LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i)
        (fun i => (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f j kbar p q
          hcard F i).hom)
Tag 03V1, a remark

Tag 03V1 in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.adicLFunction_eq_inv_charSeries_compactSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/AdicLFunctionCohomologicalInterpretation.lean, line 63. The attribute's comment: “the identity for Z_l coefficients is the l-adic limit of 03UZ at the levels, and it is equivalent to 03V0 for F ⊗ Q_l since Z_l has no l-torsion”.

The ℓ-adic cohomological interpretation of the L-function. Let X be a separated scheme of finite type over a finite field k, k̄ an algebraic closure of k, ℓ a prime invertible in k, and F = (Fₙ) an ℓ-adic sheaf on X_étale whose levels are flat over ℤ/ℓⁿ⁺¹ℤ. Then X has a compactification, and for every compactification j and every presentation #k = p ^ q: * the complexes RΓ_c(X_k̄, Fₙ) are perfect and the ℓ-adic L-function L_{ℤ_ℓ}(X, F) reduces modulo every ℓⁿ⁺¹ to det(1 - π_X^* T | RΓ_c(X_k̄, Fₙ))⁻¹; * for every c ∈ ℤ_ℓ⟦T⟧ with these reductions, L_{ℤ_ℓ}(X, F) = c if and only if L(X, F ⊗ ℚ_ℓ) = ∏ᵢ det(1 - π_X^* T | Hⁱ_c(X_k̄, F ⊗ ℚ_ℓ)) ^ ((-1) ^ (i + 1)).

public theorem LAdicSheaf.adicLFunction_eq_inv_charSeries_compactSupport (hℓ : (ℓ : k) ≠ 0) :
    haveI := isNoetherian_of_locallyOfFiniteType f
    ∀ (F : LAdicSheaf B X ℓ) (hF : ∀ n, PowExact ℓ (n + 1) (F.level n)),
    Nonempty (CompactificationOf (Over.mk f)) ∧
      ∀ (j : CompactificationOf (Over.mk f)) (p q : ℕ) [Fact p.Prime] [CharP k p]
        (hcard : Fintype.card k = p ^ q),
        ∃ hP : ∀ n, StacksDraft.Perfect.IsPerfect.{0, u + 1, u + 2} (DerivedCategory.Plus.ι.obj
            (compactSupportFrobeniusCohomology.{u, 0} (ZMod (ℓ ^ (n + 1))) f j kbar
              (LAdicSheaf.levelComplex B X ℓ F n))),
          (∀ n : ℕ, PowerSeries.map (PadicInt.toZModPow (n + 1))
              (LAdicSheaf.adicLFunction B X ℓ F hF f) =
            (((CategoryTheory.FilteredDerived.perfectDerivedCharSeries.{u + 2, 0, u + 1}
              (ZMod (ℓ ^ (n + 1)))
              ((LAdicSheaf.geometricPerfectTower B X ℓ f j kbar p q hcard F
                (LAdicSheaf.powExact_etaleLevel B X ℓ F hF) hP).obj n) (hP n)
              ((LAdicSheaf.geometricPerfectTower B X ℓ f j kbar p q hcard F
                (LAdicSheaf.powExact_etaleLevel B X ℓ F hF) hP).endo n))⁻¹ :
                (ZMod (ℓ ^ (n + 1)))⟦X⟧ˣ) : (ZMod (ℓ ^ (n + 1)))⟦X⟧)) ∧
          ∀ c : ℤ_[ℓ]⟦X⟧, (∀ n : ℕ, PowerSeries.map (PadicInt.toZModPow (n + 1)) c =
              (((CategoryTheory.FilteredDerived.perfectDerivedCharSeries.{u + 2, 0, u + 1}
                (ZMod (ℓ ^ (n + 1)))
                ((LAdicSheaf.geometricPerfectTower B X ℓ f j kbar p q hcard F
                  (LAdicSheaf.powExact_etaleLevel B X ℓ F hF) hP).obj n) (hP n)
                ((LAdicSheaf.geometricPerfectTower B X ℓ f j kbar p q hcard F
                  (LAdicSheaf.powExact_etaleLevel B X ℓ F hF) hP).endo n))⁻¹ :
                  (ZMod (ℓ ^ (n + 1)))⟦X⟧ˣ) : (ZMod (ℓ ^ (n + 1)))⟦X⟧)) →
            (LAdicSheaf.adicLFunction B X ℓ F hF f = c ↔
              LAdicSheaf.rationalLFunction B X ℓ F f =
                gradedCharSeries
                  (fun i =>
                    LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i)
                  (fun i => (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f j kbar
                    p q hcard F i).hom))
Tag 03V3, a theorem

Tag 03V3 in the Stacks Project.

Stacks.EtaleCohomology.isPerfect_compactSupport_and_sum_stalkTrace_eq_compactSupportLefschetzNumber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaConstructibleFiniteTor.lean, line 85. The attribute's comment: “Λ : Type (universe 0); X in a big étale site; K ∈ D_ctf(X, Λ) represented by a bounded below complex; RΓ_c(X_k̄, K) through any compactification (one exists by 0F41)”. References: SGA 4½ Rapport (4.10), “special case”; SGA 4½ Rapport (5.13), “more general”.

The trace formula ([Stacks, Tag 03V3]). Let k be a finite field with p ^ q elements and k̄ an algebraic closure of k, let X be a separated scheme of finite type over k (of any dimension), let Λ be a finite ring whose cardinality is invertible in k, and let K ∈ D_ctf(X, Λ). Then X has a compactification over k, and for every compactification j : X ⟶ X̄ the complex RΓ_c(X_k̄, K) = RΓ(X̄_k̄, (j_! K)|_{X̄_k̄}) lies in D_perf(Λ), and

∑_{x ∈ X(k)} Tr(π_x | K_x̄) = Tr(π_X^* | RΓ_c(X_k̄, K))

in Λ^natural, where the stalks K_x̄ at the rational points are perfect (so that their traces are defined), π_x is the geometric Frobenius acting on K_x̄ and π_X^* is the canonical Frobenius action on RΓ_c(X_k̄, K).

theorem isPerfect_compactSupport_and_sum_stalkTrace_eq_compactSupportLefschetzNumber
    (B : BigEtaleSite.{u}) (Λ : Type) [Ring Λ] [Finite Λ]
    {k : Type u} [Field k] [Fintype k] (kbar : Type u) [Field kbar] [IsAlgClosed kbar]
    [Algebra k kbar] [Algebra.IsAlgebraic k kbar] (p q : ℕ) [Fact p.Prime] [CharP k p]
    [CharP kbar p] (hcard : Fintype.card k = p ^ q)
    (hcop : Nat.Coprime (Nat.card Λ) (Fintype.card k))
    (X : B.Scheme) (f : X.obj ⟶ Spec (.of k)) [IsSeparated f] [LocallyOfFiniteType f]
    [QuasiCompact f] (K : CochainComplex.Plus (EtaleModules.{u, 0} Λ X.obj))
    (hK : IsCtf B X Λ (DerivedCategory.Q.obj K.obj)) :
    Nonempty (CompactificationOf (Over.mk f)) ∧
      ∀ j : CompactificationOf (Over.mk f),
        StacksDraft.Perfect.IsPerfect (DerivedCategory.Plus.ι.obj
          (compactSupportFrobeniusCohomology.{u, 0} Λ f j kbar K)) ∧
        ∃ (hX : StacksDraft.Perfect.IsPerfect (DerivedCategory.Plus.ι.obj
            (compactSupportFrobeniusCohomology.{u, 0} Λ f j kbar K)))
          (hs : ∀ x : rationalPoints f, StacksDraft.Perfect.IsPerfect
            (DerivedCategory.Q.obj (rationalPointStalkComplex.{u, 0} Λ kbar x.1 K))),
          ∑ᶠ x : rationalPoints f, perfectDerivedTrace Λ ⟨_, hs x⟩
              (DerivedCategory.Q.map (rationalPointStalkFrobenius.{u, 0} Λ kbar p q hcard x.1 K)) =
            canonicalCompactSupportLefschetzNumber.{u, 0} Λ f j kbar p q hcard K hX

Stacks.EtaleCohomology.perfectDerivedTrace_canonicalCompactSupportFrobenius_eq_sum_of_isCtf_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/TraceFormulaDctfFinal.lean, line 79. The attribute's comment: “RGamma_c(X_kbar, K) is perfect and the trace formula, for K in D_ctf(X, Lambda)”.

[Stacks, Tag 03V3]: the trace formula for D_ctf. Let X be a separated scheme of finite type over the finite field k with p ^ q elements, lying in the big étale site B, with a compactification j : X ⟶ X̄ (which defines RΓ_c), and k̄ an algebraic closure of k; let Λ be a finite ring (possibly noncommutative) with #Λ invertible in k, and K a bounded below complex of sheaves of Λ-modules on X_étale whose class lies in D_ctf(X, Λ). Then RΓ_c(X_k̄, K) is perfect, the stalks K_x̄ at the rational points are perfect, and Tr(π_X^* | RΓ_c(X_k̄, K)) = ∑_{x ∈ X(k)} Tr(π_x | K_x̄) in Λ^♮.

X is separated and of finite type over k as in the setting of Tag 03UG ("X/k as above"), where RΓ_c is defined (Definition 03UT); the instance Fintype (rationalPoints f) always holds (Stacks.EtaleCohomology.finite_rationalPoints).

theorem perfectDerivedTrace_canonicalCompactSupportFrobenius_eq_sum_of_isCtf_of_isSeparated
    (hΛ : (Nat.card Λ : k) ≠ 0) {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] [IsSeparated f] [QuasiCompact f]
    [Fintype (rationalPoints f)] (J : CompactificationOf (Over.mk f))
    (K : CochainComplex.Plus (EtaleModules.{u, 0} Λ X)) (hX : B.Contains X)
    (hK : IsCtf B (B.obj X hX) Λ (DerivedCategory.Q.obj K.obj)) :
    ∃ (hKs : HasPerfectStalks Λ K) (hperf : StacksDraft.Perfect.IsPerfect
        (DerivedCategory.Plus.ι.obj (compactSupportFrobeniusCohomology.{u, 0} Λ f J kbar K))),
      perfectDerivedTrace Λ ⟨_, hperf⟩ (DerivedCategory.Plus.ι.map
          (canonicalCompactSupportFrobenius.{u, 0} Λ f J kbar p q hcard K)) =
        ∑ x : rationalPoints f, perfectDerivedTrace Λ ⟨_, hKs (rationalGeometricPoint kbar x.1)⟩
          (DerivedCategory.Q.map (rationalPointStalkFrobenius.{u, 0} Λ kbar p q hcard x.1 K))
Tag 03V2, a theorem

Tag 03V2 in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.isZero_rationalGeometricCompactlySupportedCohomology_of_neg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricLAdicCompactSupport.lean, line 350. The attribute's comment: “the lower half of the degree bound: H^i_c(X_kbar, F) = 0 for i < 0”.

Hⁱ_c(X_k̄, F ⊗ Q_ℓ) = 0 for i < 0, for every ℓ-adic sheaf F on a separated scheme of finite type over a field, every extension field k̄ and every compactification: the lower half of the statement of Tag 03V2 that Hⁱ_c(X_k̄, F) is nonzero for 0 ≤ i ≤ 2 dim X only.

public theorem LAdicSheaf.isZero_rationalGeometricCompactlySupportedCohomology_of_neg
    (F : LAdicSheaf B X ℓ) (i : ℤ) (hi : i < 0) :
    IsZero (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i)

Stacks.EtaleCohomology.LAdicSheaf.traceFormula, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LAdicTraceFormulaFinal.lean, line 86. The attribute's comment: “finiteness, the degree bounds 0 <= i <= 2 dim X and the trace formula”. References: SGA 4½ Rapport (2.10), “special case”; SGA 7 I (0.1.1), “Q_ℓ clause of case 0.1.1”.

The trace formula for a ℚ_ℓ-sheaf. Let X be a separated scheme of finite type over a finite field k with p ^ q elements, k̄ an algebraic closure of k, ℓ a prime with ℓ ≠ p and F a ℚ_ℓ-sheaf on X (an ℓ-adic sheaf, tensored with ℚ_ℓ). Then * Hⁱ_c(X_k̄, F) is a finite dimensional ℚ_ℓ-vector space for every i, * it is nonzero only for 0 ≤ i ≤ 2 dim X, and * ∑_{x ∈ X(k)} Tr(π_x | F_x̄) = ∑ᵢ (-1)ⁱ Tr(π_X^* | Hⁱ_c(X_k̄, F)), the rational points being the closed points of residue degree one.

ℓ ≠ p is the chapter's standing convention; the statement is false for ℓ = p (X = 𝔸¹_k, F = ℚ_p: the right hand side is 0, the left hand side p ^ q).

theorem LAdicSheaf.traceFormula (hℓp : ℓ ≠ p) (F : LAdicSheaf.{u, u + 1} B X ℓ) :
    (∀ i : ℤ, Module.Finite ℚ_[ℓ]
      (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i)) ∧
    (∀ i : ℤ, Nontrivial
        (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i) →
      0 ≤ i ∧ ∃ d : ℕ, topologicalKrullDim X.1 = d ∧ i ≤ 2 * (d : ℤ)) ∧
    ∑ᶠ (x : closedPoints X.1) (_ : residueDegree f x.1 = 1),
        LinearMap.trace ℚ_[ℓ] _
          (LAdicSheaf.rationalStalkFrobenius B X ℓ F x.1 (finite_residueField f x.1 x.2)) =
      ∑ᶠ i : ℤ, (if Even i then (1 : ℚ_[ℓ]) else -1) *
        LinearMap.trace ℚ_[ℓ]
          (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar F i)
          (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f j kbar p q hcard F
            i).hom
Tag 03V4, a lemma

Tag 03V4 in the Stacks Project.

Stacks.InverseSystem.perfectTower_padicTrace_eq_alternating_trace_limitCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Homology/DerivedCategory/InverseSystem/PerfectTower/TraceFormula.lean, line 474. The attribute's comment: “parts (1), (2) and (3)”.

Stacks 03V4. Let ℓ be a prime. Suppose we have Kₙ ∈ D_perf(ℤ/ℓⁿ⁺¹ℤ), πₙ : Kₙ → Kₙ and isomorphisms φₙ : Kₙ₊₁ ⊗ᴸ_{ℤ/ℓⁿ⁺²ℤ} ℤ/ℓⁿ⁺¹ℤ → Kₙ compatible with πₙ₊₁ and πₙ — that is, a PerfectTower ℓ. Then

  1. the elements tₙ = Tr(πₙ | Kₙ) ∈ ℤ/ℓⁿ⁺¹ℤ form an element t_∞ = {tₙ} of ℤ_[ℓ], namely there is exactly one t_∞ ∈ ℤ_[ℓ] reducing to tₙ modulo ℓⁿ⁺¹ for every n;
  2. the ℤ_[ℓ]-module Hⁱ_∞ = limₙ Hⁱ(Kₙ) is finite and is nonzero for finitely many i only; and
  3. the operators Hⁱ(πₙ) : Hⁱ(Kₙ) → Hⁱ(Kₙ) are compatible with the transitions of the inverse system, hence define a unique πⁱ_∞ : Hⁱ_∞ → Hⁱ_∞ lying over them, and every such family satisfies ∑ᵢ (-1)ⁱ Tr(πⁱ_∞ | Hⁱ_∞ ⊗_{ℤ_[ℓ]} ℚ_[ℓ]) = t_∞.

Levels are indexed so that level n carries coefficients in ℤ/ℓⁿ⁺¹ℤ, avoiding the zero ring; (-1)ⁱ for i : ℤ is written as if Even i then 1 else -1.

public theorem perfectTower_padicTrace_eq_alternating_trace_limitCohomology
    {ℓ : ℕ} [Fact ℓ.Prime] (T : PerfectTower.{v} ℓ) :
    -- (1) the traces `tₙ` form an element `t_∞` of `ℤ_[ℓ]`
    (∃! t : ℤ_[ℓ], ∀ n : ℕ, PadicInt.toZModPow (n + 1) t = traceAtLevel T n) ∧
    -- (2) each `Hⁱ_∞` is a finite `ℤ_[ℓ]`-module, and only finitely many are nonzero
    (∀ i : ℤ, Module.Finite ℤ_[ℓ] (limitCohomology T i)) ∧
    {i : ℤ | Nontrivial (limitCohomology T i)}.Finite ∧
    -- (3) the `Hⁱ(πₙ)` are compatible with the transitions of the inverse system
    (∀ (i : ℤ) (n : ℕ), levelCohomologyEndoHom T i (n + 1) ≫ levelCohomologyTransition T i n =
        levelCohomologyTransition T i n ≫
          (ModuleCat.restrictScalars.{v} (levelCast ℓ n)).map (levelCohomologyEndoHom T i n)) ∧
    -- (3) and so define a unique family `πⁱ_∞` of endomorphisms of the `Hⁱ_∞`
    (∃! π : ∀ i : ℤ, limitCohomology T i →ₗ[ℤ_[ℓ]] limitCohomology T i,
        ∀ (i : ℤ) (n : ℕ) (a : limitCohomology T i),
          limitCohomologyProjection T i n (π i a) =
            levelCohomologyEndoₗ T i n (limitCohomologyProjection T i n a)) ∧
    -- (3) which satisfies `∑ᵢ (-1)ⁱ Tr(πⁱ_∞ | Hⁱ_∞ ⊗ ℚ_[ℓ]) = t_∞`
    (∀ t : ℤ_[ℓ], (∀ n : ℕ, PadicInt.toZModPow (n + 1) t = traceAtLevel T n) →
      ∀ π : ∀ i : ℤ, limitCohomology T i →ₗ[ℤ_[ℓ]] limitCohomology T i,
        (∀ (i : ℤ) (n : ℕ) (a : limitCohomology T i),
            limitCohomologyProjection T i n (π i a) =
              levelCohomologyEndoₗ T i n (limitCohomologyProjection T i n a)) →
          ∑ᶠ i : ℤ, (if Even i then (1 : ℚ_[ℓ]) else -1) *
              LinearMap.trace ℚ_[ℓ] (ℚ_[ℓ] ⊗[ℤ_[ℓ]] limitCohomology T i)
                (LinearMap.baseChange ℚ_[ℓ] (π i)) =
            (t : ℚ_[ℓ]))
Sources
LeanStacks.EtaleCohomology.lFunction_eq_inv_charSeries_compactSupport · Stacks.EtaleCohomology.FrobeniusMatrices.lFunction_eq_alternatingCharSeries · Stacks.EtaleCohomology.FrobeniusMatrices.lFunction_eq_alternatingCharSeries_iff · Stacks.EtaleCohomology.LAdicSheaf.rationalLFunction_eq_gradedCharSeries_compactSupportFrobenius · Stacks.EtaleCohomology.LAdicSheaf.adicLFunction_eq_inv_charSeries_compactSupport · Stacks.EtaleCohomology.isPerfect_compactSupport_and_sum_stalkTrace_eq_compactSupportLefschetzNumber · Stacks.EtaleCohomology.perfectDerivedTrace_canonicalCompactSupportFrobenius_eq_sum_of_isCtf_of_isSeparated · Stacks.EtaleCohomology.LAdicSheaf.isZero_rationalGeometricCompactlySupportedCohomology_of_neg

Section64.23 Constant sheaves#

Section 64.23 of the Stacks Project, Tag 03V7. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03V8, a lemma

Tag 03V8 in the Stacks Project.

Stacks.EtaleCohomology.LAdicSheaf.isRational_constantLFunction_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantSheafCurveCohomological.lean, line 204. The attribute's comment: “part (1): L(X, Q_ell) is a rational function, for X a smooth projective geometrically irreducible curve over a finite field and ell a prime different from the characteristic; its product with (1 - T)(1 - qT) is det(1 - pi_X^* T | H^1(X_kbar, Q_ell))”.

Tag 03V8, part (1). The L-function L(X, ℚ_ℓ) = ∏_{x ∈ |X|} (1 - T^{deg x})⁻¹ of a smooth, projective, geometrically irreducible curve over a finite field is a rational function: its product with a polynomial whose value at 0 is nonzero is a polynomial. (The polynomials are (1 - T)(1 - qT) and det(1 - π_X^* T | H¹(X_k̄, ℚ_ℓ)).)

theorem LAdicSheaf.isRational_constantLFunction_of_smoothProjectiveCurve (hℓp : ℓ ≠ p) :
    ∃ P Q : Polynomial ℚ_[ℓ], Q.eval 0 ≠ 0 ∧
      constantLFunction f ℚ_[ℓ] * (Q : PowerSeries ℚ_[ℓ]) = (P : PowerSeries ℚ_[ℓ])

Stacks.EtaleCohomology.LAdicSheaf.exists_integral_curveNumerator_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantSheafCurveCohomological.lean, line 223. The attribute's comment: “part (2), independence of ell: dim H^1(X_kbar, Q_ell) = 2g and the characteristic polynomial det(1 - pi_X^* T | H^1) is the image of the integral numerator of the zeta function of X, a polynomial over Z determined by the Euler product of X, in which ell does not occur”.

Tag 03V8, part (2), independence of ℓ. dim H¹(X_k̄, ℚ_ℓ) = 2g, and for every basis of H¹(X_k̄, ℚ_ℓ) the polynomial det(1 - π_X^* T | H¹) is the image of one integral polynomial of degree at most 2g with constant coefficient 1: the numerator L(X, ℤ)·(1 - T)(1 - qT) of the zeta function of X, in which ℓ does not occur.

theorem LAdicSheaf.exists_integral_curveNumerator_of_smoothProjectiveCurve (hℓp : ℓ ≠ p) :
    Module.finrank ℚ_[ℓ] (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f
        (CompactificationOf.ofProper f) kbar (LAdicSheaf.constantSystem B X ℓ) ((1 : ℕ) : ℤ)) =
      2 * genus f ∧
    ∀ bV : Module.Basis (Fin (2 * genus f)) ℚ_[ℓ]
        (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f
          (CompactificationOf.ofProper f) kbar (LAdicSheaf.constantSystem B X ℓ) ((1 : ℕ) : ℤ)),
      ∃ P : Polynomial ℤ, P.natDegree ≤ 2 * genus f ∧ P.coeff 0 = 1 ∧
        (P : PowerSeries ℤ) = integralCurveNumerator f (Fintype.card k) ∧
        P.map (Int.castRingHom ℚ_[ℓ]) = localCharPolynomial (LinearMap.toMatrix bV bV
          (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f
            (CompactificationOf.ofProper f) kbar p r hcard (LAdicSheaf.constantSystem B X ℓ)
              ((1 : ℕ) : ℤ)).hom) 1

Stacks.EtaleCohomology.LAdicSheaf.isIntegral_curveEigenvalue_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantSheafCurveCohomological.lean, line 245. The attribute's comment: “part (2): the eigenvalues alpha_1, ..., alpha_{2g} of pi_X^* on H^1(X_kbar, Q_ell) are algebraic integers, being the reciprocal roots of the integral numerator of the zeta function, of constant coefficient 1”.

Tag 03V8, part (2), integrality. The eigenvalues α_1, …, α_{2g} of π_X^* on H¹(X_k̄, ℚ_ℓ) are algebraic integers.

theorem LAdicSheaf.isIntegral_curveEigenvalue_of_smoothProjectiveCurve (hℓp : ℓ ≠ p)
    (bV : Module.Basis (Fin (2 * genus f)) ℚ_[ℓ]
      (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f
        (CompactificationOf.ofProper f) kbar (LAdicSheaf.constantSystem B X ℓ) ((1 : ℕ) : ℤ)))
    {Ω : Type*} [CommRing Ω] (φ : ℚ_[ℓ] →+* Ω) (α : Fin (2 * genus f) → Ω)
    (hα : (localCharPolynomial (LinearMap.toMatrix bV bV
        (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f
          (CompactificationOf.ofProper f) kbar p r hcard (LAdicSheaf.constantSystem B X ℓ)
            ((1 : ℕ) : ℤ)).hom) 1).map φ =
      ∏ i, (1 - Polynomial.C (α i) * Polynomial.X))
    (i : Fin (2 * genus f)) : IsIntegral ℤ (α i)

Stacks.EtaleCohomology.LAdicSheaf.natCard_fieldValuedPoints_eq_one_sub_sum_add_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantSheafCurveCohomological.lean, line 264. The attribute's comment: “part (3): #X(k_n) = 1 - sum_{i=1}^{2g} alpha_i^n + q^n for every extension k_n of k of degree n >= 1, alpha_i the eigenvalues of pi_X^* on H^1(X_kbar, Q_ell)”.

Tag 03V8, part (3). The number of points of X with values in an extension k_n of k of degree n ≥ 1 is #X(k_n) = 1 - ∑_{i=1}^{2g} α_i^n + q^n, α_i the eigenvalues of π_X^* on H¹(X_k̄, ℚ_ℓ).

theorem LAdicSheaf.natCard_fieldValuedPoints_eq_one_sub_sum_add_of_smoothProjectiveCurve
    (hℓp : ℓ ≠ p)
    (bV : Module.Basis (Fin (2 * genus f)) ℚ_[ℓ]
      (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f
        (CompactificationOf.ofProper f) kbar (LAdicSheaf.constantSystem B X ℓ) ((1 : ℕ) : ℤ)))
    {Ω : Type*} [CommRing Ω] (φ : ℚ_[ℓ] →+* Ω) (α : Fin (2 * genus f) → Ω)
    (hα : (localCharPolynomial (LinearMap.toMatrix bV bV
        (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f
          (CompactificationOf.ofProper f) kbar p r hcard (LAdicSheaf.constantSystem B X ℓ)
            ((1 : ℕ) : ℤ)).hom) 1).map φ =
      ∏ i, (1 - Polynomial.C (α i) * Polynomial.X))
    {n : ℕ} (hn : n ≠ 0) (K : Type u) [Field K] [Algebra k K] [Finite K]
    (hK : Module.finrank k K = n) :
    (Nat.card (fieldValuedPoints f K) : Ω) = 1 - ∑ i, α i ^ n + (Fintype.card k : Ω) ^ n

Stacks.EtaleCohomology.LAdicSheaf.norm_curveEigenvalue_lt_of_smoothProjectiveCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/ConstantSheafCurveCohomological.lean, line 319. The attribute's comment: “part (4): |alpha_i| < q for every eigenvalue alpha_i of pi_X^* on H^1(X_kbar, Q_ell) read in C; it follows from the Riemann hypothesis |alpha_i| = sqrt q, which the source states right after the lemma”.

Tag 03V8, part (4). Every eigenvalue α_i of π_X^* on H¹(X_k̄, ℚ_ℓ), read in ℂ along a ring map ℚ_ℓ → ℂ, has |α_i| < q.

theorem LAdicSheaf.norm_curveEigenvalue_lt_of_smoothProjectiveCurve (hℓp : ℓ ≠ p)
    (bV : Module.Basis (Fin (2 * genus f)) ℚ_[ℓ]
      (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f
        (CompactificationOf.ofProper f) kbar (LAdicSheaf.constantSystem B X ℓ) ((1 : ℕ) : ℤ)))
    (φ : ℚ_[ℓ] →+* ℂ) (α : Fin (2 * genus f) → ℂ)
    (hα : (localCharPolynomial (LinearMap.toMatrix bV bV
        (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f
          (CompactificationOf.ofProper f) kbar p r hcard (LAdicSheaf.constantSystem B X ℓ)
            ((1 : ℕ) : ℤ)).hom) 1).map φ =
      ∏ i, (1 - Polynomial.C (α i) * Polynomial.X))
    (i : Fin (2 * genus f)) : ‖α i‖ < (Fintype.card k : ℝ)
Tag 03V9, an exercise

Tag 03V9 in the Stacks Project.

Stacks.TraceFormula.exists_pow_mem_sector, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/NumberTheory/TraceFormula/SimultaneousPowersSector.lean, line 110.

Exercise 03V9. For complex numbers α 1, …, α n and a conic sector C_ε = {z | |arg z| < ε} with ε > 0 about the positive real axis, there is an integer k ≥ 1 with α 1 ^ k, …, α n ^ k all in C_ε.

theorem exists_pow_mem_sector (α : ι → ℂ) {ε : ℝ} (hε : 0 < ε) :
    ∃ k : ℕ, 1 ≤ k ∧ ∀ i, α i ^ k ∈ {z : ℂ | |z.arg| < ε}
Sources
LeanStacks.EtaleCohomology.LAdicSheaf.isRational_constantLFunction_of_smoothProjectiveCurve · Stacks.EtaleCohomology.LAdicSheaf.exists_integral_curveNumerator_of_smoothProjectiveCurve · Stacks.EtaleCohomology.LAdicSheaf.isIntegral_curveEigenvalue_of_smoothProjectiveCurve · Stacks.EtaleCohomology.LAdicSheaf.natCard_fieldValuedPoints_eq_one_sub_sum_add_of_smoothProjectiveCurve · Stacks.EtaleCohomology.LAdicSheaf.norm_curveEigenvalue_lt_of_smoothProjectiveCurve · Stacks.TraceFormula.exists_pow_mem_sector

Section64.27 Fundamental groups#

Section 64.27 of the Stacks Project, Tag 03VD. 4 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03VE, a definition

Tag 03VE in the Stacks Project.

AlgebraicGeometry.EtaleFundamentalGroup.IsOpenSubgroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/GaloisCategory/OpenSubgroups.lean, line 61.

Stacks Project, Tag 03VE. A subgroup of the étale fundamental group is open if it is the stabilizer of a point of the geometric fibre of some finite étale cover.

public abbrev IsOpenSubgroup {X : Scheme.{u}} [ConnectedSpace X]
    (x : GeometricPoint X) (H : Subgroup (EtaleFundamentalGroup X x)) : Prop
Tag 03VF, a theorem

Tag 03VF in the Stacks Project.

AlgebraicGeometry.exists_finiteEtaleEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/EtaleFundamental/FundamentalGroupTheorem.lean, line 85. The attribute's comment: “(3) the functor sending a finite étale Y/X to F_x(Y) with its natural action is an equivalence onto the finite discrete continuous π₁(X, x)-sets; (1) and (2) are not covered here”.

Stacks Project, Tags 0BND (1) and 03VF (3). Finite étale covers of a connected scheme X are equivalent to finite sets with a continuous action of π₁(X, x), by an equivalence whose underlying finite sets are the geometric fibres at x and whose action is evaluation of natural automorphisms.

theorem exists_finiteEtaleEquivalence (X : Scheme.{u}) [ConnectedSpace X]
    (x : GeometricPoint X) :
    ∃ E : FiniteEtaleOver X ≌ ContAction FintypeCat.{u} (EtaleFundamentalGroup X x),
      ∃ α : E.functor ⋙
          forget₂ (ContAction FintypeCat.{u} (EtaleFundamentalGroup X x))
            FintypeCat.{u} ⋙ FintypeCat.incl ≅ finiteEtaleFiberFunctor x,
        ∀ (Y : FiniteEtaleOver X) (σ : EtaleFundamentalGroup X x)
          (y : (E.functor.obj Y).obj.V.obj),
          (α.hom.app Y) (ConcreteCategory.hom ((E.functor.obj Y).obj.ρ σ).asHom y) =
            (σ.asIso.app Y).hom ((α.hom.app Y) y)

AlgebraicGeometry.EtaleFundamentalGroup.isOpen_coe_of_isOpenSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/GaloisCategory/OpenSubgroups.lean, line 93. The attribute's comment: “(1) the open subgroups are open subsets; that they are a neighbourhood basis of the identity is nhds_one_hasBasis_isOpenSubgroup, and (2) and (3) are not covered here”.

Stacks Project, Tag 03VF (1), openness. An open subgroup of the étale fundamental group is an open subset for the canonical topology.

theorem isOpen_coe_of_isOpenSubgroup {H : Subgroup (EtaleFundamentalGroup X x)}
    (hH : IsOpenSubgroup x H) : IsOpen (H : Set (EtaleFundamentalGroup X x))

AlgebraicGeometry.EtaleFundamentalGroup.nhds_one_hasBasis_isOpenSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/GaloisCategory/OpenSubgroups.lean, line 163. The attribute's comment: “(1) the open subgroups are a neighbourhood basis of the identity; that each of them is an open subset is isOpen_coe_of_isOpenSubgroup, and (2) and (3) are not covered here”.

Stacks Project, Tag 03VF (1). For the canonical topology on the étale fundamental group of a connected scheme, the open subgroups — the stabilizers of points of geometric fibres — form a fundamental system of neighbourhoods of the identity.

theorem nhds_one_hasBasis_isOpenSubgroup (X : Scheme.{u}) [ConnectedSpace X]
    (x : GeometricPoint X) :
    (nhds (1 : EtaleFundamentalGroup X x)).HasBasis (IsOpenSubgroup x)
      fun H ↦ (H : Set (EtaleFundamentalGroup X x))

AlgebraicGeometry.isProfiniteTop_etaleFundamentalGroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/ProfiniteFundamentalGroup.lean, line 53. The attribute's comment: “part (2)”.

Stacks Project, Tag 03VF, part (2). With its canonical topology the étale fundamental group of a connected scheme at a geometric point is a profinite group: it is a topological group by AlgebraicGeometry.etaleFundamentalGroupIsTopologicalGroup, and its underlying space is compact, Hausdorff and totally disconnected.

theorem isProfiniteTop_etaleFundamentalGroup (X : Scheme.{u}) [ConnectedSpace X]
    (x : GeometricPoint X) :
    Stacks.Chapter05.Tag_0BR1.IsProfiniteTop (EtaleFundamentalGroup X x)
Tag 03VG, a proposition

Tag 03VG in the Stacks Project.

AlgebraicGeometry.absoluteGaloisToFundamentalGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/FundamentalGroupIso.lean, line 475. The attribute's comment: “canonical generic-point homomorphism”.

The residue-field Galois action on the geometric fibre functor at sbar. Its action is specified below, independently of any isomorphism of groups.

public noncomputable def absoluteGaloisToFundamentalGroup
    [ConnectedSpace X] :
    Gal(sbar.residueField / X.residueField (sbar.hom default)) →ₜ*
      AlgebraicGeometry.EtaleFundamentalGroup X sbar

AlgebraicGeometry.fundamentalGroupIsoGalMaximalEtaleExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/FundamentalGroupIso.lean, line 671. The attribute's comment: “fundamental group”.

The étale fundamental group is the Galois group of the maximal extension unramified over the scheme, with canonicality specified below.

public noncomputable def fundamentalGroupIsoGalMaximalEtaleExtension
    [IsIntegral X] [IsNormal X]
    (hs : GeometricPoint.IsAlgebraic sbar)
    (hgeneric : sbar.hom default = genericPoint X) :
    AlgebraicGeometry.EtaleFundamentalGroup X sbar ≃ₜ*
      Gal(maximalEtaleExtension X sbar / X.residueField (sbar.hom default))

AlgebraicGeometry.fundamentalGroupIsoGalMaximalEtaleExtension_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/FundamentalGroupIso.lean, line 698. The attribute's comment: “compatibility with restriction”.

The canonical identification sends the generic-point homomorphism to restriction of absolute Galois automorphisms to the maximal étale extension.

public theorem fundamentalGroupIsoGalMaximalEtaleExtension_apply
    [IsIntegral X] [IsNormal X]
    (hs : GeometricPoint.IsAlgebraic sbar)
    (hgeneric : sbar.hom default = genericPoint X) :
    letI : Normal (X.residueField (sbar.hom default))
        (maximalEtaleExtension X sbar) :=
      normal_maximalEtaleExtension X sbar hs hgeneric
    ∀ σ : Gal(sbar.residueField / X.residueField (sbar.hom default)),
      fundamentalGroupIsoGalMaximalEtaleExtension X sbar hs hgeneric
          (absoluteGaloisToFundamentalGroup X sbar σ) =
        (AlgEquiv.restrictNormalHom (maximalEtaleExtension X sbar)) σ

AlgebraicGeometry.absoluteGaloisToFundamentalGroup_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/FundamentalGroupIso.lean, line 733. The attribute's comment: “canonical generic-point action”.

A generic-field automorphism acts on a finite étale geometric fibre by precomposition with the induced automorphism of the geometric point.

public theorem absoluteGaloisToFundamentalGroup_apply
    [ConnectedSpace X]
    (σ : Gal(sbar.residueField/X.residueField (sbar.hom default)))
    (Y : FiniteEtaleOver X)
    (p : finiteEtaleFiber sbar Y) :
    ((((absoluteGaloisToFundamentalGroup X sbar) σ).asIso.app Y).hom p).1 =
      Spec.map (CommRingCat.ofHom σ.toAlgHom.toRingHom) ≫ p.1

AlgebraicGeometry.maximalEtaleExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/MaximalEtaleExtension.lean, line 332. The attribute's comment: “maximal extension”.

The compositum of all finite extensions giving finite étale normalizations.

public def maximalEtaleExtension :
    IntermediateField (X.residueField (sbar.hom default)) sbar.residueField

AlgebraicGeometry.normal_maximalEtaleExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/MaximalEtaleExtension.lean, line 712. The attribute's comment: “Galois extension”.

The maximal finite-étale extension is normal over the function field.

public theorem normal_maximalEtaleExtension
    [IsIntegral X] [IsNormal X]
    (hs : GeometricPoint.IsAlgebraic sbar)
    (hgeneric : sbar.hom default = genericPoint X) :
    Normal (X.residueField (sbar.hom default)) (maximalEtaleExtension X sbar)

AlgebraicGeometry.le_maximalEtaleExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/MaximalEtaleExtension.lean, line 735. The attribute's comment: “maximality”.

The extension is largest among extensions with finite étale normalizations of all finite subextensions.

public theorem le_maximalEtaleExtension
    [IsIntegral X] [IsNormal X]
    (hs : GeometricPoint.IsAlgebraic sbar)
    (hgeneric : sbar.hom default = genericPoint X)
    (M : IntermediateField (X.residueField (sbar.hom default)) sbar.residueField)
    (hM : ∀ L : IntermediateField (X.residueField (sbar.hom default)) sbar.residueField,
      L ≤ M → FiniteDimensional (X.residueField (sbar.hom default)) L →
        FiniteEtaleNormalization X sbar L) :
    M ≤ maximalEtaleExtension X sbar

AlgebraicGeometry.finiteEtaleNormalization_of_le_maximalEtaleExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FundamentalGroup/NormalFunctionField/QuotientMap.lean, line 234. The attribute's comment: “finite étale normalization”.

Every finite subextension of the maximal extension gives a finite étale normalization.

public theorem finiteEtaleNormalization_of_le_maximalEtaleExtension
    [IsIntegral X] [IsNormal X]
    (hs : GeometricPoint.IsAlgebraic sbar)
    (hgeneric : sbar.hom default = genericPoint X)
    (L : IntermediateField (X.residueField (sbar.hom default)) sbar.residueField)
    [FiniteDimensional (X.residueField (sbar.hom default)) L]
    (hL : L ≤ maximalEtaleExtension X sbar) :
    FiniteEtaleNormalization X sbar L
Tag 03VH, a theorem

Tag 03VH in the Stacks Project.

Stacks.EtaleCohomology.IsMixedOfWeightLE.of_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FrobeniusWeights.lean, line 225. The attribute's comment: “the weight bound: the eigenvalues on H^i_c are algebraic numbers of absolute value q ^ (w / 2) with w an integer at most i. The weight datum is the cited theorem of [WeilII]; it is carried here for the two outer terms of the excision sequence of an open-closed decomposition of X and propagated to H^i_c(X)”.

Mixedness of weight at most i propagates along an exact sequence: in the excision sequence H^i_c(U) → H^i_c(X) → H^i_c(Z) of an open-closed decomposition X = U ⊔ Z, if the Frobenius actions on the two outer terms are mixed of weight at most i, then so is the Frobenius action on H^i_c(X), whose eigenvalues are therefore algebraic numbers of absolute value q ^ (w / 2) with w an integer at most i.

public theorem IsMixedOfWeightLE.of_exact {A B C : Type*} [AddCommGroup A] [Module K A]
    [AddCommGroup B] [Module K B] [AddCommGroup C] [Module K C] [FiniteDimensional K A]
    [FiniteDimensional K B] {fA : Module.End K A} {fB : Module.End K B} {fC : Module.End K C}
    {j : A →ₗ[K] B} {p : B →ₗ[K] C} (hA : IsMixedOfWeightLE q ι i fA)
    (hC : IsMixedOfWeightLE q ι i fC) (hj : ∀ a, j (fA a) = fB (j a))
    (hp : ∀ b, p (fB b) = fC (p b)) (hexact : LinearMap.ker p ≤ LinearMap.range j) :
    IsMixedOfWeightLE q ι i fB

Stacks.EtaleCohomology.isPureOfWeight_of_duality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/FrobeniusWeights.lean, line 241. The attribute's comment: “the final assertion, that w = i when X is smooth and projective of dimension d: proved from mixedness in degree i and in the dual degree 2 * d - i together with the Poincare duality matching of the two spectra”.

Poincaré duality turns mixedness into purity: if the Frobenius action f on H^i_c is mixed of weight at most i, the action g on the cohomology of the dual sheaf in degree 2 * d - i is mixed of weight at most 2 * d - i, and duality matches each eigenvalue α of f with the eigenvalue q ^ d / α of g, then f is pure of weight i.

public theorem isPureOfWeight_of_duality {d : ℤ} {g : Module.End K W}
    (hf : IsMixedOfWeightLE q ι i f) (hg : IsMixedOfWeightLE q ι (2 * d - i) g)
    (hdual : ∀ α : K, f.HasEigenvalue α → g.HasEigenvalue ((q : K) ^ d / α)) (hq : 1 < q) :
    IsPureOfWeight q ι i f

Stacks.EtaleCohomology.LAdicSheaf.weightBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/WeilIIWeightBound.lean, line 63. The attribute's comment: “the whole tag: the eigenvalues of pi_X^* on H^i_c(X_kbar, F_rho) are algebraic numbers of absolute value q^(w/2) with w <= i an integer, and w = i for X smooth and proper (the source says projective), for rho satisfying the conclusions of Deligne's conjecture along every embedding of Q_ell in C”.

Weil II (Tag 03VH; Deligne, La conjecture de Weil II). Let k be a finite field with p ^ q elements, k̄ an algebraic closure, ℓ ≠ p a prime, X connected and separated of finite type over k with a compactification j, and ρ : π₁(X, x̄) → GL_r(ℚ_ℓ) continuous, satisfying the conclusions of Deligne's conjecture (Stacks.EtaleCohomology.HasDeligneConclusions) along every embedding ι : ℚ_ℓ → ℂ. Then for every i the eigenvalues of π_X^* on Hⁱ_c(X_k̄, ℱ_ρ ⊗ ℚ_ℓ) (finite dimensional) are algebraic numbers of absolute value (p ^ q) ^ (w / 2) along ι with w ∈ ℤ, w ≤ i; and if X is smooth and proper over k (the source asks for projective), then w = i.

theorem LAdicSheaf.weightBound
    {k : Type u} [Field k] [Fintype k] (kbar : Type u) [Field kbar] [Algebra k kbar]
    [IsAlgClosure k kbar] (p q : ℕ) [Fact p.Prime] [CharP k p] (hcard : Fintype.card k = p ^ q)
    (hℓ : ℓ ≠ p) (X : B.Scheme) [IsNoetherian X.1] [ConnectedSpace X.1] (f : X.1 ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] (j : CompactificationOf (Over.mk f))
    (x : GeometricPoint X.1) {r : ℕ} (ρ : EtaleFundamentalGroup X.1 x →* GL (Fin r) ℚ_[ℓ])
    (hρ : Continuous ρ)
    (hD : ∀ ι : ℚ_[ℓ] →+* ℂ, HasDeligneConclusions (geometricFrobeniusFamily f x) p ι ρ) :
    (∀ (i : ℤ) (ι : ℚ_[ℓ] →+* ℂ),
      haveI : FiniteDimensional ℚ_[ℓ] (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X
        ℓ f j kbar (LAdicSheaf.representationSheaf B X x ρ hρ) i) :=
        LAdicSheaf.finiteDimensional_rationalGeometricCompactlySupportedCohomology B ℓ kbar p q
          hcard hℓ X f j _ i
      IsCharpolyMixedOfWeightLE (p ^ q) ι i
        (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f j kbar p q hcard
          (LAdicSheaf.representationSheaf B X x ρ hρ) i).hom) ∧
    (IsProper f → Smooth f → ∀ (i : ℤ) (ι : ℚ_[ℓ] →+* ℂ),
      haveI : FiniteDimensional ℚ_[ℓ] (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X
        ℓ f j kbar (LAdicSheaf.representationSheaf B X x ρ hρ) i) :=
        LAdicSheaf.finiteDimensional_rationalGeometricCompactlySupportedCohomology B ℓ kbar p q
          hcard hℓ X f j _ i
      IsCharpolyPureOfWeight (p ^ q) ι i
        (LAdicSheaf.rationalGeometricCompactlySupportedFrobenius B X ℓ f j kbar p q hcard
          (LAdicSheaf.representationSheaf B X x ρ hρ) i).hom)
Sources
LeanAlgebraicGeometry.EtaleFundamentalGroup.IsOpenSubgroup · AlgebraicGeometry.exists_finiteEtaleEquivalence · AlgebraicGeometry.EtaleFundamentalGroup.isOpen_coe_of_isOpenSubgroup · AlgebraicGeometry.EtaleFundamentalGroup.nhds_one_hasBasis_isOpenSubgroup · AlgebraicGeometry.isProfiniteTop_etaleFundamentalGroup · AlgebraicGeometry.absoluteGaloisToFundamentalGroup · AlgebraicGeometry.fundamentalGroupIsoGalMaximalEtaleExtension · AlgebraicGeometry.fundamentalGroupIsoGalMaximalEtaleExtension_apply

Section64.28 Profinite groups, cohomology and homology#

Section 64.28 of the Stacks Project, Tag 03VI. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03VI, the section

Tag 03VI in the Stacks Project.

Stacks.GroupCohomology.normalInvariantsFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/NormalQuotientInvariants.lean, line 187. The attribute's comment: “H⁰(N, -) takes discrete Γ-modules to discrete Γ/N-modules”.

Taking invariants under a normal subgroup N of a topological group Γ is a functor H⁰(N, -) from discrete Γ-modules to discrete Γ ⧸ N-modules.

def normalInvariantsFunctor :
    ContinuousGModule.{u, v} Γ ⥤ ContinuousGModule.{u, v} (Γ ⧸ N)

Stacks.GroupCohomology.derivedNormalInvariantsFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/NormalQuotientInvariants.lean, line 232. The attribute's comment: “the derived functor RH⁰(N, -) of the invariants functor”.

The right derived functor RH⁰(N, -) : D⁺(Mod_Γ) ⥤ D⁺(Mod_{Γ⧸N}) of taking invariants under a normal subgroup.

abbrev derivedNormalInvariantsFunctor :
    DerivedCategory.Plus (ContinuousGModule.{u, max u v} Γ) ⥤
      DerivedCategory.Plus (ContinuousGModule.{u, max u v} (Γ ⧸ N))

Declarations registered for the tag:

Sources
LeanStacks.GroupCohomology.normalInvariantsFunctor · Stacks.GroupCohomology.derivedNormalInvariantsFunctor · _root_.continuousGroupCohomologyFunctor · _root_.continuousGroupCohomology

Section64.29 Cohomology of curves, revisited#

Section 64.29 of the Stacks Project, Tag 03VJ. 3 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03VK, a lemma

Tag 03VK in the Stacks Project.

AlgebraicGeometry.compactSupportCanonicalTwistEquiv_galois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportCanonicalTwistGalois.lean, line 315.

H²_c(X_k̄, ℱ_ρ) = M_{π₁(X_k̄, η̄)}(-1) canonically, as Gal(k^{sep}/k)-modules. Let X be a geometrically connected smooth curve over a field k (f : X ⟶ Spec k), k̄ an algebraic closure of k, Λ a finite ring with n = #Λ invertible (in k̄, equivalently in k), η̄ a geometric point of X_k̄, and ℱ_ρ the sheaf on X_étale attached to a finite Λ-module M with a continuous action ρ of π₁(X, η̄) (AlgebraicGeometry.representationSheaf). The canonical Λ-linear isomorphism Ψ = AlgebraicGeometry.compactSupportCanonicalTwistEquiv : H²_c(X_k̄, ℱ_ρ) ≃ Hom(μ_n(k̄), M_N) carries the action of every σ ∈ Aut_k(k̄) on H²_c (induced by id × Spec σ) to the action g ↦ σ ∘ g ∘ σ⁻¹ on Hom(μ_n(k̄), M_N) = M_N(-1) (Stacks.EtaleCohomology.rootsOfUnityHomRepresentation).

Here M_N is the module of ρ_N = AlgebraicGeometry.geometricNormalCoinvariants, which is on the nose the coinvariants of M under the image N of π₁(X_k̄, η̄) in π₁(X, η̄) (AlgebraicGeometry.geometricNormalCoinvariantsEquiv), that is M_{π₁(X_k̄, η̄)} (AlgebraicGeometry.geometricCoinvariantsRangeEquiv); σ acts on it through π₁(X, η̄)/N ≅ Aut_k(k̄) (AlgebraicGeometry.geometricNormalCoinvariantsGaloisRepresentation, which is AlgebraicGeometry.geometricCoinvariantsGaloisRepresentation on the coinvariants by AlgebraicGeometry.geometricNormalCoinvariantsEquiv_galoisRepresentation). Hom(μ_n(k̄), M_N) with this action is the Tate twist M_N(-1): evaluation at any primitive n-th root of unity turns it into σ ↦ χ_cycl(σ)⁻¹ σ (Stacks.EtaleCohomology.rootsOfUnityHomRepresentation_apply_ofMul, into Stacks.EtaleCohomology.tateTwistNegOne).

Conventions: Aut_k(k̄) ≅ Gal(k^{sep}/k) by restriction (AlgebraicGeometry.separableClosureRestrictMulEquiv); H²_c is that of Remark 03UI (2), RΓ(X̄_k̄, (j_! ℱ)|_{X̄_k̄}) for a compactification j : X ⟶ X̄ over k, independent of j (geometricCompactSupportGroupCanonicalComparison, Tag 03UI); Λ : Type, a finite ring being isomorphic to one in Type.

Canonicity: Ψ is the source's own reformulation (Deligne), H²_c of the largest quotient ℱ_ρ ⟶ ℱ_{ρ_N} constant on X_k̄ followed by the trace on the smooth projective model of X_k̄ and evaluation at η̄; its values involve no choice, in particular no root of unity (AlgebraicGeometry.compactSupportCanonicalTwistEquiv_apply_ofMul). The isomorphism θ of AlgebraicGeometry.compactSupportGeometricCoinvariantsMap (and AlgebraicGeometry.compactSupportGaloisTwistEquiv built on it) is not used: it goes through AlgebraicGeometry.representationSheafPullbackIso, a chosen isomorphism ℱ_ρ|_{X_k̄} ≅ ℱ_{ρ|π₁(X_k̄)} (Tag 0DV6 only gives its existence). Two choices differ by a natural automorphism of restriction to π₁(X_k̄), such as ρ(c) for c centralising the image of π₁(X_k̄), which changes θ by the action of c on M_π; so Galois equivariance holds for θ only for suitable choices and cannot be proved for θ as defined.

theorem compactSupportCanonicalTwistEquiv_galois (σ : kbar ≃ₐ[k] kbar)
    (ρ : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom)))
    (x : letI := connectedSpace_of_isCurve B X f
      galoisCompactSupportCohomologyGroup.{u, 0} Λ f j kbar
        ((Stacks.DerivedIndexing.singlePlusFunctor _ 0).obj
          ((representationSheaf B X _ Λ).obj ρ)) ((2 : ℕ) : ℤ)) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    compactSupportCanonicalTwistEquiv B X f kbar Λ y j hn ρ
        ((galoisCompactSupportGroupAction Λ f j kbar σ
          ((Stacks.DerivedIndexing.singlePlusFunctor _ 0).obj
            ((representationSheaf B X _ Λ).obj ρ)) ((2 : ℕ) : ℤ)).hom x) =
      rootsOfUnityHomRepresentation k kbar (Fintype.card Λ) Λ
        (geometricNormalCoinvariantsGaloisRepresentation B X f kbar Λ y ρ) σ
        (compactSupportCanonicalTwistEquiv B X f kbar Λ y j hn ρ x)

Stacks.EtaleCohomology.compactlySupportedCohomologyTwo_galoisIso_tateTwistCoinvariants, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportTateTwistCoinvariants.lean, line 472. The attribute's comment: “the Galois-module conclusion, obtained from an equivariant nondegenerate pairing with μ_n coefficients. The right-hand side (M)_{π₁(X_k̄,η̄)}(-1) is constructed: coinvariants of Tag 03UD for the geometric fundamental group, the residual Gal(k^sep/k)-action through the fundamental exact sequence, and the Tate twist by -1 as the source defines it, χ_cycl(σ)⁻¹ composed with σ; the left-hand side is H²_c of Tag 0GJZ. Four inputs are explicit hypotheses because this library has no statement for them: the sheaf ℱ_ρ attached to ρ, which is Tag 0DV5 part (1), that is Tag 03RV and hence Tag 0245, so the sheaf is a variable and its link to ρ is carried by the pairing; the Galois action on H²_c and its compatibility, Tag 03ST in degree two and Tag 03Q9, of which only degree zero is available here; the fundamental exact sequence, Tags 03VJ, 0BTX and 0BNE, carried by the normal subgroup N and the isomorphism φ; and the trace isomorphism H²_c(X_k̄, μ_n) = ℤ/nℤ quoted inside the source's proof, carried by the nondegeneracy of the pairing. Tag 0F7I being absent, the compactification is an explicit argument as in Tag 0GJZ, and Xbar is pinned as the base change X ×_k k^sep by hbase. What is proved is that these inputs produce the twisted equivariant isomorphism: the Tate twist and the Galois equivariance of the identification”.

Stacks Project, Tag 03VK, as an isomorphism of Gal(k^{sep}/k)-modules.

The right-hand side is built here: Stacks.Trace.coinvariants of the restriction of ρ to the geometric fundamental group N, carrying the residual Galois action of Stacks.EtaleCohomology.galoisCoinvariantsRepresentation through the fundamental exact sequence φ, Tate-twisted by -1 as the source defines the twist. The left-hand side is the compactly supported cohomology module of Tag 0GJZ in degree two, carrying the Galois action galois.

The geometric input is a pairing of H²_c with the n-th roots of unity, taking values in the coinvariants, equivariant for the Galois actions on all three of its arguments and nondegenerate at one root of unity ζ₀. That is the shape in which the source supplies it: the twist in the conclusion is not assumed anywhere, it comes out of the computation of the Galois action on μ_n, which is the cyclotomic character. See the module docstring for the inputs carried as hypotheses and the tags they belong to.

hbase pins Xbar as the geometric curve X_{k̄} = X ×_k k^{sep}, so that the cohomology on the left is that of the base change and not of an unrelated scheme over k^{sep}; both the projection gbar and the structure morphism fbar are determined by that one isomorphism, so neither is an unconstrained choice. The identification itself plays no part in the twist bookkeeping, which is why the proof only destructures it.

public theorem compactlySupportedCohomologyTwo_galoisIso_tateTwistCoinvariants
    [LocallyOfFiniteType fbar] [QuasiCompact fbar] [IsSeparated fbar]
    [IsCurve k fX] [Smooth fX] [GeometricallyConnected fX]
    (gbar : Xbar ⟶ X)
    (hbase : ∃ e : Xbar ≅ pullback fX (Spec.map (CommRingCat.ofHom (algebraMap k ksep))),
      gbar = e.hom ≫ pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap k ksep))) ∧
        fbar = e.hom ≫ pullback.snd fX (Spec.map (CommRingCat.ofHom (algebraMap k ksep))))
    (etabar : AlgebraicGeometry.GeometricPoint X)
    (ρ : Representation Λ (EtaleFundamentalGroup X etabar) M)
    (N : Subgroup (EtaleFundamentalGroup X etabar)) [N.Normal]
    (φ : EtaleFundamentalGroup X etabar ⧸ N ≃* (ksep ≃ₐ[k] ksep))
    (galois : Representation Λ (ksep ≃ₐ[k] ksep)
      (compactlySupportedCohomologyTwo.{u, r} ksep fbar jbar Λ F))
    (pair : Additive (rootsOfUnity n ksep) →+
      (compactlySupportedCohomologyTwo.{u, r} ksep fbar jbar Λ F →ₗ[Λ]
        Stacks.Trace.coinvariants (ρ.comp N.subtype)))
    (hpair : ∀ (σ : ksep ≃ₐ[k] ksep) (ζ : rootsOfUnity n ksep)
        (x : compactlySupportedCohomologyTwo.{u, r} ksep fbar jbar Λ F),
      pair (Additive.ofMul (galoisRootsOfUnity k ksep n σ ζ)) (galois σ x) =
        galoisCoinvariantsRepresentation ρ N φ σ (pair (Additive.ofMul ζ) x))
    (ζ₀ : rootsOfUnity n ksep)
    (hζ₀ : Function.Bijective (pair (Additive.ofMul ζ₀))) :
    ∃ θ : compactlySupportedCohomologyTwo.{u, r} ksep fbar jbar Λ F ≃ₗ[Λ]
        Stacks.Trace.coinvariants (ρ.comp N.subtype),
      ∀ (σ : ksep ≃ₐ[k] ksep)
        (x : compactlySupportedCohomologyTwo.{u, r} ksep fbar jbar Λ F),
        θ (galois σ x) =
          tateTwistNegOne k ksep n Λ (galoisCoinvariantsRepresentation ρ N φ) σ (θ x)
Tag 03VL, a remark

Tag 03VL in the Stacks Project.

AlgebraicGeometry.isZero_curveCompactlySupportedCohomologyZero_of_not_isProjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveRepresentationCohomology.lean, line 130. The attribute's comment: “H⁰_c(X_k̄, ℱ_ρ) = 0 if X is not projective, H_c in the sense of Tag 0GJZ, for every algebraic extension K of k in place of k̄”. References: SGA 5 VII (7.1.1), “b), special case”.

Stacks Project, Tag 03VL, last assertion: H⁰_c(X_K, ℱ_ρ) = 0 if X is not projective. For a geometrically connected smooth curve X over k which is not projective, an algebraic extension K of k, a finite ring Λ and a finite Λ-module M with a continuous action ρ of π₁(X, η̄), the zeroth compactly supported cohomology module, in the sense of Tag 0GJZ, of the restriction of ℱ_ρ to X_K vanishes, through any compactification of X_K over K.

theorem isZero_curveCompactlySupportedCohomologyZero_of_not_isProjective
    (hnp : ¬ IsProjective f)
    (jbar : CompactificationOf (Over.mk (pullback.snd (Over.mk f).hom (specAlgebraMap k K))))
    (y : GeometricPoint (fieldBaseChange (Over.mk f) K))
    (M : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{r, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f K
          (contains_fieldBaseChange_of_isCurve B X f K)).hom))) :
    letI := connectedSpace_of_isCurve B X f
    IsZero ((compactlySupportedCohomologyGroup.{u, r} K
        (pullback.snd (Over.mk f).hom (specAlgebraMap k K)) jbar Λ 0).obj
      ((DerivedCategory.Plus.singleFunctor
        (EtaleModules.{u, r} Λ (fieldBaseChange (Over.mk f) K)) 0).obj
          ((geometricRepresentationSheaf B X
            (y.map (fieldBaseChangeObjProj B X f K
              (contains_fieldBaseChange_of_isCurve B X f K)).hom) Λ f K).obj M)))

AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricGlobalSectionsCanonical.lean, line 294. The attribute's comment: “H⁰(X_k̄, ℱ_ρ) = M^{π₁(X_k̄,η̄)}: the canonical identification, by evaluation at η̄”.

Stacks Project, Tag 03VL, degree zero, canonically: H⁰(X_k̄, ℱ_ρ) = M^{π₁(X_k̄, η̄)}. The evaluation at the geometric point η̄ of X_k̄ identifies the global sections of the restriction of ℱ_ρ to X_k̄ with the π₁(X_k̄, η̄)-invariants of M. It involves no choice: it is built from the explicit sheaf ℱ_ρ of Tag 0DV5 and evaluation, not from the existence-only comparison of Tag 0DV6. Its naturality in ρ is geometricGlobalSectionsInvariantsEquiv_naturality and its Galois equivariance geometricGlobalSectionsInvariantsEquiv_galois. The source states this for X projective and #Λ ∈ k^*; neither is used.

def geometricGlobalSectionsInvariantsEquiv (ρ : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom))) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    ↑((etaleModuleGlobalSections.{u, 0} Λ (fieldBaseChange (Over.mk f) kbar)).obj
        (geometricRepresentationRestriction B X f kbar Λ y ρ)) ≃ₗ[Λ]
      ↑((finiteTypeContinuousModuleInvariants Λ
        (EtaleFundamentalGroup (fieldBaseChange (Over.mk f) kbar) y)).obj
          ((finiteTypeContinuousModuleRes Λ (etaleFundamentalGroupMap
            (fieldBaseChangeObjProj B X f kbar (contains_fieldBaseChange_of_isCurve B X f kbar)).hom
              y)).obj ρ))

AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricGlobalSectionsCanonical.lean, line 326. The attribute's comment: “H⁰(X_k̄, ℱ_ρ) = M^{π₁(X_k̄,η̄)} functorially in ρ”.

Stacks Project, Tag 03VL, degree zero: the identification is natural in ρ. For φ : ρ ⟶ ρ', it carries the map induced by φ on global sections to φ on invariants.

theorem geometricGlobalSectionsInvariantsEquiv_naturality
    {ρ ρ' : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom))} (φ : ρ ⟶ ρ')
    (z : letI := connectedSpace_of_isCurve B X f
      ↑((etaleModuleGlobalSections.{u, 0} Λ (fieldBaseChange (Over.mk f) kbar)).obj
        (geometricRepresentationRestriction B X f kbar Λ y ρ))) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    (geometricGlobalSectionsInvariantsEquiv B X f kbar Λ y ρ'
        ((etaleModuleGlobalSections.{u, 0} Λ (fieldBaseChange (Over.mk f) kbar)).map
          ((etaleModuleInverseImage.{u, 0} Λ (fieldBaseChangeProj (Over.mk f) kbar)).map
            ((representationSheaf B X (y.map (fieldBaseChangeObjProj B X f kbar
              (contains_fieldBaseChange_of_isCurve B X f kbar)).hom) Λ).map φ)) z)).1 =
      φ.hom.hom.hom.hom.hom (geometricGlobalSectionsInvariantsEquiv B X f kbar Λ y ρ z).1

AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv_galois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricGlobalSectionsCanonical.lean, line 350. The attribute's comment: “H⁰(X_k̄, ℱ_ρ) = M^{π₁(X_k̄,η̄)} as Gal(k̄/k) = π₁(X,η̄)/π₁(X_k̄,η̄)-modules”.

Stacks Project, Tag 03VL, degree zero: the identification is Galois-equivariant. For γ ∈ π₁(X, η̄) with image σ ∈ Aut(k̄/k) = π₁(X, η̄)/π₁(X_k̄, η̄), it carries the action of σ on H⁰(X_k̄, ℱ_ρ) (through id × Spec σ on X_k̄) to the action of ρ(γ) on M^{π₁(X_k̄, η̄)}.

theorem geometricGlobalSectionsInvariantsEquiv_galois (ρ : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom)))
    (γ : letI := connectedSpace_of_isCurve B X f
      EtaleFundamentalGroup X.1 (y.map (fieldBaseChangeObjProj B X f kbar
        (contains_fieldBaseChange_of_isCurve B X f kbar)).hom))
    (z : letI := connectedSpace_of_isCurve B X f
      ↑((etaleModuleGlobalSections.{u, 0} Λ (fieldBaseChange (Over.mk f) kbar)).obj
        (geometricRepresentationRestriction B X f kbar Λ y ρ))) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    (geometricGlobalSectionsInvariantsEquiv B X f kbar Λ y ρ
        ((fieldBaseChangeGlobalSectionsGaloisAction Λ (Over.mk f) kbar
          (geometricQuotientGaloisEquiv B X f kbar y (QuotientGroup.mk γ)) _).hom z)).1 =
      (finiteTypeContinuousModuleRepresentation Λ _ ρ) γ
        (geometricGlobalSectionsInvariantsEquiv B X f kbar Λ y ρ z).1

Stacks.EtaleCohomology.LAdicSheaf.subsingleton_rationalGeometricCompactlySupportedCohomology_zero_of_not_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LisseCompactSupportZero.lean, line 201. The attribute's comment: “last assertion: H^0_c(X_kbar, F_rho) = 0 when X is not projective (here: not proper over k)”.

Stacks Project, Tag 03VL, last assertion: if X is not projective, then H⁰_c(X_k̄, ℱ_ρ) = 0. Here X is a smooth geometrically connected curve over the finite field k, ρ = τ : π₁(X, x̄) → GL_r(Q_ℓ) is continuous, H⁰_c(X_k̄, ℱ_ρ) is the compactly supported cohomology of ℱ_τ ⊗ Q_ℓ on X_k̄ for an algebraic closure k̄ (for any compactification), and "not projective" is ¬ IsProper f (a projective curve is proper over k, so this is the weaker hypothesis). A connected smooth curve which is not proper is affine (Tag 0A28).

theorem LAdicSheaf.subsingleton_rationalGeometricCompactlySupportedCohomology_zero_of_not_isProper
    [ConnectedSpace X.1] [SmoothOfRelativeDimension 1 f] [IsAlgClosure k kbar]
    (hf : ¬ IsProper f) (x : GeometricPoint X.1) {r : ℕ}
    (τ : EtaleFundamentalGroup X.1 x →* GL (Fin r) ℚ_[ℓ]) (hτ : Continuous τ) :
    Subsingleton (LAdicSheaf.rationalGeometricCompactlySupportedCohomology B X ℓ f j kbar
      (LAdicSheaf.representationSheaf B X x τ hτ) 0)

Stacks.EtaleCohomology.compactlySupportedSections_eq_bot_of_not_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/LocallyConstantCompactSupport.lean, line 321. The attribute's comment: “the non-projective assertion H^0_c = 0, at the level of the sections of proper support of Tag 0F72: for an arbitrary locally constant abelian sheaf in place of the sheaf ℱ_ρ attached to a representation, which needs part (1) of Tag 0DV5 and hence Tag 0245, and on an integral scheme not proper over the base field in place of a non-projective geometrically connected smooth curve. The identification of these sections with H^0_c is Tag 0GK1, not available here; the two projective assertions of the tag are not proved, nor is the Tate twist they carry”. References: SGA 4½ Sommes trig (1.18), “Clause b)”.

On an integral scheme which is not proper over the base field, a global section of a locally constant abelian sheaf on the small étale site whose support is proper over the base field is zero.

public theorem compactlySupportedSections_eq_bot_of_not_isProper [IsIntegral X]
    (hf : ¬ IsProper f) [IsLocallyConstant (SmallEtale.topology B X hX) F] :
    compactlySupportedSections k X f B hX F = ⊥

AlgebraicGeometry.properCurveCompactSupportTwoEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/Remark03VL.lean, line 113. The attribute's comment: “H²_c(X_k̄, ℱ_ρ) = M_{π₁(X_k̄,η̄)}(-1) for X projective (here: proper): the root-of-unity free (ζ-independent) Λ-linear identification, M(-1) being Hom(μ_n, M); functoriality in ρ is properCurveCompactSupportTwoEquiv_naturality”.

Stacks Project, Tag 03VL, degree two: H²_c(X_k̄, ℱ_ρ) = M_{π₁(X_k̄, η̄)}(-1) for X projective. For a geometrically connected smooth proper curve X over a field k, an algebraic closure k̄, a finite ring Λ with #Λ invertible, and a finite Λ-module M with a continuous action ρ of π₁(X, η̄), the compactly supported cohomology H²_c(X_k̄, ℱ_ρ), X being its own compactification, is M_{π₁(X_k̄, η̄)}(-1) = Hom(μ_n(k̄), M_{π₁(X_k̄, η̄)}), n = #Λ, with no choice of a root of unity. The source assumes X projective; a projective morphism is proper (AlgebraicGeometry.isProper_of_isProjectiveMorphism), and for a curve the two are equivalent (Tag 0A26), so properness is the hypothesis. Its functoriality in ρ is AlgebraicGeometry.properCurveCompactSupportTwoEquiv_naturality.

def properCurveCompactSupportTwoEquiv [IsProper f]
    (ρ : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom))) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    galoisCompactSupportCohomologyGroup.{u, 0} Λ f (CompactificationOf.ofProper f) kbar
        ((Stacks.DerivedIndexing.singlePlusFunctor _ 0).obj
          ((representationSheaf B X _ Λ).obj ρ)) ((2 : ℕ) : ℤ) ≃ₗ[Λ]
      (Additive (_root_.rootsOfUnity (Fintype.card Λ) kbar) →+
        Stacks.Trace.coinvariants (geometricRepresentation B X f kbar Λ y ρ))

AlgebraicGeometry.properCurveCompactSupportTwoEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/Remark03VL.lean, line 131. The attribute's comment: “H²_c(X_k̄, ℱ_ρ) = M_{π₁(X_k̄,η̄)}(-1) is functorial in ρ”.

Stacks Project, Tag 03VL, degree two, functoriality in ρ. For v : ρ ⟶ ρ', the identification H²_c(X_k̄, ℱ_ρ) = M_{π₁(X_k̄, η̄)}(-1) carries the map induced by v on H²_c to the map induced by v on coinvariants.

theorem properCurveCompactSupportTwoEquiv_naturality [IsProper f]
    {ρ ρ' : letI := connectedSpace_of_isCurve B X f
      FiniteTypeContinuousModule.{0, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f kbar
          (contains_fieldBaseChange_of_isCurve B X f kbar)).hom))} (v : ρ ⟶ ρ')
    (x : letI := connectedSpace_of_isCurve B X f
      letI := connectedSpace_fieldBaseChange f kbar
      galoisCompactSupportCohomologyGroup.{u, 0} Λ f (CompactificationOf.ofProper f) kbar
        ((Stacks.DerivedIndexing.singlePlusFunctor _ 0).obj
          ((representationSheaf B X _ Λ).obj ρ)) ((2 : ℕ) : ℤ)) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f kbar
    properCurveCompactSupportTwoEquiv B X f kbar Λ y hn ρ'
        (((DerivedCategory.Plus.homologyFunctor (ModuleCat.{u + 1} Λ) ((2 : ℕ) : ℤ)).map
          (galoisCompactSupportCohomologyMap Λ f (CompactificationOf.ofProper f) kbar
            ((Stacks.DerivedIndexing.singlePlusFunctor _ 0).map
              ((representationSheaf B X _ Λ).map v)))).hom x) =
      (geometricCoinvariantsMap B X f kbar Λ y v).toAddMonoidHom.comp
        (properCurveCompactSupportTwoEquiv B X f kbar Λ y hn ρ x)
Tag 03VM, a proposition

Tag 03VM in the Stacks Project.

AlgebraicGeometry.compactSupportDerivedHomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportDerivedHomologyIso.lean, line 163. The attribute's comment: “third assertion (the derived version of the homological half): RΓ_c(X_k̄, ℱ_ρ) ≅ LH₀(π₁(X_k̄, η̄), M(-1))[-2] in the derived category of Λ[[Aut(k̄/k)]]-modules, natural in (M, ρ)”.

Tag 03VM, homological derived clause: RΓ_c(X_k̄, ℱ_ρ) ≅ LH₀(π₁(X_k̄, η̄), M(-1))[-2] in the derived category of Λ[[Aut(k̄/k)]]-modules (Aut(k̄/k) ≅ Ẑ for k finite), naturally in the finite Λ-module M with continuous action ρ of π₁(X, η̄). Here X is a geometrically connected smooth curve over k with X_k̄ ≇ 𝐏¹_k̄, k̄ is an algebraic closure of k separable over k (automatic for k finite), and Λ is a finite ring with #Λ invertible in k. The left side is the Galois-equivariant RΓ_c of Remark 03UI (2), M(-1) = Hom(μ_n(k̄), M), and LH₀ is the derived functor of the coinvariants in the continuous sense, M ⊗^L_{Λ[[π₁(X_k̄)]]} Λ computed on pseudocompact modules (see the module docstring).

def compactSupportDerivedHomologyIso (hΛ : IsUnit ((Nat.card Λ : ℕ) : k))
    (hP : ¬ ∃ e : fieldBaseChange (Over.mk f) K ≅ projectiveSpaceOver 1 (Spec (.of K)),
      e.hom ≫ (projectiveSpaceOver 1 (Spec (.of K)) ↘ Spec (.of K)) =
        pullback.snd (Over.mk f).hom (specAlgebraMap k K)) :
    letI := connectedSpace_of_isCurve B X f
    haveI : IsAlgClosed K := IsAlgClosure.isAlgClosed k
    haveI : Algebra.IsAlgebraic k K := IsAlgClosure.isAlgebraic
    geometricGaloisCompactSupportDerived B X f K y Λ j ≅
      (geometricTateTwist B X f K y Λ ⋙ geometricDerivedHomology B X f K y Λ) ⋙
        shiftFunctor _ (-2 : ℤ)

AlgebraicGeometry.compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportGroupHomologyGaloisNotProjectiveLine.lean, line 46. The attribute's comment: “second assertion: H_c^{2-i}(X_k̄, ℱ_ρ) ≅ H_i(π₁(X_k̄, η̄), M)(-1) as homological δ-functors in (M, ρ)”.

When X_k̄ ≇ ℙ¹_k̄, the isomorphism H_c^{2-i}(X_k̄, ℱ_ρ) ≅ H_i(π₁(X_k̄, η̄), M)(-1) of homological δ-functors, extending the choice-free identification H²_c(X_k̄, ℱ_ρ) = Hom(μ_n(k̄), M_{π₁(X_k̄, η̄)}) of Tag 03VK.

def compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f K
    haveI : IsAlgClosed K := IsAlgClosure.isAlgClosed k
    letI : Fintype Λ := Fintype.ofFinite Λ
    compactSupportRepresentationHomology B X
        (y.map (fieldBaseChangeObjProj B X f K (contains_fieldBaseChange_of_isCurve B X f K)).hom)
        Λ f j K ≅
      geometricGroupHomologyTwist B X f K Λ y (isUnit_card_fieldBaseChange K Λ hΛ)

AlgebraicGeometry.compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine_galois, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportGroupHomologyGaloisNotProjectiveLine.lean, line 76. The attribute's comment: “second assertion, Galois action: the isomorphism H_c^{2-i}(X_k̄, ℱ_ρ) ≅ H_i(π₁(X_k̄, η̄), M)(-1) commutes with every σ ∈ Aut_k(k̄)”.

The isomorphism H_c^{2-i}(X_k̄, ℱ_ρ) ≅ H_i(π₁(X_k̄, η̄), M)(-1) is Gal(k^{sep}/k)-equivariant: for every σ ∈ Aut_k(k̄) the action of σ on H_c^{2-i}(X_k̄, ℱ_ρ) (AlgebraicGeometry.compactSupportRepresentationHomologyGalois) corresponds, in every degree, to the action of σ on H_i(π₁(X_k̄, η̄), M)(-1) (AlgebraicGeometry.geometricGroupHomologyTwistGalois), which in degree zero is f ↦ σ ∘ f ∘ σ⁻¹ on Hom(μ_n(k̄), M_{π₁(X_k̄, η̄)}).

theorem compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine_galois (σ : K ≃ₐ[k] K) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f K
    letI := QuasiCompact.compactSpace_of_compactSpace f
    letI := quasiSeparatedSpace_of_quasiSeparated f
    haveI : IsAlgClosed K := IsAlgClosure.isAlgClosed k
    haveI : Algebra.IsAlgebraic k K := IsAlgClosure.isAlgebraic
    letI : Fintype Λ := Fintype.ofFinite Λ
    compactSupportRepresentationHomologyGalois B X
        (y.map (fieldBaseChangeObjProj B X f K (contains_fieldBaseChange_of_isCurve B X f K)).hom)
        Λ f j K σ ≫
        (compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine B X f K Λ y j hΛ hP).hom =
      (compactSupportGroupHomologyTwistIsoOfNotIsoProjectiveLine B X f K Λ y j hΛ hP).hom ≫
        geometricGroupHomologyTwistGalois B X f K Λ y σ j (isUnit_card_fieldBaseChange K Λ hΛ)
          (isIso_geometricComparison_of_not_iso_projectiveLine B X f K Λᵐᵒᵖ y
            (isUnit_natCard_mulOpposite Λ hΛ) hP)

AlgebraicGeometry.isUniversal_compactSupportRepresentationHomology_of_not_iso_projectiveLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CompactSupportGroupHomologyNotProjectiveLine.lean, line 59. The attribute's comment: “first assertion: (M, ρ) ↦ H_c^{2-i}(X_k̄, ℱ_ρ) is a universal homological δ-functor, i.e. the left derived functors of (M, ρ) ↦ H_c^2(X_k̄, ℱ_ρ)”.

(M, ρ) ↦ H_c^{2-i}(X_k̄, ℱ_ρ) are the left derived functors of (M, ρ) ↦ H_c^2(X_k̄, ℱ_ρ): they form a universal homological δ-functor, for X_k̄ ≇ ℙ¹_k̄ and #Λ invertible in k.

theorem isUniversal_compactSupportRepresentationHomology_of_not_iso_projectiveLine :
    letI := connectedSpace_of_isCurve B X f
    haveI : IsAlgClosed K := IsAlgClosure.isAlgClosed k
    (compactSupportRepresentationHomology B X
      (y.map (fieldBaseChangeObjProj B X f K (contains_fieldBaseChange_of_isCurve B X f K)).hom)
      Λ f j K).IsUniversal

Stacks.EtaleCohomology.CurveFundamentalGroup.deltaFunctorIsoLeftDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 146. The attribute's comment: “first assertion, by the source's own proof (both sides are universal δ-functors): a homological δ-functor whose positive degrees vanish on projectives IS the left derived functor of its degree-zero part. The compactly supported cohomology δ-functor i ↦ H_c^{2-i}(X_k̄, F_ρ) of the pair (M, ρ) is the hypothesis Hc and its vanishing on projectives the hypothesis hvanish, since the étale input (0GIY, 03QW, 0GK1, 03VL) is not available; no Tate twist is constructed”.

[Stacks, Tag 03VM], first assertion. A homological δ-functor Hc whose positive-degree parts vanish on projective objects, and whose degree-zero part is identified with the degree-zero left derived functor of an additive T, is the left derived functor of T: the identification extends uniquely to an isomorphism of homological δ-functors.

In the source Hc is i ↦ H_c^{2-i}(X_{k̄}, F_ρ) on the category of pairs (M, ρ) and T is (M, ρ) ↦ H_c^2(X_{k̄}, F_ρ); the proof is the source's, that both sides are universal δ-functors.

def deltaFunctorIsoLeftDerived (Hc : HomologicalDeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    (hvanish : ∀ (n : ℕ) (P : A) [Projective P], IsZero ((Hc.functor (n + 1)).obj P))
    (base : Hc.functor 0 ≅ T.leftDerived 0) :
    Hc ≅ T.leftDerivedHomologicalDeltaFunctor

Stacks.EtaleCohomology.CurveFundamentalGroup.isoLeftDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 158. The attribute's comment: “first assertion read degreewise: H_c^{2-i} ≅ L_i(H_c^2), with the compactly supported cohomology δ-functor and its vanishing on projectives as hypotheses”.

[Stacks, Tag 03VM], first assertion, degree by degree: Hcᵢ ≅ Lᵢ T.

def isoLeftDerived (Hc : HomologicalDeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    (hvanish : ∀ (n : ℕ) (P : A) [Projective P], IsZero ((Hc.functor (n + 1)).obj P))
    (base : Hc.functor 0 ≅ T.leftDerived 0) (i : ℕ) :
    Hc.functor i ≅ T.leftDerived i

Stacks.EtaleCohomology.CurveFundamentalGroup.isoLeftDerivedOfRightExact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 172. The attribute's comment: “first assertion with a right exact degree-zero part: from H_c^2 ≅ T with T right exact, H_c^{2-i} ≅ L_i T for every i. The δ-functor and the vanishing on projectives are hypotheses”.

[Stacks, Tag 03VM], first assertion with the degree-zero hypothesis in its usable form. When T is right exact — as (M, ρ) ↦ H_c^2(X_{k̄}, F_ρ) is, being the final term of the long exact sequence — the degree-zero input is an identification Hc₀ ≅ T itself, because L₀ T ≅ T.

def isoLeftDerivedOfRightExact (Hc : HomologicalDeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    [PreservesFiniteColimits T]
    (hvanish : ∀ (n : ℕ) (P : A) [Projective P], IsZero ((Hc.functor (n + 1)).obj P))
    (base : Hc.functor 0 ≅ T) (i : ℕ) :
    Hc.functor i ≅ T.leftDerived i

Stacks.EtaleCohomology.CurveFundamentalGroup.compactSupportIsoGroupHomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 193. The attribute's comment: “second assertion: two homological δ-functors that both vanish on projectives in positive degree and agree in degree zero agree in every degree, which is the source's proof of H_c^{2-i} = H_i(π₁(X_k̄, η̄), M)(-1). The twisted group homology side is the hypothesis Hgp (group homology of a profinite group is the absent homological half of 03VI, and no Tate twist is formalized) and the degree-zero base case is the hypothesis base (03VK)”.

[Stacks, Tag 03VM], second assertion. Two homological δ-functors whose positive-degree parts vanish on projective objects and whose degree-zero parts are identified are identified in every degree.

This is the "so" of the proposition: with Hc the compactly supported cohomology i ↦ H_c^{2-i}(X_{k̄}, F_ρ), with Hgp the twisted group homology i ↦ H_i(π₁(X_{k̄}, η̄), M)(-1), and with base the isomorphism of [Stacks, Tag 03VK], both sides are universal δ-functors and therefore agree in all degrees. Neither side is constructed here — see the module docstring.

def compactSupportIsoGroupHomology (Hc Hgp : HomologicalDeltaFunctor A B)
    (hHc : ∀ (n : ℕ) (P : A) [Projective P], IsZero ((Hc.functor (n + 1)).obj P))
    (hHgp : ∀ (n : ℕ) (P : A) [Projective P], IsZero ((Hgp.functor (n + 1)).obj P))
    (base : Hc.functor 0 ≅ Hgp.functor 0) (i : ℕ) :
    Hc.functor i ≅ Hgp.functor i

Stacks.EtaleCohomology.CurveFundamentalGroup.deltaFunctorIsoRightDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 231. The attribute's comment: “fourth assertion, by the source's own proof: a cohomological δ-functor whose positive degrees vanish on injectives IS the right derived functor of its degree-zero part, so H^i(X_k̄, F_ρ) = H^i(π₁(X_k̄, η̄), M). The étale δ-functor Het and its vanishing on injectives are hypotheses, since the étale input 0GIY is not available”.

[Stacks, Tag 03VM], fourth assertion. A cohomological δ-functor Het whose positive-degree parts vanish on injective objects, and whose degree-zero part is identified with the degree-zero right derived functor of an additive T, is the right derived functor of T.

In the source Het is i ↦ H^i(X_{k̄}, F_ρ) on the category of pairs (M, ρ) and T is (M, ρ) ↦ M^{π₁(X_{k̄}, η̄)}.

def deltaFunctorIsoRightDerived (Het : DeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    (hvanish : ∀ (n : ℕ) (I : A) [Injective I], IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ T.rightDerived 0) :
    Het ≅ Stacks.DerivedIndexing.rightDerivedDeltaFunctorOfEnoughInjectives T

Stacks.EtaleCohomology.CurveFundamentalGroup.isoRightDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 245. The attribute's comment: “fourth assertion read degreewise: H^i(X_k̄, F_ρ) ≅ R^i(M ↦ M^{π₁}), with the étale δ-functor and its vanishing on injectives as hypotheses”.

[Stacks, Tag 03VM], fourth assertion, degree by degree: Hetⁱ ≅ R ⁱT.

def isoRightDerived (Het : DeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    (hvanish : ∀ (n : ℕ) (I : A) [Injective I], IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ T.rightDerived 0) (i : ℕ) :
    Het.functor i ≅ T.rightDerived i

Stacks.EtaleCohomology.CurveFundamentalGroup.isoRightDerivedOfLeftExact, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 259. The attribute's comment: “fourth assertion with a left exact degree-zero part: from H^0(X_k̄, F_ρ) ≅ T with T left exact (invariants), H^i(X_k̄, F_ρ) ≅ R^i T for every i. The étale δ-functor and its vanishing on injectives are hypotheses”.

[Stacks, Tag 03VM], fourth assertion with the degree-zero hypothesis in its usable form. When T is left exact — as M ↦ M^{π₁(X_{k̄}, η̄)} is — the degree-zero input is an identification Het₀ ≅ T itself, because R ⁰T ≅ T.

def isoRightDerivedOfLeftExact (Het : DeltaFunctor A B) (T : A ⥤ B) [T.Additive]
    [PreservesFiniteLimits T]
    (hvanish : ∀ (n : ℕ) (I : A) [Injective I], IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ T) (i : ℕ) :
    Het.functor i ≅ T.rightDerived i

Stacks.EtaleCohomology.CurveFundamentalGroup.isoContinuousGroupCohomologyRightDerived, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 293. The attribute's comment: “fourth assertion with the group-cohomology side CONCRETE: for a cohomological δ-functor on discrete continuous G-modules vanishing on injectives in positive degree and agreeing with R^0 of invariants in degree zero, every degree agrees with the right derived functors of invariants, i.e. with the continuous group cohomology H^i(G, M) of 04JR. The étale δ-functor is still a hypothesis (0GIY is not available)”. References: SGA 3 I (5.2.1), “special case”.

[Stacks, Tag 03VM], fourth assertion with the group side concrete. A cohomological δ-functor on discrete continuous G-modules whose positive degrees vanish on injectives and whose degree-zero part is H⁰ of the invariants functor agrees, in every degree, with the higher right derived functors of invariants — the continuous group cohomology H^i(G, M) of [Stacks, Tag 04JR].

Taking G = π₁(X_{k̄}, η̄) and the δ-functor i ↦ H^i(X_{k̄}, F_ρ), this is the fourth assertion of [Stacks, Tag 03VM].

def isoContinuousGroupCohomologyRightDerived
    (Het : DeltaFunctor (ContinuousGModule.{u, max u v} G) AddCommGrpCat.{max u v})
    (hvanish : ∀ (n : ℕ) (I : ContinuousGModule.{u, max u v} G) [Injective I],
      IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ (continuousGModuleInvariants.{u, max u v} G).rightDerived 0)
    (i : ℕ) :
    Het.functor i ≅ (continuousGModuleInvariants.{u, max u v} G).rightDerived i

Stacks.EtaleCohomology.CurveFundamentalGroup.isoContinuousGroupCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 310. The attribute's comment: “fourth assertion with the right-hand side spelled as the continuous group cohomology functor of 04JR itself. The étale δ-functor and its vanishing on injectives are hypotheses”. References: SGA 3 I (5.2.1), “special case”.

[Stacks, Tag 03VM], fourth assertion against Stacks.continuousGroupCohomologyFunctor. The same identification, with the right-hand side spelled as the cohomology functor of [Stacks, Tag 04JR] (CategoryTheory.Functor.rightDerivedPlus of invariants) rather than as Mathlib's ℕ-indexed CategoryTheory.Functor.rightDerived; the two agree by Stacks.DerivedIndexing.rightDerivedIso.

def isoContinuousGroupCohomology
    (Het : DeltaFunctor (ContinuousGModule.{u, max u v} G) AddCommGrpCat.{max u v})
    (hvanish : ∀ (n : ℕ) (I : ContinuousGModule.{u, max u v} G) [Injective I],
      IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ (continuousGModuleInvariants.{u, max u v} G).rightDerived 0)
    (i : ℕ) :
    Het.functor i ≅ continuousGroupCohomologyFunctor.{u, v} G i

Stacks.EtaleCohomology.CurveFundamentalGroup.isoContinuousGroupCohomologyOfInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/CurveFundamentalGroupCohomology.lean, line 336. The attribute's comment: “fourth assertion with BOTH sides in the source's own form: from H^0(X_k̄, F_ρ) ≅ M^{π₁} (the invariants functor itself) the étale δ-functor agrees in every degree with the continuous group cohomology H^i(G, M) of 04JR. Left exactness of the invariants functor is an instance hypothesis — true, but Mathlib gives no PreservesFiniteLimits instance for a full-subcategory inclusion — and the étale δ-functor with its vanishing on injectives is a hypothesis (0GIY is not available)”.

[Stacks, Tag 03VM], fourth assertion with both sides in the source's own form. From the degree-zero identification H^0(X_{k̄}, F_ρ) ≅ M^{π₁(X_{k̄}, η̄)} — invariants themselves, not R ⁰ of invariants — the étale δ-functor agrees in every degree with the continuous group cohomology H^i(G, M) of [Stacks, Tag 04JR].

Left exactness of Stacks.continuousGModuleInvariants is an instance hypothesis: it is true (invariants are a right adjoint, and the two full-subcategory inclusions involved are exact), but CategoryTheory.ObjectProperty.ι carries no PreservesFiniteLimits instance in Mathlib, so there is nothing here to discharge it with. The variant without it is isoContinuousGroupCohomology, whose degree-zero input is phrased against R ⁰.

def isoContinuousGroupCohomologyOfInvariants
    [PreservesFiniteLimits (continuousGModuleInvariants.{u, max u v} G)]
    (Het : DeltaFunctor (ContinuousGModule.{u, max u v} G) AddCommGrpCat.{max u v})
    (hvanish : ∀ (n : ℕ) (I : ContinuousGModule.{u, max u v} G) [Injective I],
      IsZero ((Het.functor (n + 1)).obj I))
    (base : Het.functor 0 ≅ continuousGModuleInvariants.{u, max u v} G) (i : ℕ) :
    Het.functor i ≅ continuousGroupCohomologyFunctor.{u, v} G i

AlgebraicGeometry.geometricGaloisDerivedInvariantsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricDerivedGaloisInvariants.lean, line 957. The attribute's comment: “sixth assertion (the derived version of the cohomological half) with the Galois action: RH⁰(π₁(X_k̄, η̄), M) ≅ RΓ^{Gal}(X_k̄, ℱ_ρ) in the derived category of discrete Λ-modules with continuous Aut(k̄/k)-action, natural in (M, ρ)”.

The derived version of H^i(X_{k̄}, ℱ_ρ) = H^i(π₁(X_{k̄}), M) with its Galois action ([Stacks, Tag 03VM], "Moreover, in this case there is a derived version too"): for a geometrically connected smooth curve X over k, k̄ an algebraic closure of k, separable over k, Λ a finite ring with #Λ invertible in k, and X_{k̄} ≇ 𝐏¹_{k̄}, there is an isomorphism

RH⁰(π₁(X_{k̄}), M) ≅ RΓ^{Gal}(X_{k̄}, ℱ_ρ)

in the bounded below derived category of discrete Λ-modules with a continuous action of Aut(k̄/k), natural in the finite Λ-module M with continuous action ρ of π₁(X). Here RH⁰(π₁(X_{k̄}), -) is the right derived functor of the invariants under π₁(X_{k̄}) with their residual action of π₁(X)/π₁(X_{k̄}) = Aut(k̄/k) (Stacks.GroupCohomology.derivedKernelInvariants), and RΓ^{Gal}(X_{k̄}, -) that of global sections on X_{k̄} with their Galois action (Stacks.EtaleCohomology.galoisDerivedGlobalSections). The degree-zero identification is the canonical one of Tag 03VL.

def geometricGaloisDerivedInvariantsIso
    (y : GeometricPoint (Stacks.Frobenius.fieldBaseChange (Over.mk f) K))
    (hΛ : IsUnit ((Nat.card Λ : ℕ) : k))
    (hP : ¬ ∃ e : Stacks.Frobenius.fieldBaseChange (Over.mk f) K ≅
        projectiveSpaceOver 1 (Spec (.of K)),
      e.hom ≫ (projectiveSpaceOver 1 (Spec (.of K)) ↘ Spec (.of K)) =
        pullback.snd (Over.mk f).hom (Stacks.Frobenius.specAlgebraMap k K)) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f K
    haveI : IsAlgClosed K := IsAlgClosure.isAlgClosed k
    haveI : Algebra.IsAlgebraic k K := IsAlgClosure.isAlgebraic
    (finiteTypeContinuousModuleι.{0, u + 1, u + 1} Λ
        (EtaleFundamentalGroup X.1
        (y.map (fieldBaseChangeObjProj B X f K
        (contains_fieldBaseChange_of_isCurve B X f K)).hom))) ⋙
        DerivedCategory.Plus.singleFunctor _ 0 ⋙
        derivedKernelInvariants.{0, u + 1, u, 0} Λ (geometricGaloisProjection B X f K y)
          (surjective_geometricGaloisProjection B X f K y) ≅
      representationSheaf.{u, 0} B X
          (y.map (fieldBaseChangeObjProj B X f K (contains_fieldBaseChange_of_isCurve B X f K)).hom)
          Λ ⋙ DerivedCategory.Plus.singleFunctor _ 0 ⋙
        Stacks.EtaleCohomology.galoisDerivedGlobalSections Λ (Over.mk f) K

AlgebraicGeometry.geometricDerivedInvariantsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Trace/GeometricDerivedInvariants.lean, line 1074. The attribute's comment: “sixth assertion (the derived version of the cohomological half): RΓ(π₁(X_k̄, η̄), M) ≅ RΓ(X_k̄, ℱ_ρ), natural in (M, ρ)”.

The derived version of H^i(X_{k̄}, ℱ_ρ) = H^i(π₁(X_{k̄}), M) ([Stacks, Tag 03VM], "Moreover, in this case there is a derived version too"): for a geometrically connected smooth curve X over k, k̄ an algebraic closure of k, Λ a finite ring with #Λ invertible in k, and X_{k̄} ≇ 𝐏¹_{k̄}, there is an isomorphism

RΓ(π₁(X_{k̄}), M) ≅ RΓ(X_{k̄}, ℱ_ρ)

in the bounded below derived category of Λ-modules, natural in the finite Λ-module M with continuous action ρ of π₁(X). Here RΓ(π₁(X_{k̄}), -) is the right derived functor of the invariants on all continuous discrete π₁(X_{k̄})-modules, and RΓ(X_{k̄}, -) that of global sections on (X_{k̄})_{étale}. The source's hypotheses and nothing else.

def geometricDerivedInvariantsIso
    (y : GeometricPoint (Stacks.Frobenius.fieldBaseChange (Over.mk f) K))
    (hΛ : IsUnit ((Nat.card Λ : ℕ) : k))
    (hP : ¬ ∃ e : Stacks.Frobenius.fieldBaseChange (Over.mk f) K ≅
        projectiveSpaceOver 1 (Spec (.of K)),
      e.hom ≫ (projectiveSpaceOver 1 (Spec (.of K)) ↘ Spec (.of K)) =
        pullback.snd (Over.mk f).hom (Stacks.Frobenius.specAlgebraMap k K)) :
    letI := connectedSpace_of_isCurve B X f
    letI := connectedSpace_fieldBaseChange f K
    finiteTypeContinuousModuleToRes Λ
        (geometricFundamentalGroupMap B X f K (contains_fieldBaseChange_of_isCurve B X f K) y) ⋙
        DerivedCategory.Plus.singleFunctor _ 0 ⋙
        (continuousModuleRingInvariants.{0, u + 1, u + 1} Λ
          (EtaleFundamentalGroup (Stacks.Frobenius.fieldBaseChange (Over.mk f) K)
            y)).rightDerivedFunctorPlus ≅
      geometricRepresentationSheaf.{u, 0} B X
          (y.map (fieldBaseChangeObjProj B X f K (contains_fieldBaseChange_of_isCurve B X f K)).hom)
          Λ f K ⋙
        DerivedCategory.Plus.singleFunctor _ 0 ⋙
        (Stacks.EtaleCohomology.etaleModuleGlobalSections.{u, 0} Λ
          (Stacks.Frobenius.fieldBaseChange (Over.mk f) K)).rightDerivedFunctorPlus

Declarations registered for the tag:

Sources
LeanAlgebraicGeometry.compactSupportCanonicalTwistEquiv_galois · Stacks.EtaleCohomology.compactlySupportedCohomologyTwo_galoisIso_tateTwistCoinvariants · AlgebraicGeometry.isZero_curveCompactlySupportedCohomologyZero_of_not_isProjective · AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv · AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv_naturality · AlgebraicGeometry.geometricGlobalSectionsInvariantsEquiv_galois · Stacks.EtaleCohomology.LAdicSheaf.subsingleton_rationalGeometricCompactlySupportedCohomology_zero_of_not_isProper · Stacks.EtaleCohomology.compactlySupportedSections_eq_bot_of_not_isProper

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.