59.56 Galois action on stalks to 59.69 Picard groups of curves

Section59.56 Galois action on stalks#

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

Tag 03QW, the section

Tag 03QW in the Stacks Project.

Declarations registered for the tag:

Tag 04JK, an equation

Tag 04JK in the Stacks Project.

AlgebraicGeometry.geometricPointStalkMap_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GeometricPointStalkMap.lean, line 548. The attribute's comment: “the displayed rule: the germ of (U, u, t) goes to that of (U, u ∘ Spec σ, t)”.

The canonical map takes the germ of (U, u', σ) to the germ of (U, u' ∘ a, σ).

public theorem geometricPointStalkMap_germ
    (F : (SmallEtale B S hS)ᵒᵖ ⥤ Type u)
    (U : (geometricPointFiber B S hS t).Elementsᵒᵖ)
    (σ : F.obj (Opposite.op U.unop.1)) :
    (geometricPointStalkMap B S hS a (Type u)).app F
        ((colimit.ι
          ((CategoryOfElements.π (geometricPointFiber B S hS t)).op ⋙ F) U) σ) =
      (colimit.ι
        ((CategoryOfElements.π (geometricPointFiber B S hS s)).op ⋙ F)
        ((neighborhoodFunctor B S hS a).op.obj U)) σ
Tag 03QX, a definition

Tag 03QX in the Stacks Project.

AlgebraicGeometry.GeometricPoint.separableClosure, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/Basic.lean, line 66. The attribute's comment: “the separable algebraic closure”.

The separable algebraic closure of the residue field at the image of a geometric point inside its algebraically closed defining field.

noncomputable abbrev separableClosure {S : AlgebraicGeometry.Scheme.{u}}
    (sbar : GeometricPoint S)

AlgebraicGeometry.GeometricPoint.absoluteGaloisGroup, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/Basic.lean, line 80. The attribute's comment: “part (1): the absolute Galois group”. References: SGA 3 VIIB (3.3.3), “more general”; SGA 4 VIII (2.1), “more general”; SGA 4½ Arcata (2.4.2), “more general”; SGA 7 I (0.3); SGA 7 XIII (0.2), “(0.2.5)”; SGA 7 XVI (1.6).

The absolute Galois group at a geometric point is the automorphism group of the separable closure of the residue field at its image.

noncomputable abbrev absoluteGaloisGroup {S : AlgebraicGeometry.Scheme.{u}}
    (sbar : GeometricPoint S)

AlgebraicGeometry.GeometricPoint.IsAlgebraic, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/Basic.lean, line 88. The attribute's comment: “part (2): algebraic geometric points”.

A geometric point is algebraic when its algebraically closed defining field is algebraic over the residue field at its image, and hence is an algebraic closure of that residue field.

noncomputable abbrev IsAlgebraic {S : AlgebraicGeometry.Scheme.{u}}
    (sbar : GeometricPoint S) : Prop
Tag 03QT, a theorem

Tag 03QT in the Stacks Project.

AlgebraicGeometry.etaleSheafStalkEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkEquivalence/SheafStalk.lean, line 842. References: SGA 4 VIII (2.1), “j is an equivalence”; SGA 7 XIII (1.2.2), “(a)”; SGA 7 XIII (1.1.3), “Y = Spec k”.

Stacks 03QT. For a geometric point of the spectrum of a field, taking stalks is an equivalence from the small étale topos to the category of continuous sets over the absolute Galois group, naturally identified with the stalk functor, and the Galois action on a germ changes the geometric lift of the étale neighborhood by precomposition.

def etaleSheafStalkEquivalence :
    Σ e : smallEtaleTopos.{u, max u v} B (Spec (.of K)) hK ≌
        AlgebraicGeometry.ContinuousGSet.{u, max u v}
          (GeometricPoint.absoluteGaloisGroup sbar),
      { α : e.functor ⋙ AlgebraicGeometry.ContinuousGSet.forget
            (GeometricPoint.absoluteGaloisGroup sbar) ≅
          etaleStalkFunctor.{u, v} B (Spec (.of K)) hK sbar //
        ∀ (F : smallEtaleTopos.{u, max u v} B (Spec (.of K)) hK)
          (σ : GeometricPoint.absoluteGaloisGroup sbar),
          letI := GeometricPoint.residueFieldAlgebra sbar
          ∀ (τ : Gal(sbar.residueField /
              (Spec (.of K)).residueField (sbar.hom default)))
            (_hτ : ∀ a : GeometricPoint.separableClosure sbar,
              (σ a : sbar.residueField) = τ (a : sbar.residueField))
            (U : (geometricPointFiber B (Spec (.of K)) hK sbar).Elements)
            (q : (geometricPointFiber B (Spec (.of K)) hK sbar).obj U.1)
            (_hq : q.1 = Spec.map (CommRingCat.ofHom τ.toRingHom) ≫ U.2.1)
            (t : ((sheafToPresheaf _ _).obj F).obj (op U.1)),
            let V : (geometricPointFiber B (Spec (.of K)) hK sbar).Elements := Functor.elementsMk _ U.1 q
            ConcreteCategory.hom (α.app F).hom
                (ConcreteCategory.hom ((e.functor.obj F).obj.obj.ρ σ).asHom
                  (ConcreteCategory.hom (α.app F).inv
                    (etaleStalkGerm.{u, v} B (Spec (.of K)) hK sbar F U t))) =
              etaleStalkGerm.{u, v} B (Spec (.of K)) hK sbar F V t }
Tag 04JM, a lemma

Tag 04JM in the Stacks Project.

AlgebraicGeometry.bijective_etaleGlobalSectionGerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/GlobalSections.lean, line 104.

For a geometric point of the spectrum of a field, taking the germ at that point is a bijection from the global sections of a sheaf of sets on the small étale site onto the elements of its stalk fixed by the absolute Galois group.

theorem bijective_etaleGlobalSectionGerm
    (F : smallEtaleTopos.{u, max u v} B (Spec (.of K)) hK) :
    Function.Bijective
      (fun t : ((sheafToPresheaf _ _).obj F).obj
          (op (SmallEtale.final B (Spec (.of K)) hK)) ↦
        (⟨etaleGlobalSectionGerm.{u, v} B K hK sbar F t,
            fun σ ↦ etaleStalkSmul_etaleGlobalSectionGerm.{u, v} B K hK sbar F σ t⟩ :
          etaleStalkGaloisFixedPoints.{u, v} B K hK sbar F))

AlgebraicGeometry.etaleGlobalSectionsEquivGaloisFixedPoints, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/GlobalSections.lean, line 123. The attribute's comment: “the functorial bijection”.

The bijection between the global sections of a sheaf of sets on the small étale site of the spectrum of a field and the Galois-fixed elements of its stalk at a geometric point.

def etaleGlobalSectionsEquivGaloisFixedPoints
    (F : smallEtaleTopos.{u, max u v} B (Spec (.of K)) hK) :
    ((sheafToPresheaf _ _).obj F).obj (op (SmallEtale.final B (Spec (.of K)) hK)) ≃
      etaleStalkGaloisFixedPoints.{u, v} B K hK sbar F

AlgebraicGeometry.etaleGlobalSectionGerm_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/GlobalSections.lean, line 142. The attribute's comment: “functoriality in the sheaf”.

The bijection between global sections and Galois-fixed stalk elements is functorial: a morphism of sheaves carries the germ of a global section to the germ of its image.

theorem etaleGlobalSectionGerm_map
    {F F' : smallEtaleTopos.{u, max u v} B (Spec (.of K)) hK} (φ : F ⟶ F')
    (t : ((sheafToPresheaf _ _).obj F).obj (op (SmallEtale.final B (Spec (.of K)) hK))) :
    etaleGlobalSectionGerm.{u, v} B K hK sbar F'
        (ConcreteCategory.hom (((sheafToPresheaf _ _).map φ).app
          (op (SmallEtale.final B (Spec (.of K)) hK))) t) =
      ConcreteCategory.hom ((etaleStalkFunctor.{u, v} B (Spec (.of K)) hK sbar).map φ)
        (etaleGlobalSectionGerm.{u, v} B K hK sbar F t)
Tag 04JN, a remark

Tag 04JN in the Stacks Project.

AlgebraicGeometry.GeometricPoint.subsingleton_absoluteGaloisGroup_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/AlgebraicallyClosed.lean, line 167. The attribute's comment: “trivial absolute Galois group”.

Stacks Project, Tag 04JN. An algebraically closed field has trivial absolute Galois group at every geometric point of its spectrum.

theorem subsingleton_absoluteGaloisGroup_of_isAlgClosed :
    Subsingleton (absoluteGaloisGroup s)

AlgebraicGeometry.globalSections_isEquivalence_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/AlgebraicallyClosed.lean, line 263. The attribute's comment: “equivalence by global sections”.

Stacks Project, Tag 04JN. Over an algebraically closed field, taking global sections is an equivalence from the small étale topos to the category of sets.

theorem globalSections_isEquivalence_of_isAlgClosed :
    (Sheaf.Γ (SmallEtale.topology B (Spec (.of K)) hK) (Type (u + 1))).IsEquivalence

AlgebraicGeometry.etaleStalkIsoPullbackGlobalSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/AlgebraicallyClosed.lean, line 338. The attribute's comment: “the stalk as global sections of the pullback”.

Stacks Project, Tag 04JN. The alternative description of the stalk functor at a geometric point sbar of S: it is the functor sending a sheaf to the global sections of its pullback along sbar.

def etaleStalkIsoPullbackGlobalSections (s : GeometricPoint S)
    (hK : B.Contains (Spec (.of s.residueField))) :
    letI : (smallEtaleBaseChange B (⟨s.hom⟩ :
        (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme))).IsContinuous
        (SmallEtale.topology B S hS)
        (SmallEtale.topology B (Spec (.of s.residueField)) hK) :=
      smallEtaleBaseChange_isContinuous B
        (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme))
    (smallEtaleBaseChange B (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶
            (⟨S, hS⟩ : B.Scheme))).sheafPullback (Type (u + 1)) (SmallEtale.topology B S hS)
          (SmallEtale.topology B (Spec (.of s.residueField)) hK) ⋙
        Sheaf.Γ (SmallEtale.topology B (Spec (.of s.residueField)) hK) (Type (u + 1)) ≅
      etaleStalkFunctor.{u, u + 1} B S hS s

AlgebraicGeometry.etaleStalkIsoPullbackGlobalSections_inv_app_etaleStalkGerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisActionStalks/AlgebraicallyClosed.lean, line 378. The attribute's comment: “the comparison on germs”.

Stacks Project, Tag 04JN. The alternative description of the stalk functor is the canonical comparison: it carries the germ at sbar of a section over a pointed étale neighbourhood to the section of the pullback obtained by restricting along the corresponding morphism from the final étale object over sbar.

theorem etaleStalkIsoPullbackGlobalSections_inv_app_etaleStalkGerm (s : GeometricPoint S)
    (hK : B.Contains (Spec (.of s.residueField)))
    (F : Sheaf (SmallEtale.topology B S hS) (Type (u + 1)))
    (V : (geometricPointFiber B S hS s).Elements)
    (a : SmallEtale.final B (Spec (.of s.residueField)) hK ⟶
      (smallEtaleBaseChange B (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶
        (⟨S, hS⟩ : B.Scheme))).obj V.1)
    (ha : (SmallEtale.toScheme B (Spec (.of s.residueField)) hK).map a ≫
      B.inclusion.map (pullback.fst V.1.obj.hom
        (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶
          (⟨S, hS⟩ : B.Scheme))) = V.2.1)
    (t : F.obj.obj (op V.1)) :
    letI : (smallEtaleBaseChange B (⟨s.hom⟩ :
        (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme))).IsContinuous
        (SmallEtale.topology B S hS)
        (SmallEtale.topology B (Spec (.of s.residueField)) hK) :=
      smallEtaleBaseChange_isContinuous B
        (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶ (⟨S, hS⟩ : B.Scheme))
    (Sheaf.ΓNatIsoSheafSections (SmallEtale.topology B (Spec (.of s.residueField)) hK)
          (Type (u + 1))
          (SmallEtale.finalIsTerminal B (Spec (.of s.residueField)) hK)).hom.app
        (((smallEtaleBaseChange B (⟨s.hom⟩ :
            (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶
              (⟨S, hS⟩ : B.Scheme))).sheafPullback (Type (u + 1))
              (SmallEtale.topology B S hS)
              (SmallEtale.topology B (Spec (.of s.residueField)) hK)).obj F)
        ((etaleStalkIsoPullbackGlobalSections B S hS s hK).inv.app F
          (etaleStalkGerm.{u, u + 1} B S hS s F V t)) =
      pullbackSectionAlong B (⟨s.hom⟩ : (⟨Spec (.of s.residueField), hK⟩ : B.Scheme) ⟶
          (⟨S, hS⟩ : B.Scheme)) F V.1
        (SmallEtale.final B (Spec (.of s.residueField)) hK) a t
Sources
LeanAlgebraicGeometry.etaleStalkSmul · AlgebraicGeometry.etaleStalkSmul_germ · AlgebraicGeometry.etaleStalkSmul_one · AlgebraicGeometry.etaleStalkSmul_mul · AlgebraicGeometry.etaleStalkMulAction · AlgebraicGeometry.etaleStalkSmul_naturality · AlgebraicGeometry.continuousSMul_etaleStalk · AlgebraicGeometry.etaleStalkContinuousGSet

Section59.57 Group cohomology#

Section 59.57 of the Stacks Project, Tag 0A2H. 6 tags here are carried by 11 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04JP, a definition

Tag 04JP in the Stacks Project.

Stacks.GroupCohomology.ofRepresentation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/DiscreteModules.lean, line 100. The attribute's comment: “R-G-modules”.

Stacks Project, Tag 04JP. An R-G-module: an R-module M together with a left action of G on M by R-linear maps which is continuous when M is given the discrete topology.

def ofRepresentation (ρ : Representation R G M)
    (h : (actionOfRepresentation R G M ρ).IsContinuous) :
    Stacks.Injectives.ContinuousModule.{u, v, w} R G

Stacks.GroupCohomology.homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/DiscreteModules.lean, line 132. The attribute's comment: “morphisms of R-G-modules”.

Stacks Project, Tag 04JP. A morphism of R-G-modules is a G-equivariant R-module map.

def homEquiv (X Y : Stacks.Injectives.ContinuousModule.{u, v, w} R G) :
    (X ⟶ Y) ≃ {f : X.obj.obj.V →ₗ[R] Y.obj.obj.V // ∀ (g : G) (x : X.obj.obj.V),
      f ((X.obj.obj.ρ g).asHom.hom x) = (Y.obj.obj.ρ g).asHom.hom (f x)}

Stacks.GroupCohomology.ofDistribMulAction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/DiscreteModules.lean, line 181. The attribute's comment: “G-modules”.

Stacks Project, Tag 04JP. A G-module, or discrete G-module: an abelian group M together with a left action of G on M by group homomorphisms which is continuous when M is given the discrete topology.

def ofDistribMulAction (h : (actionOfDistribMulAction G M).IsContinuous) :
    Stacks.Injectives.ContinuousModule.{0, v, w} ℤ G

Stacks.GroupCohomology.gModuleHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/DiscreteModules.lean, line 194. The attribute's comment: “morphisms of G-modules”.

Stacks Project, Tag 04JP. A morphism of G-modules is a G-equivariant homomorphism of abelian groups.

def gModuleHomEquiv (X Y : Stacks.Injectives.ContinuousModule.{0, v, w} ℤ G) :
    (X ⟶ Y) ≃ {f : X.obj.obj.V →+ Y.obj.obj.V // ∀ (g : G) (x : X.obj.obj.V),
      f ((X.obj.obj.ρ g).asHom.hom x) = (Y.obj.obj.ρ g).asHom.hom (f x)}

Declarations registered for the tag:

Tag 04JR, a definition

Tag 04JR in the Stacks Project.

continuousGroupCohomologyFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/Continuous.lean, line 205. The attribute's comment: “the cohomology functors”.

The i-th continuous group cohomology functor, namely the i-th right derived functor of taking invariants.

abbrev continuousGroupCohomologyFunctor [IsTopologicalGroup G]
    (i : ℕ) : ContinuousGModule.{u, max u v} G ⥤ AddCommGrpCat.{max u v}

continuousGroupCohomology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/Continuous.lean, line 213. The attribute's comment: “the cohomology groups”.

The continuous group cohomology group Hⁱ(G, M). For discrete groups this is group cohomology, and for Galois groups it is Galois cohomology. When G = Gal(Kˢᵉᵖ/K), it is also denoted Hⁱ(K, M).

abbrev continuousGroupCohomology [IsTopologicalGroup G]
    (i : ℕ) (M : ContinuousGModule.{u, max u v} G) : AddCommGrpCat.{max u v}
Tag 0DVD, a lemma

Tag 0DVD in the Stacks Project.

Stacks.ContinuousCohomology.continuousModuleCohomologyForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ContinuousCohomology/ForgetCoefficients.lean, line 688.

Continuous group cohomology of continuous discrete R-G-modules commutes, naturally in the module, with forgetting the R-module structure.

def continuousModuleCohomologyForgetIso [IsTopologicalGroup G]
    [HasDerivedCategory.{d} (Stacks.Injectives.ContinuousModule.{u, v, max u v w} R G)]
    [HasDerivedCategory.{d} (ModuleCat.{max u v w} R)] (i : ℕ) :
    cohomologyFunctor.{d, u, v, w} R G i ⋙
        forget₂ (ModuleCat.{max u v w} R) AddCommGrpCat.{max u v w} ≅
      continuousModuleForget.{u, v, max u v w} R G ⋙
        continuousGroupCohomologyFunctor.{v, max u v w} G i
Tag 0DVE, a lemma

Tag 0DVE in the Stacks Project.

Stacks.ContinuousCohomology.extIsoCohomologyDualTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ContinuousCohomology/ExtComparison.lean, line 425. The attribute's comment: “R-linear, in every degree; the Ext-universe smallness (hasExt_continuousModule) and themodel of the derived category are free instance arguments”.

Let G be a topological group, R a commutative ring and M, N continuous discrete R-G-modules. If M is finite projective as an R-module, then Extⁱ(M, N), computed in the category of continuous discrete R-G-modules, is the continuous group cohomology Hⁱ(G, Mᵛ ⊗_R N) of the diagonal action on Mᵛ ⊗_R N, R-linearly and in every degree.

def extIsoCohomologyDualTensor
    [HasDerivedCategory.{d} (Stacks.Injectives.ContinuousModule.{u, v, max u v w} R G)]
    [HasDerivedCategory.{d} (ModuleCat.{max u v w} R)]
    (N : Stacks.Injectives.ContinuousModule.{u, v, max u v w} R G) (i : ℕ) :
    Ext.{max u v w} M N i ≃ₗ[R]
      (cohomologyFunctor.{d, u, v, w} R G i).obj
        (dualTensorContinuousModule.{u, v, max u v w} R G M N)
Tag 0DVF, a lemma

Tag 0DVF in the Stacks Project.

Stacks.ContinuousCohomology.finite_cohomologyFunctor_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ContinuousCohomology/FiniteDimensionalDegreeOne.lean, line 496.

Let G be a topological group, k a field and V a k-G-module, that is a k-module with a continuous action of G for the discrete topology on V. If G is topologically finitely generated, so that some finite subset generates a dense subgroup, and V is finite dimensional over k, then the first continuous cohomology group H¹(G, V) is finite dimensional over k.

theorem finite_cohomologyFunctor_one
    (hG : ∃ S : Finset G, Dense ((Subgroup.closure (S : Set G) : Subgroup G) : Set G))
    (V : Stacks.Injectives.ContinuousModule.{u, v, max u v w} k G)
    [Module.Finite k V.obj.obj.V] :
    Module.Finite k ((cohomologyFunctor.{d, u, v, w} k G 1).obj V)
Tag 0DV3, a lemma

Tag 0DV3 in the Stacks Project.

continuousGroupCohomology_isTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/Profinite.lean, line 449. The attribute's comment: “part (1)”.

Positive-degree continuous cohomology of a profinite group with discrete coefficients is a torsion abelian group.

public theorem continuousGroupCohomology_isTorsion
    (hG : Stacks.Chapter05.Tag_0BR1.IsProfiniteTop G) (i : ℕ) (hi : 0 < i)
    (M : ContinuousGModule.{u, max u v} G) :
    Module.IsTorsion ℤ (continuousGroupCohomology G i M)

isZero_continuousGroupCohomology_of_module_rat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GroupCohomology/Profinite.lean, line 458. The attribute's comment: “part (2)”.

Positive-degree continuous cohomology of a profinite group vanishes when the discrete coefficient module is a rational vector space.

public theorem isZero_continuousGroupCohomology_of_module_rat
    (hG : Stacks.Chapter05.Tag_0BR1.IsProfiniteTop G) (i : ℕ) (hi : 0 < i)
    (M : ContinuousGModule.{u, max u v} G) [Module ℚ M.1.1.V] :
    IsZero (continuousGroupCohomology G i M)
Sources
LeanStacks.GroupCohomology.ofRepresentation · Stacks.GroupCohomology.homEquiv · Stacks.GroupCohomology.ofDistribMulAction · Stacks.GroupCohomology.gModuleHomEquiv · Stacks.Injectives.ContinuousModule · continuousGroupCohomologyFunctor · continuousGroupCohomology · Stacks.ContinuousCohomology.continuousModuleCohomologyForgetIso

Section59.59 Cohomology of a point#

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

Tag 04JQ, a lemma

Tag 04JQ in the Stacks Project.

AlgebraicGeometry.abelianEtaleSheafStalkEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkEquivalence/AbelianSheafStalk.lean, line 736. References: SGA 4 VIII (2.2).

For a geometric point of the spectrum of a field, taking stalks is an equivalence from abelian sheaves on the small étale site to discrete modules over the absolute Galois group at that point, naturally identified with the abelian-group-valued stalk functor, and the Galois action on a germ changes the geometric lift of the étale neighbourhood by precomposition.

def abelianEtaleSheafStalkEquivalence :
    Σ e : Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v} ≌
        ContinuousGAddCommGrp.{u, max u v} (GeometricPoint.absoluteGaloisGroup sbar),
      { α : e.functor ⋙
            ContinuousGAddCommGrp.forget (GeometricPoint.absoluteGaloisGroup sbar) ≅
          abelianEtaleStalkFunctor.{u, v} B (Spec (.of K)) hK sbar //
        ∀ (F : Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v})
          (σ : GeometricPoint.absoluteGaloisGroup sbar),
          letI := GeometricPoint.residueFieldAlgebra sbar
          ∀ (τ : Gal(sbar.residueField /
              (Spec (.of K)).residueField (sbar.hom default)))
            (_hτ : ∀ a : GeometricPoint.separableClosure sbar,
              (σ a : sbar.residueField) = τ (a : sbar.residueField))
            (U : (geometricPointFiber B (Spec (.of K)) hK sbar).Elements)
            (q : (geometricPointFiber B (Spec (.of K)) hK sbar).obj U.1)
            (_hq : q.1 = Spec.map (CommRingCat.ofHom τ.toRingHom) ≫ U.2.1)
            (t : ((sheafToPresheaf _ _).obj F).obj (op U.1)),
            let V : (geometricPointFiber B (Spec (.of K)) hK sbar).Elements := ⟨q⟩
            ConcreteCategory.hom (α.app F).hom
                (ConcreteCategory.hom ((e.functor.obj F).obj.obj.ρ σ).asHom
                  (ConcreteCategory.hom (α.app F).inv
                    (abelianEtaleStalkGerm.{u, v} B (Spec (.of K)) hK sbar F U t))) =
              abelianEtaleStalkGerm.{u, v} B (Spec (.of K)) hK sbar F V t }

Declarations registered for the tag:

Tag 03QU, a lemma

Tag 03QU in the Stacks Project.

AlgebraicGeometry.etaleH0AddEquivGaloisInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/GaloisInvariants.lean, line 232. The attribute's comment: “part (2)”.

Let K be a field, let sbar be a geometric point of Spec K with absolute Galois group G, and let F be an abelian sheaf on the small étale site of Spec K corresponding to the G-module M. Then the degree-zero étale cohomology of Spec K with coefficients in F is the group M ^ G of Galois invariants.

def etaleH0AddEquivGaloisInvariants
    [HasSheafify (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v})] :
    Sheaf.H.{w, max u v} F 0 ≃+ ↥(etaleStalkGaloisInvariants.{u, v} B K hK sbar F)

AlgebraicGeometry.etaleH0AddEquivGaloisInvariants_coe, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/GaloisInvariants.lean, line 243. The attribute's comment: “part (2), the comparison is taking germs at the geometric point”.

The identification of degree-zero étale cohomology with the Galois invariants is taking germs at the geometric point: a cohomology class is sent to the germ of the global section which represents it.

theorem etaleH0AddEquivGaloisInvariants_coe
    [HasSheafify (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v})]
    (x : Sheaf.H.{w, max u v} F 0) :
    (etaleH0AddEquivGaloisInvariants B K hK sbar F x).1 =
      etaleGlobalSectionGerm.{u, v} B K hK sbar (abelianEtaleSheafOfSets.{u, v} B K hK F)
        (Sheaf.H.equiv₀ F (SmallEtale.finalIsTerminal B (Spec (.of K)) hK) x)

AlgebraicGeometry.etaleH0AddEquivGaloisInvariants_abelianEtaleStalkGerm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/GaloisInvariants.lean, line 256. The attribute's comment: “part (2), the comparison in the abelian stalk”.

Read in the abelian-group-valued stalk, the identification of degree-zero étale cohomology with the Galois invariants sends a cohomology class to the germ, at the final pointed étale neighbourhood, of the global section which represents it.

theorem etaleH0AddEquivGaloisInvariants_abelianEtaleStalkGerm
    [HasSheafify (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v})]
    (x : Sheaf.H.{w, max u v} F 0) :
    etaleGaloisModuleAddEquivStalk.{u, v} B K hK sbar F
        (etaleH0AddEquivGaloisInvariants B K hK sbar F x).1 =
      abelianEtaleStalkGerm.{u, v} B (Spec (.of K)) hK sbar F
        (finalPointedNeighborhood B K hK sbar)
        (Sheaf.H.equiv₀ F (SmallEtale.finalIsTerminal B (Spec (.of K)) hK) x)

AlgebraicGeometry.additiveSheafHAddEquivContinuousGroupCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/AdditiveGroupGaloisModule.lean, line 269. The attribute's comment: “part (3) at 𝐆_a, in every degree: the degree-q étale cohomology of the spectrum of a field with coefficients in the additive group is the degree-q continuous group cohomology of the absolute Galois group with coefficients in the separable closure under addition. This is the general objectwise form of part (3) on Mathlib's small étale site, smallEtaleSheafCohomologyAddEquivContinuousGroupCohomology, with its Galois module computed at 𝐆_a by additiveContinuousGModuleIso -- the stalk computation additiveStalkIsoSepClosure packaged with its germwise Galois equivariance additiveSectionEval_galoisFiberAction into an isomorphism of discrete Galois modules. Nothing is assumed of the field and nothing is carried. NOT proved here: parts (1) and (2) of the tag, which are separate registrations”.

Stacks Project, Tag 03QU, part (3), at 𝐆_a. For a field K, a geometric point sbar of Spec K and every degree q,

H^q_étale(Spec K, 𝐆_a) ≅ H^q(Gal(Kˢᵉᵖ/κ), Kˢᵉᵖ),

κ being the residue field at the image of sbar and Kˢᵉᵖ the Galois module with addition as group law. This is the general comparison AlgebraicGeometry.smallEtaleSheafCohomologyAddEquivContinuousGroupCohomology with its Galois module identified at 𝐆_a by AlgebraicGeometry.additiveContinuousGModuleIso.

def additiveSheafHAddEquivContinuousGroupCohomology (q : ℕ) :
    Sheaf.H.{u + 1, u + 1}
        (Stacks.ArtinSchreier.additiveSheaf.{u, u + 1} (Spec (.of K))) q ≃+
      continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) q
        (sepClosureAddGModule K sbar)

AlgebraicGeometry.etaleRightDerivedGammaIsoContinuousGroupCohomologyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 134. The attribute's comment: “part (3), as an isomorphism of functors, with étale cohomology as the right derived functor of global sections”.

In every degree q, the q-th right derived functor of the global sections functor CategoryTheory.Sheaf.Γ of the small étale site of Spec K is the stalk equivalence AlgebraicGeometry.etaleContinuousGModuleEquivalence followed by the q-th continuous group cohomology functor of the absolute Galois group.

def etaleRightDerivedGammaIsoContinuousGroupCohomologyFunctor (q : ℕ) :
    (Sheaf.Γ (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{u + 1}).rightDerived q ≅
      (etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor ⋙
        continuousGroupCohomologyFunctor.{u, u + 1}
          (GeometricPoint.absoluteGaloisGroup sbar) q

AlgebraicGeometry.etaleSheafCohomologyIsoContinuousGroupCohomologyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 158. The attribute's comment: “part (3), in every degree, as a natural isomorphism of functors: sheaf cohomology on the small étale site of the spectrum of a field is the stalk equivalence of 04JQ followed by the continuous group cohomology functor of 04JR”.

Let K be a field, let sbar be a geometric point of Spec K and let G be the absolute Galois group at sbar. For every q, Mathlib's degree-q sheaf cohomology functor CategoryTheory.Sheaf.functorH on the small étale site of Spec K is the stalk equivalence AlgebraicGeometry.etaleContinuousGModuleEquivalence followed by the degree-q continuous group cohomology functor of G.

def etaleSheafCohomologyIsoContinuousGroupCohomologyFunctor (q : ℕ) :
    Sheaf.functorH.{u + 1, u + 1, u, u + 1}
        (SmallEtale.topology B (Spec (.of K)) hK) q ≅
      (etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor ⋙
        continuousGroupCohomologyFunctor.{u, u + 1}
          (GeometricPoint.absoluteGaloisGroup sbar) q

AlgebraicGeometry.etaleSheafCohomologyAddEquivContinuousGroupCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 175. The attribute's comment: “part (3): in every degree q, the degree-q étale cohomology of the spectrum of a field with coefficients in an abelian sheaf is the degree-q continuous group cohomology of the absolute Galois group with coefficients in the sheaf's module of 04JQ”.

Let K be a field, let sbar be a geometric point of Spec K with absolute Galois group G, and let F be an abelian sheaf on the small étale site of Spec K, corresponding to the G-module M under AlgebraicGeometry.etaleContinuousGModuleEquivalence. Then for every q

H^q_étale(Spec K, F) = H^q(G, M).

def etaleSheafCohomologyAddEquivContinuousGroupCohomology
    (F : Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{u + 1}) (q : ℕ) :
    Sheaf.H.{u + 1, u + 1} F q ≃+
      continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) q
        ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj F)

AlgebraicGeometry.etaleDerivedGlobalSectionsIsoDerivedGaloisInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 211. The attribute's comment: “part (1)”.

Let K be a field, let sbar be a geometric point of Spec K with absolute Galois group G, let F be an abelian sheaf on the small étale site of Spec K and let M be the discrete G-module it corresponds to under AlgebraicGeometry.etaleContinuousGModuleEquivalence. Then in the derived category of abelian groups there is a canonical isomorphism

RΓ(Spec K, F) ≅ RΓ_G(M)

between the derived global sections of F and the derived G-invariants of M, both computed on bounded below derived categories and mapped to the unbounded one by DerivedCategory.Plus.ι.

def etaleDerivedGlobalSectionsIsoDerivedGaloisInvariants
    (F : Sheaf (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{u + 1}) :
    DerivedCategory.Plus.ι.obj
        ((Sheaf.Γ (SmallEtale.topology B (Spec (.of K)) hK)
          AddCommGrpCat.{u + 1}).rightDerivedFunctorPlus.obj
            ((DerivedCategory.Plus.singleFunctor _ 0).obj F)) ≅
      DerivedCategory.Plus.ι.obj
        ((continuousGModuleInvariants.{u, u + 1}
          (GeometricPoint.absoluteGaloisGroup sbar)).rightDerivedFunctorPlus.obj
            ((DerivedCategory.Plus.singleFunctor _ 0).obj
              ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj F)))

AlgebraicGeometry.smallEtaleSheafCohomologyIsoContinuousGroupCohomologyFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 274. The attribute's comment: “part (3), in every degree, on Mathlib's small étale site of the spectrum of a field: sheaf cohomology there is restriction to the site of 021B followed by the stalk equivalence of 04JQ and the continuous group cohomology functor of 04JR”.

For every q, Mathlib's degree-q sheaf cohomology functor on its small étale site of Spec K is the restriction AlgebraicGeometry.smallEtaleSheafRestriction to the site AlgebraicGeometry.SmallEtale.topology, followed by the stalk equivalence AlgebraicGeometry.etaleContinuousGModuleEquivalence and the degree-q continuous group cohomology functor of the absolute Galois group.

def smallEtaleSheafCohomologyIsoContinuousGroupCohomologyFunctor (q : ℕ) :
    Sheaf.functorH.{u + 1, u + 1, u, u + 1}
        ((Spec (.of K) : Scheme.{u})).smallEtaleTopology q ≅
      smallEtaleSheafRestriction B K hK ⋙
        ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor ⋙
          continuousGroupCohomologyFunctor.{u, u + 1}
            (GeometricPoint.absoluteGaloisGroup sbar) q)

AlgebraicGeometry.smallEtaleSheafCohomologyAddEquivContinuousGroupCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleGaloisCohomologyComparison.lean, line 298. The attribute's comment: “part (3) on Mathlib's small étale site, objectwise: the degree-q étale cohomology group of the spectrum of a field with coefficients in an abelian sheaf is the degree-q continuous group cohomology of the absolute Galois group with coefficients in the sheaf's Galois module”.

For every abelian sheaf F on Mathlib's small étale site of Spec K and every degree q,

H^q_étale(Spec K, F) = H^q(G, M),

M being the Galois module of the restriction of F to the site AlgebraicGeometry.SmallEtale.topology.

def smallEtaleSheafCohomologyAddEquivContinuousGroupCohomology
    (F : Sheaf ((Spec (.of K) : Scheme.{u})).smallEtaleTopology AddCommGrpCat.{u + 1})
    (q : ℕ) :
    Sheaf.H.{u + 1, u + 1} F q ≃+
      continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) q
        ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj
          ((smallEtaleSheafRestriction B K hK).obj F))

AlgebraicGeometry.etaleGlobalSectionsIsoInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleStalkModules.lean, line 225. The attribute's comment: “part (2), as a natural isomorphism of functors, in the abelian-group encoding of discrete Galois modules”.

Stacks Project, Tag 03QU, part (2), as an isomorphism of functors. Over a field, global sections of an abelian étale sheaf and the Galois invariants of its module of Tag 04JQ are isomorphic functors to abelian groups, by taking germs at the geometric point.

def etaleGlobalSectionsIsoInvariants :
    (sheafSections (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}).obj
        (op (SmallEtale.final B (Spec (.of K)) hK)) ≅
      (abelianEtaleStalkEquivalence.{u, v} B K hK sbar).functor ⋙
        continuousGAddCommGrpInvariants.{u, max u v}
          (GeometricPoint.absoluteGaloisGroup sbar)

AlgebraicGeometry.etaleGlobalSectionsIsoContinuousGModuleInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleStalkModules.lean, line 257. The attribute's comment: “part (2), as a natural isomorphism of functors, in the coefficient category of continuousGroupCohomology”.

Stacks Project, Tag 03QU, part (2), as an isomorphism of functors, in the vocabulary of continuous group cohomology. Global sections of an abelian étale sheaf over a field are the continuousGModuleInvariants of the discrete Galois module of Tag 04JQ.

def etaleGlobalSectionsIsoContinuousGModuleInvariants :
    (sheafSections (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}).obj
        (op (SmallEtale.final B (Spec (.of K)) hK)) ≅
      (etaleContinuousGModuleEquivalence.{u, v} B K hK sbar).functor ⋙
        continuousGModuleInvariants.{u, max u v}
          (GeometricPoint.absoluteGaloisGroup sbar)

AlgebraicGeometry.etaleGammaIsoGaloisInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleStalkModules.lean, line 281. The attribute's comment: “part (2), as an isomorphism of functors on the global sections functor”.

Stacks Project, Tag 03QU, part (2), functorially, for the global sections functor of the site. The global sections functor CategoryTheory.Sheaf.Γ of the small étale site of the spectrum of a field is the functor of Galois invariants of the module of Tag 04JQ, in the abelian-group encoding of discrete Galois modules. This is AlgebraicGeometry.etaleGlobalSectionsIsoInvariants with sections over the final object rewritten as global sections.

def etaleGammaIsoGaloisInvariants
    [HasSheafify (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}] :
    Sheaf.Γ (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v} ≅
      (abelianEtaleStalkEquivalence.{u, v} B K hK sbar).functor ⋙
        continuousGAddCommGrpInvariants.{u, max u v}
          (GeometricPoint.absoluteGaloisGroup sbar)

AlgebraicGeometry.etaleGammaIsoContinuousGModuleInvariants, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/EtaleStalkModules.lean, line 295. The attribute's comment: “part (2), as an isomorphism of functors with the module invariants”.

Stacks Project, Tag 03QU, part (2), functorially and in the module encoding, for the global sections functor of the site. The global sections functor CategoryTheory.Sheaf.Γ of the small étale site of the spectrum of a field is the stalk equivalence of Tag 04JQ followed by the functor of G-invariants of discrete modules over the absolute Galois group.

def etaleGammaIsoContinuousGModuleInvariants
    [HasSheafify (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v}] :
    Sheaf.Γ (SmallEtale.topology B (Spec (.of K)) hK) AddCommGrpCat.{max u v} ≅
      (etaleContinuousGModuleEquivalence.{u, v} B K hK sbar).functor ⋙
        continuousGModuleInvariants.{u, max u v}
          (GeometricPoint.absoluteGaloisGroup sbar)

AlgebraicGeometry.multiplicativeSheafHAddEquivContinuousGroupCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupGaloisModule.lean, line 260. The attribute's comment: “part (3) at 𝐆_m, in every degree: the degree-q étale cohomology of the spectrum of a field with coefficients in the multiplicative group is the degree-q continuous group cohomology of the absolute Galois group with coefficients in the units of the separable closure. This is the general objectwise form of part (3) on Mathlib's small étale site, smallEtaleSheafCohomologyAddEquivContinuousGroupCohomology, with its Galois module computed at 𝐆_m by multiplicativeContinuousGModuleIso -- the stalk computation multiplicativeStalkIsoUnits packaged with its germwise Galois equivariance multiplicativeSectionEval_galoisFiberAction into an isomorphism of discrete Galois modules. Nothing is assumed of the field and nothing is carried. NOT proved here: parts (1) and (2) of the tag, which are separate registrations”.

For a field K, a geometric point sbar of Spec K and every degree q,

H^q_étale(Spec K, 𝐆_m) ≅ H^q(Gal(Kˢᵉᵖ/κ), (Kˢᵉᵖ)ˣ),

κ being the residue field at the image of sbar.

def multiplicativeSheafHAddEquivContinuousGroupCohomology (q : ℕ) :
    Sheaf.H.{u + 1, u + 1}
        (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec (.of K))) q ≃+
      continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) q
        (sepClosureUnitsGModule K sbar)
Tag 03QV, an example

Tag 03QV in the Stacks Project.

AlgebraicGeometry.stacks03QV, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/SheavesOnAPoint.lean, line 138.

Stacks Project, Tag 03QV, whole. Sheaves on Spec(K)_étale for K a field, with G = Gal(Kˢᵉᵖ/K) the absolute Galois group.

Under the equivalence of Tag 04JQ between abelian sheaves on the small étale site of Spec K and discrete G-modules: (1) the constant sheaf 𝐙/n𝐙 corresponds to 𝐙/n𝐙 with the trivial G-action, (2) 𝐆_m corresponds to (Kˢᵉᵖ)^*, (3) 𝐆_a corresponds to (Kˢᵉᵖ, +), and (4) μ_n corresponds to μ_n(Kˢᵉᵖ), each with its G-action. Moreover

0 = Pic(Spec K) = H¹_étale(Spec(K)_étale, 𝐆_m) = H¹(G, (Kˢᵉᵖ)^*),

which is Hilbert's 90 theorem, and, for every i ≥ 1,

0 = H^i(Spec K, 𝒪) = H^i_étale(Spec(K)_étale, 𝐆_a) = H^i(G, Kˢᵉᵖ).

The module docstring lists the declaration proving each component.

public def stacks03QV :
    ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj
        (constantEtaleSheaf B K hK (ULift.{u + 1} (ZMod n))) ≅
      constantGModule K sbar (ULift.{u + 1} (ZMod n))) ×
    ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj
        (multiplicativeSheafRestriction B K hK) ≅ sepClosureUnitsGModule K sbar) ×
    ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj
        (additiveSheafRestriction B K hK) ≅ sepClosureAddGModule K sbar) ×
    ((etaleContinuousGModuleEquivalence.{u, u + 1} B K hK sbar).functor.obj
        (rootsOfUnitySheafRestriction B K hK n) ≅ sepClosureRootsOfUnityGModule K sbar n) ×
    (Sheaf.H.{u + 1, u + 1}
        (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec (.of K))) 1 ≃+
      continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) 1
        (sepClosureUnitsGModule K sbar)) ×
    (∀ i : ℕ, Hgroup (Spec (CommRingCat.of K)).ringCatSheaf ⊤ (i + 1)
          (Scheme.unitModule (Spec (CommRingCat.of K))) ≃+
        Sheaf.H.{u + 1, u + 1}
          (Stacks.ArtinSchreier.additiveSheaf.{u, u + 1} (Spec (.of K))) (i + 1)) ×
    (∀ q : ℕ, Sheaf.H.{u + 1, u + 1}
          (Stacks.ArtinSchreier.additiveSheaf.{u, u + 1} (Spec (.of K))) q ≃+
        continuousGroupCohomology.{u, u + 1} (GeometricPoint.absoluteGaloisGroup sbar) q
          (sepClosureAddGModule K sbar)) ×
    PLift (Subsingleton (Spec (CommRingCat.of K)).picardGroup ∧
      Subsingleton (Sheaf.H.{u + 1, u + 1}
        (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec (.of K))) 1) ∧
      IsZero (continuousGroupCohomology.{u, u + 1}
        (GeometricPoint.absoluteGaloisGroup sbar) 1 (sepClosureUnitsGModule K sbar)) ∧
      (∀ i : ℕ, 0 < i → IsZero (Hgroup (Spec (CommRingCat.of K)).ringCatSheaf ⊤ i
        (Scheme.unitModule (Spec (CommRingCat.of K))))) ∧
      (∀ i : ℕ, 0 < i → Subsingleton (Sheaf.H.{u + 1, u + 1}
        (Stacks.ArtinSchreier.additiveSheaf.{u, u + 1} (Spec (.of K))) i)) ∧
      (∀ i : ℕ, 0 < i → IsZero (continuousGroupCohomology.{u, u + 1}
        (GeometricPoint.absoluteGaloisGroup sbar) i (sepClosureAddGModule K sbar))))
Tag 0D1W, a lemma

Tag 0D1W in the Stacks Project.

Stacks.EtaleCohomology.SmallEtaleModules.allModules_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/QuasiCoherentSheaves/ZeroDimensionalLocalRing.lean, line 1199.

Every module on the small étale site of a zero-dimensional local ring is quasi-coherent.

public theorem allModules_isQuasicoherent
    (R : Type u) [CommRing R] [IsLocalRing R] (hdim : ringKrullDim R = 0)
    (B : BigEtaleSite.{u})
    (hS : B.Contains (Spec (.of R)))
    (F : SheafOfModules.{u}
      (AlgebraicGeometry.SmallEtale.structureSheaf B (Spec (.of R)) hS)) :
    F.IsQuasicoherent
Sources
LeanAlgebraicGeometry.abelianEtaleSheafStalkEquivalence · AlgebraicGeometry.etaleContinuousGModuleEquivalence · AlgebraicGeometry.etaleH0AddEquivGaloisInvariants · AlgebraicGeometry.etaleH0AddEquivGaloisInvariants_coe · AlgebraicGeometry.etaleH0AddEquivGaloisInvariants_abelianEtaleStalkGerm · AlgebraicGeometry.additiveSheafHAddEquivContinuousGroupCohomology · AlgebraicGeometry.etaleRightDerivedGammaIsoContinuousGroupCohomologyFunctor · AlgebraicGeometry.etaleSheafCohomologyIsoContinuousGroupCohomologyFunctor

Section59.61 Brauer groups#

Section 59.61 of the Stacks Project, Tag 03R1. 7 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 10 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03R2, a theorem

Tag 03R2 in the Stacks Project.

Declarations registered for the tag:

Tag 03R4, a lemma

Tag 03R4 in the Stacks Project.

Declarations registered for the tag:

Tag 03R3, a definition

Tag 03R3 in the Stacks Project.

Declarations registered for the tag:

Tag 03R5, a definition

Tag 03R5 in the Stacks Project.

Declarations registered for the tag:

Tag 03R6, a lemma

Tag 03R6 in the Stacks Project.

centralSimpleAlgebraClassEquivPGLH1, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/NonabelianGaloisCohomology/Classification.lean, line 647. References: SGA 4½ Arcata (3.1.2), “θ_n bijection”.

Central simple algebras of degree d are classified by nonabelian PGL_d-valued Galois cohomology.

public noncomputable def centralSimpleAlgebraClassEquivPGLH1
    (K : Type u) [Field K] (Ksep : Type v) [Field Ksep] [Algebra K Ksep]
    [IsSepClosure K Ksep] (d : ℕ) (hd : d ≠ 0) :
    CentralSimpleAlgebraClass.{u, v} K d ≃ PGLH1 K Ksep d
Tag 0A2I, an equation

Tag 0A2I in the Stacks Project.

Stacks.GaloisCohomology.twoCocycleOfLift, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/ProjectiveLiftTwoCocycle.lean, line 142. The attribute's comment: “the two-cocycle”.

Equation 59.61.5.1. The two-cocycle attached to a family of lifts with central defect: the scalar g̃_σ⁻¹ g̃_{σ τ} σ(g̃_τ⁻¹) ∈ Kˣ.

def twoCocycleOfLift (i : n) (lift : G → GL n K)
    (hc : ∀ σ τ, liftDefect lift σ τ ∈ Subgroup.center (GL n K)) : G × G → Kˣ

Stacks.GaloisCohomology.scalar_twoCocycleOfLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/ProjectiveLiftTwoCocycle.lean, line 149. The attribute's comment: “the displayed formula”.

Equation 59.61.5.1, as displayed: the scalar matrix of the two-cocycle at (σ, τ) is g̃_σ⁻¹ g̃_{σ τ} σ(g̃_τ⁻¹).

theorem scalar_twoCocycleOfLift (i : n) (lift : G → GL n K)
    (hc : ∀ σ τ, liftDefect lift σ τ ∈ Subgroup.center (GL n K)) (σ τ : G) :
    Matrix.GeneralLinearGroup.scalar n (twoCocycleOfLift i lift hc (σ, τ)) =
      (lift σ)⁻¹ * lift (σ * τ) *
        Matrix.GeneralLinearGroup.map (MulSemiringAction.toRingHom G K σ) (lift τ)⁻¹

Stacks.GaloisCohomology.twoCocycleOfLift_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/ProjectiveLiftTwoCocycle.lean, line 198. The attribute's comment: “the two-cocycle identity”.

Stacks Project, Tag 0A2I. The scalar defect of a lift of a projective crossed homomorphism satisfies the multiplicative two-cocycle identity c(σ τ, υ) c(σ, τ) = σ(c(τ, υ)) c(σ, τ υ).

theorem twoCocycleOfLift_mul (i : n) (lift : G → GL n K)
    (hc : ∀ σ τ, liftDefect lift σ τ ∈ Subgroup.center (GL n K)) (σ τ υ : G) :
    twoCocycleOfLift i lift hc (σ * τ, υ) * twoCocycleOfLift i lift hc (σ, τ) =
      Units.map (MulSemiringAction.toRingHom G K σ : K →* K)
          (twoCocycleOfLift i lift hc (τ, υ)) *
        twoCocycleOfLift i lift hc (σ, τ * υ)

Stacks.GaloisCohomology.twoCocycleOfPGLCocycle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/ProjectiveLiftTwoCocycle.lean, line 275. The attribute's comment: “the Galois two-cocycle”.

Equation 59.61.5.1 for the absolute Galois group: the scalar two-cocycle (σ, τ) ↦ g̃_σ⁻¹ g̃_{σ τ} σ(g̃_τ⁻¹) attached to a lift of the projective cocycle classifying a central simple algebra of degree d.

def twoCocycleOfPGLCocycle (hd : 0 < d) (g : PGLCocycle K Ksep d)
    (lift : (Ksep ≃ₐ[K] Ksep) → GL (Fin d) Ksep)
    (hlift : ∀ σ, Matrix.ProjGenLinGroup.mk (lift σ) = g.toFun σ) :
    (Ksep ≃ₐ[K] Ksep) × (Ksep ≃ₐ[K] Ksep) → Ksepˣ

Stacks.GaloisCohomology.isMulCocycle₂_twoCocycleOfPGLCocycle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/ProjectiveLiftTwoCocycle.lean, line 296. The attribute's comment: “the Galois two-cocycle identity”.

Stacks Project, Tag 0A2I. The scalar defect of a lift of the projective cocycle of a central simple algebra is a two-cocycle of the absolute Galois group with values in (Kˢᵉᵖ)ˣ, for the action of Gal(Kˢᵉᵖ/K) on units used by the crossed product construction.

theorem isMulCocycle₂_twoCocycleOfPGLCocycle (hd : 0 < d) (g : PGLCocycle K Ksep d)
    (lift : (Ksep ≃ₐ[K] Ksep) → GL (Fin d) Ksep)
    (hlift : ∀ σ, Matrix.ProjGenLinGroup.mk (lift σ) = g.toFun σ) :
    IsMulCocycle₂ (twoCocycleOfPGLCocycle hd g lift hlift)
Tag 03R7, a theorem

Tag 03R7 in the Stacks Project.

Stacks.GaloisCohomology.brauerDelta, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupConnectingMap.lean, line 485. The attribute's comment: “the map δ”. References: SGA 4½ Arcata (3.1.2), “definition of δ”.

The map δ : Br(K) → H²(Gal(Kˢᵉᵖ/K), (Kˢᵉᵖ)ˣ). The Brauer class of a central simple algebra A of degree d is sent to the class of the scalar two-cocycle (σ, τ) ↦ g̃_σ⁻¹ g̃_{σ τ} σ(g̃_τ⁻¹) of a lift g̃ of the projective cocycle of a splitting of Kˢᵉᵖ ⊗ A.

def brauerDelta : BrauerGroup.{u, v} K → TwoCohomology K Ksep

Stacks.GaloisCohomology.brauerDelta_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupConnectingMap.lean, line 498. The attribute's comment: “δ is a group homomorphism”. References: SGA 4½ Arcata (3.1.2), “δ is a homomorphism”.

The map δ of tag 03R7 is a group homomorphism: it takes the group law of the Brauer group, which is tensor product, to the group law of the second cohomology group.

theorem brauerDelta_mul (x y : BrauerGroup.{u, v} K) :
    brauerDelta K Ksep (x * y) = brauerDelta K Ksep x * brauerDelta K Ksep y

Stacks.GaloisCohomology.brauerDelta_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupIsomorphism.lean, line 592. The attribute's comment: “δ is surjective”. References: SGA 4½ Arcata (3.1.2), “δ is surjective”.

δ is surjective. Every class in H²(Gal(Kˢᵉᵖ/K), (Kˢᵉᵖ)ˣ) is the class of a locally constant cocycle, that cocycle is the scalar defect of a projective cocycle, and the classification of tag 03R6 realises the projective class by a central simple algebra.

theorem brauerDelta_surjective :
    Function.Surjective (brauerDelta K Ksep : BrauerGroup.{u, v} K → TwoCohomology K Ksep)

Stacks.GaloisCohomology.brauerDelta_injective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupIsomorphism.lean, line 636. The attribute's comment: “δ is injective”. References: SGA 4½ Arcata (3.1.2), “δ is injective”.

δ is injective. If two central simple algebras have the same class then A ⊗ Bᵐᵒᵖ has trivial class, hence is a matrix algebra over K, and that exhibits a Brauer equivalence between A and B.

theorem brauerDelta_injective :
    Function.Injective (brauerDelta K Ksep : BrauerGroup.{u, v} K → TwoCohomology K Ksep)

Stacks.GaloisCohomology.brauerDelta_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupIsomorphism.lean, line 656. The attribute's comment: “δ is bijective”.

The map δ of tag 03R7 is bijective.

theorem brauerDelta_bijective :
    Function.Bijective (brauerDelta K Ksep : BrauerGroup.{u, v} K → TwoCohomology K Ksep)

Stacks.GaloisCohomology.brauerDeltaEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroups/BrauerGroupIsomorphism.lean, line 675. The attribute's comment: “δ is an isomorphism”. References: SGA 4½ Arcata (3.1.2), “δ is an isomorphism”.

Stacks Project, Tag 03R7. The map δ : Br(K) → H²(Gal(Kˢᵉᵖ/K), (Kˢᵉᵖ)ˣ) is an isomorphism of groups. As for brauerDeltaHom, the commutative group structure on the Brauer group is available for central simple algebras in the universe of the ground field, so this bundling is stated with Kˢᵉᵖ in that universe too; brauerDelta_injective and brauerDelta_surjective are the two halves without that restriction.

def brauerDeltaEquiv : BrauerGroup.{u, u} K ≃* TwoCohomology K Ksep
Sources
LeanAlgebra.isCentralSimple_tfae · Algebra.IsSplit.matrix_size_eq_degree · mulLeftRight_bijective_of_simple · IsBrauerEquivalent · BrauerGroup · BrauerGroup.mk · BrauerGroup.instCommGroup · BrauerGroup.mk_mul_mk

Section59.62 The Brauer group of a scheme#

Section 59.62 of the Stacks Project, Tag 0A2J. 3 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A2J, the section

Tag 0A2J in the Stacks Project.

Stacks.EtaleCohomology.BrauerScheme.IsSimilar, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/AlgebraSheaf.lean, line 362. The attribute's comment: “the equivalence of Azumaya algebras”.

The equivalence of Tag 0A2J. Two sheaves of 𝒪_S-algebras A and B are similar if there are finite locally free sheaves of 𝒪_S-modules F and G of positive rank at every point of S with A ⊗_{𝒪_S} 𝓗om(F,F) ≅ B ⊗_{𝒪_S} 𝓗om(G,G) as 𝒪_S-algebras. The Brauer group of S is the set of equivalence classes of Azumaya 𝒪_S-algebras for this relation, with the operation induced by the tensor product.

def IsSimilar (A B : AlgebraSheaf S) : Prop

Stacks.EtaleCohomology.BrauerScheme.IsAzumaya, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/AlgebraSheaf.lean, line 672. The attribute's comment: “the Azumaya condition”.

The Azumaya condition of Tag 0A2J. A sheaf of 𝒪_S-algebras is Azumaya if it is étale locally a matrix algebra: there is an étale covering {φ_i : U_i → S} of S and integers d_i ≥ 1 with φ_i^* A ≅ Mat_{d_i}(𝒪_{U_i}) as 𝒪_{U_i}-algebras. An AlgebraicGeometry.Scheme.Cover at AlgebraicGeometry.Scheme.etalePrecoverage packages both halves of "étale covering": every 𝒰.f i is étale, and the family is jointly surjective.

The pullback φ_i^* of the sheaf of algebras is algebraPullback, which transports the multiplication along the tensor comparison of Tag 01CD — the map φ^*(A ⊗ B) ⟶ φ^*A ⊗ φ^*B of Stacks.RingedSpace.comparison, see monoidalModulePullback.

def IsAzumaya {S : Scheme.{u}} (A : AlgebraSheaf S) : Prop

Stacks.EtaleCohomology.BrauerScheme.BrauerGroup, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/AlgebraSheaf.lean, line 689. The attribute's comment: “the Brauer group”.

The Brauer group of a scheme, Tag 0A2J: the set of equivalence classes of Azumaya 𝒪_S-algebras for the equivalence of IsSimilar. The operation induced by the tensor product is BrauerGroup.mul.

def BrauerGroup (S : Scheme.{u}) : Type (u + 1)

Stacks.EtaleCohomology.BrauerScheme.BrauerGroup.mul, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/AlgebraSheaf.lean, line 738. The attribute's comment: “the operation of the Brauer group”.

The operation of the Brauer group of Tag 0A2J: the one induced by the tensor product of sheaves of algebras. It is well defined because a tensor product of Azumaya algebra sheaves is Azumaya (IsAzumaya.tensor) and because similarity is compatible with the tensor product (IsSimilar.tensor).

def BrauerGroup.mul {S : Scheme.{u}} : BrauerGroup S → BrauerGroup S → BrauerGroup S
Tag 0A2K, a lemma

Tag 0A2K in the Stacks Project.

Stacks.EtaleCohomology.exists_invertible_tensor_iso_of_endomorphism_algebra_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/EndomorphismAlgebra/InvertibleTwist.lean, line 355.

An isomorphism of the endomorphism algebra sheaves of two positive-rank vector bundles is conjugation by an isomorphism after an invertible twist.

public theorem exists_invertible_tensor_iso_of_endomorphism_algebra_iso
    (S : Scheme.{u})
    (F G : SheafOfModules.{u} (structureSheaf S.sheaf))
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree (C := Opens S)
      (J := Opens.grothendieckTopology S) F]
    [AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree (C := Opens S)
      (J := Opens.grothendieckTopology S) G]
    (hF : ∃ q : SheafOfModules.LocalGeneratorsData F,
      q.IsLocallyFreeData ∧ ∀ i, Nonempty (q.generators i).I)
    (hG : ∃ q : SheafOfModules.LocalGeneratorsData G,
      q.IsLocallyFreeData ∧ ∀ i, Nonempty (q.generators i).I)
    (HFF : SheafHom S.sheaf F F) (HGG : SheafHom S.sheaf G G)
    (α : HFF.obj ≅ HGG.obj)
    (hα_one : ∀ U : Opens S, HGG.sectionsEquiv U
      (α.hom.val.app (op U) ((HFF.sectionsEquiv U).symm (𝟙 (F.over U)))) =
        𝟙 (G.over U))
    (hα_comp : ∀ (U : Opens S) (f g : F.over U ⟶ F.over U),
      HGG.sectionsEquiv U
        (α.hom.val.app (op U) ((HFF.sectionsEquiv U).symm (f ≫ g))) =
      (HGG.sectionsEquiv U
        (α.hom.val.app (op U) ((HFF.sectionsEquiv U).symm f))) ≫
      (HGG.sectionsEquiv U
        (α.hom.val.app (op U) ((HFF.sectionsEquiv U).symm g)))) :
    ∃ L : SheafOfModules.{u} (structureSheaf S.sheaf),
      Stacks.SheafOfModules.IsInvertible S.sheaf.obj (structureSheaf S.sheaf).property L ∧
      ∃ e : (((Stacks.SheafOfModules.Tensor.sheafTensor
          ⟨((S.toLocallyRingedSpace.toRingedSpace)).presheaf,
            ((S.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (L)) ≅ G,
        ∀ (U : Opens S) (s : HFF.obj.val.obj (op U))
          (f : F.val.obj (op U)) (l : L.val.obj (op U)),
          ((HGG.sectionsEquiv U (α.hom.val.app (op U) s)).val.app
            (op (Over.mk (𝟙 U)))).hom
              ((e.hom.val.app (op U)).hom
                (toTensorSheafSection S.toLocallyRingedSpace.toRingedSpace F L (op U)
                  (f ⊗ₜ[(O S.toLocallyRingedSpace.toRingedSpace).obj (op U)] l))) =
            (e.hom.val.app (op U)).hom
              (toTensorSheafSection S.toLocallyRingedSpace.toRingedSpace F L (op U)
                ((((HFF.sectionsEquiv U s).val.app (op (Over.mk (𝟙 U)))).hom f) ⊗ₜ[
                  (O S.toLocallyRingedSpace.toRingedSpace).obj (op U)] l))
Tag 0A2L, a lemma

Tag 0A2L in the Stacks Project.

Stacks.EtaleCohomology.BrauerScheme.brauerClass_pow_eq_one_of_rank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BrauerGroupScheme/BrauerClassAnnihilated.lean, line 212.

The class in Br(S) of an Azumaya 𝒪_S-algebra whose underlying sheaf of modules is finite locally free of rank d ^ 2 is annihilated by d.

This is [Stacks, Tag 0A2L]. The case d = 0 is pow_zero; for d ≥ 1 the reduction Stacks.EtaleCohomology.BrauerScheme.brauerClass_pow_eq_one_of_isTrivialClass_natTensorPow leaves exactly Saltman's construction, Stacks.EtaleCohomology.BrauerScheme.isTrivialClass_natTensorPow_of_rank.

theorem brauerClass_pow_eq_one_of_rank (A : Azumaya S) {d : ℕ}
    (hrank : AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank (C := Opens S)
      (J := Opens.grothendieckTopology S) A.1.X (d ^ 2)) :
    brauerClass A ^ d = 1
Sources
LeanStacks.EtaleCohomology.BrauerScheme.IsSimilar · Stacks.EtaleCohomology.BrauerScheme.IsAzumaya · Stacks.EtaleCohomology.BrauerScheme.BrauerGroup · Stacks.EtaleCohomology.BrauerScheme.BrauerGroup.mul · Stacks.EtaleCohomology.exists_invertible_tensor_iso_of_endomorphism_algebra_iso · Stacks.EtaleCohomology.BrauerScheme.brauerClass_pow_eq_one_of_rank

Section59.63 The Artin-Schreier sequence#

Section 59.63 of the Stacks Project, Tag 0A3J. 6 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A3J, the section

Tag 0A3J in the Stacks Project.

Stacks.ArtinSchreier.constantArtinSchreierSequence_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ConstantKernel.lean, line 404. References: SGA 1 XI (6.7); SGA 4 IX (3.5).

The Artin–Schreier sequence. For a scheme X of characteristic p,

0 ⟶ 𝐙/p𝐙 ⟶ 𝐆_a ⟶ 𝐆_a ⟶ 0

is a short exact sequence of abelian sheaves on the small étale site of X, the second map being x ↦ x ^ p - x.

theorem constantArtinSchreierSequence_shortExact :
    (constantArtinSchreierSequence.{u, v} X hp hX).ShortExact
Tag 0A3K, a lemma

Tag 0A3K in the Stacks Project.

Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ConstantCoefficientVanishingUnconditional.lean, line 48. The attribute's comment: “(2)”.

Let p be a prime and let S be a quasi-compact and quasi-separated scheme of characteristic p and of dimension at most d. Then H ^ q (S_étale, 𝐙/p𝐙) = 0 for every q ≥ d + 2. Only the upper bound on the dimension of S is needed.

public theorem subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_unconditional (p : ℕ)
    [Fact p.Prime] (S : Scheme.{u}) [CompactSpace S] [QuasiSeparatedSpace S]
    (hS : (p : Γ(S, ⊤)) = 0)
    [HasExt.{w} (Sheaf S.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (d : ℕ) (hdim : topologicalKrullDim (S : Type u) ≤ (d : WithBot ℕ∞))
    (q : ℕ) (hq : d + 2 ≤ q) :
    Subsingleton (Sheaf.H.{w, u + 1} (etaleConstantZMod S p) q)

Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_isAffine_constantSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ConstantSequenceDatum.lean, line 199. The attribute's comment: “part (1)”.

[Stacks, Tag 0A3K] (1). Let p be a prime and let S be an affine scheme on which p vanishes. Then H ^ q (S_étale, 𝐙/p𝐙) = 0 for every q ≥ 2.

The cohomology of the structure sheaf of an affine scheme vanishes in positive degree by [Stacks, Tag 01XB], so the Artin–Schreier degree shift applies with n = 0.

public theorem subsingleton_etaleH_constantZMod_of_isAffine_constantSequence (p : ℕ)
    [Fact p.Prime] (S : Scheme.{u}) [IsAffine S] (hS : (p : Γ(S, ⊤)) = 0)
    [HasExt.{w} (Sheaf S.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (q : ℕ) (hq : 2 ≤ q) :
    Subsingleton (Sheaf.H.{w, u + 1} (etaleConstantZMod S p) q)

Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_constantSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ConstantSequenceDatum.lean, line 216. The attribute's comment: “part (2)”. References: SGA 4½ Arcata (4.4), “H^q(X_0, special case”.

[Stacks, Tag 0A3K] (2). Let p be a prime and let S be a quasi-compact and quasi-separated scheme on which p vanishes and of dimension at most d. Then H ^ q (S_étale, 𝐙/p𝐙) = 0 for every q ≥ d + 2.

The underlying space of S is spectral, so the cohomology of the structure sheaf vanishes above its dimension by [Stacks, Tag 0A3G], and the Artin–Schreier degree shift applies with n = d.

public theorem subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_constantSequence
    (p : ℕ) [Fact p.Prime] (S : Scheme.{u}) [CompactSpace S] [QuasiSeparatedSpace S]
    (hS : (p : Γ(S, ⊤)) = 0)
    [HasExt.{u} (Sheaf (Opens.grothendieckTopology (S : Type u)) AddCommGrpCat.{u})]
    [HasExt.{w} (Sheaf S.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (d : ℕ) (hdim : topologicalKrullDim (S : Type u) ≤ (d : WithBot ℕ∞))
    (q : ℕ) (hq : d + 2 ≤ q) :
    Subsingleton (Sheaf.H.{w, u + 1} (etaleConstantZMod S p) q)
Tag 0A3L, a lemma

Tag 0A3L in the Stacks Project.

fixedPoints_finiteDimensional_of_frobenius_semilinear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/FrobeniusFixedPoints.lean, line 145. The attribute's comment: “kernel_bound”.

The fixed points of a Frobenius-semilinear additive endomorphism of a finite-dimensional vector space are finite-dimensional over the prime field.

theorem fixedPoints_finiteDimensional_of_frobenius_semilinear
    (hF : ∀ (c : k) (x : V), F (c • x) = c ^ p • F x) :
    letI : Module (ZMod p) V :=
      Module.compHom V (ZMod.castHom (dvd_refl p) k)
    FiniteDimensional (ZMod p) (AddMonoidHom.ker (F - AddMonoidHom.id V))

finrank_fixedPoints_le_of_frobenius_semilinear, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/FrobeniusFixedPoints.lean, line 159. The attribute's comment: “kernel_bound”.

The dimension over the prime field of the fixed points of a Frobenius-semilinear additive endomorphism is at most the dimension of the original vector space.

theorem finrank_fixedPoints_le_of_frobenius_semilinear
    (hF : ∀ (c : k) (x : V), F (c • x) = c ^ p • F x) :
    letI : Module (ZMod p) V :=
      Module.compHom V (ZMod.castHom (dvd_refl p) k)
    Module.finrank (ZMod p) (AddMonoidHom.ker (F - AddMonoidHom.id V)) ≤
      Module.finrank k V

frobeniusSemilinear_sub_id_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/FrobeniusSurjectivity.lean, line 40. The attribute's comment: “surjectivity”. References: SGA 7 XXII (1.2), “alg. closed, q=p”.

Let V be a finite-dimensional vector space over an algebraically closed field k of positive characteristic p. If the additive endomorphism F is Frobenius-semilinear, then F - 1 is surjective.

public theorem frobeniusSemilinear_sub_id_surjective
    {p : ℕ} (k : Type*) [Field k] [IsAlgClosed k] [CharP k p] (hp : 0 < p)
    (V : Type*) [AddCommGroup V] [Module k V] [FiniteDimensional k V]
    (F : V →+ V) (hF : ∀ (a : k) (v : V), F (a • v) = a ^ p • F v) :
    Function.Surjective (fun v ↦ F v - v)
Tag 0A3M, a lemma

Tag 0A3M in the Stacks Project.

AlgebraicGeometry.finiteDimensional_cohomologyOverField_of_finiteType_of_dimension_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeCoherentFiniteness/Basic.lean, line 96. The attribute's comment: “the case dim X = 0, in every degree and without the separatedness hypothesis”.

For X of finite type over a field k with dim(X) = 0 and ℱ coherent, every Hⁿ(X, ℱ) is a finite-dimensional k-vector space.

theorem finiteDimensional_cohomologyOverField_of_finiteType_of_dimension_zero
    [LocallyOfFiniteType f] [QuasiCompact f] (hdim : topologicalKrullDim (X : Type u) = 0)
    (F : X.Modules) [F.IsCoherent] (n : ℕ) :
    FiniteDimensional k (cohomologyOverField k f F n)

AlgebraicGeometry.finiteDimensional_topCohomology_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeCoherentFiniteness/Basic.lean, line 120. The attribute's comment: “the case of an affine X”.

Let X be an affine scheme separated and of finite type over a field k, let ℱ be a coherent 𝒪_X-module and let d = dim(X). Then H^d(X, ℱ) is a finite-dimensional k-vector space.

theorem finiteDimensional_topCohomology_of_isAffine [IsAffine X] [LocallyOfFiniteType f]
    [QuasiCompact f] [IsSeparated f] (F : X.Modules) [F.IsCoherent] (d : ℕ)
    (hd : topologicalKrullDim (X : Type u) = (d : WithBot ℕ∞)) :
    FiniteDimensional k (cohomologyOverField k f F d)

AlgebraicGeometry.finiteDimensional_cohomologyOverField_topologicalKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeCoherentFiniteness/Full.lean, line 376.

[Stacks, Tag 0A3M]. Let X be a separated scheme of finite type over a field k and let ℱ be a coherent 𝒪_X-module. Then dim_k H^d(X, ℱ) < ∞, where d = dim(X).

theorem finiteDimensional_cohomologyOverField_topologicalKrullDim (k : Type u) [Field k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [LocallyOfFiniteType f] [QuasiCompact f]
    [IsSeparated f] (F : X.Modules) (hF : _root_.SheafOfModules.IsCoherent F) (d : ℕ)
    (hd : topologicalKrullDim (X : Type u) = (d : WithBot ℕ∞)) :
    FiniteDimensional k (cohomologyOverField k f F d)

AlgebraicGeometry.TopDegreeFiniteness.finiteDimensional_topCohomology_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeCoherentFiniteness/General.lean, line 293.

Let X be a separated scheme of finite type over a field k, let ℱ be a coherent 𝒪_X-module and let d = dim(X). Then H^d(X, ℱ) is a finite-dimensional k-vector space.

theorem finiteDimensional_topCohomology_of_isSeparated {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] (F : X.Modules) [F.IsCoherent]
    (d : ℕ) (hd : topologicalKrullDim X = (d : WithBot ℕ∞)) :
    FiniteDimensional k (cohomologyOverField k f F d)

AlgebraicGeometry.finiteDimensional_topCohomology_of_isSeparated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TopDegreeCoherentFiniteness/Separated.lean, line 156. The attribute's comment: “the full statement: for X separated and of finite type over a field k, F a coherent O_X-module and d = dim X, the k-vector space H^d(X, F) is finite-dimensional”.

[Stacks, Tag 0A3M]. Let X be a separated scheme of finite type over a field k, with structure morphism f : X ⟶ Spec k, let ℱ be a coherent 𝒪_X-module and let d = dim(X). Then H^d(X, ℱ) is a finite-dimensional k-vector space.

Nagata's compactification theorem ([Stacks, Tag 0F41], AlgebraicGeometry.hasCompactification_of_compactSpace_quasiSeparatedSpace, applied over the affine base Spec k) factors f as a quasi-compact open immersion followed by a proper morphism, and finiteDimensional_cohomologyOverField_of_isImmersion_of_isProper applies.

theorem finiteDimensional_topCohomology_of_isSeparated {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f] (F : X.Modules) [F.IsCoherent]
    (d : ℕ) (hd : topologicalKrullDim (X : Type u) = (d : WithBot ℕ∞)) :
    FiniteDimensional k (cohomologyOverField k f F d)
Tag 0A3N, a lemma

Tag 0A3N in the Stacks Project.

Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_isAlgClosed_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/TopDegreeVanishingUnconditional.lean, line 45. References: SGA 4½ Arcata (4.4), “special case”.

Let X be separated and of finite type over an algebraically closed field k of characteristic p > 0, and let d be a natural number with dim X ≤ d. Then H ^ q (X_étale, 𝐙/p𝐙) = 0 for every q ≥ d + 1.

public theorem subsingleton_etaleH_constantZMod_of_isAlgClosed_unconditional {p : ℕ} (hp : 0 < p)
    (k : Type u) [Field k] [IsAlgClosed k] [CharP k p] {X : Scheme.{u}} (f : X ⟶ Spec (.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] [IsSeparated f]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})]
    (d : ℕ) (hd : topologicalKrullDim (X : Type u) ≤ (d : WithBot ℕ∞))
    (q : ℕ) (hq : d + 1 ≤ q) :
    Subsingleton (Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q)
Tag 0A3P, a lemma

Tag 0A3P in the Stacks Project.

Stacks.ArtinSchreier.finite_etaleH_constantZMod_of_isProper', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ConstantCoefficientsUnconditional.lean, line 69. The attribute's comment: “part (1)”.

Let X be a scheme proper over an algebraically closed field k of characteristic p > 0. Then H ^ q (X_étale, 𝐙/p𝐙) is finite for every q.

theorem finite_etaleH_constantZMod_of_isProper' {p : ℕ} (hp : 0 < p) (k : Type u) [Field k]
    [IsAlgClosed k] [CharP k p] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsProper f]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})] (q : ℕ) :
    Finite (Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q)

Stacks.ArtinSchreier.finite_etaleH_constantZMod_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperConstantCoefficients.lean, line 195. The attribute's comment: “part (1); the Artin-Schreier sequence (0A3J) and the comparison of étale with Zariski cohomology of the structure sheaf in its Frobenius-semilinear form (03P2) are carried as hypotheses”.

[Stacks, Tag 0A3P] (1). Let X be a scheme proper over an algebraically closed field k of characteristic p > 0. Then H ^ q (X_étale, 𝐙/p𝐙) is finite for every q.

The Artin–Schreier comparison embeds H ^ q (X_étale, 𝐙/p𝐙) into the F-fixed vectors of H ^ q (X, 𝒪_X). That group is a finite-dimensional k-vector space by [Stacks, Tag 02O6], X being proper over k, so its F-fixed vectors form a finite-dimensional module over the prime field 𝐙/p𝐙 by [Stacks, Tag 0A3L], hence a finite set.

public theorem finite_etaleH_constantZMod_of_isProper (hp : 0 < p) [IsAlgClosed k] [CharP k p]
    [IsProper f] (cmp : ∀ i : ℕ, TopDegreeFrobeniusComparison p k f AS.Ga AS.φ i) :
    Finite (Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q)

Stacks.ArtinSchreier.bijective_of_frobenius_base_change, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperConstantCoefficients.lean, line 553. The attribute's comment: “part (2); the Artin-Schreier sequence (0A3J), the comparison of étale with Zariski cohomology of the structure sheaf in its Frobenius-semilinear form (03P2), the flat base change of the cohomology of the structure sheaf (02KH) and the induced map on étale cohomology are carried as hypotheses”.

[Stacks, Tag 0A3P] (2). Let X be proper over an algebraically closed field k of characteristic p > 0, let k' be another algebraically closed field with a ring map φ : k ⟶ k', and let X' be proper over k'. Suppose β is the base-change map on the cohomology of the structure sheaves, so that H ^ q (X', 𝒪_{X'}) is the base change along φ of H ^ q (X, 𝒪_X) compatibly with the Frobenius, and suppose γ is a map on the étale cohomology of 𝐙/p𝐙 compatible with β through the two Artin–Schreier comparisons. Then γ is bijective.

The compatibility hγ determines γ uniquely, the Artin–Schreier comparison of X' being injective, so no generality is lost by carrying γ. For the scalar extension X' = X ×_k k' along an extension of algebraically closed fields, β is the flat base change of [Stacks, Tag 02KH] and γ is the canonical map Stacks.EtaleCohomology.etaleCohomologyBaseChangeMap.

Both sides are identified with the Frobenius-fixed vectors of the cohomology of the structure sheaf, finite-dimensional because X and X' are proper, and bijOn_fixedPoints_of_frobenius_base_change matches the two groups of fixed vectors.

public theorem bijective_of_frobenius_base_change (hp : 0 < p)
    (cmp : ∀ i : ℕ, TopDegreeFrobeniusComparison p k f AS.Ga AS.φ i)
    (cmp' : ∀ i : ℕ, TopDegreeFrobeniusComparison p k' f' AS'.Ga AS'.φ i)
    (β : cohomologyOverField k f (SheafOfModules.unit X.ringCatSheaf) q →+
      cohomologyOverField k' f' (SheafOfModules.unit X'.ringCatSheaf) q)
    (hβ : ∀ (c : k) (v : cohomologyOverField k f (SheafOfModules.unit X.ringCatSheaf) q),
      β (c • v) = φ c • β v)
    (hβinj : Function.Injective β) (hβspan : Submodule.span k' (Set.range β) = ⊤)
    (hβfrob : ∀ v, β ((cmp q).frobenius v) = (cmp' q).frobenius (β v))
    (γ : Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q →+
      Sheaf.H.{w, u + 1} (etaleConstantZMod X' p) q)
    (hγ : ∀ x, artinSchreierComparison k' f' AS' q (cmp' q) (γ x) =
      β (artinSchreierComparison k f AS q (cmp q) x)) :
    Function.Bijective γ

Stacks.ArtinSchreier.finite_etaleH_constantZMod_of_isProper_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperConstantCoefficientsUnconditional.lean, line 174. The attribute's comment: “(1)”.

Let X be a scheme proper over an algebraically closed field k of characteristic p > 0. Then H ^ q (X_étale, 𝐙/p𝐙) is finite for every q.

public theorem finite_etaleH_constantZMod_of_isProper_unconditional (hp : 0 < p) [IsAlgClosed k]
    [CharP k p] [IsProper f] (q : ℕ) :
    Finite (Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q)

Stacks.ArtinSchreier.bijective_etaleCohomologyBaseChangeMap_constantZMod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperConstantCoefficientsUnconditional.lean, line 302. The attribute's comment: “(2)”.

Let X be proper over an algebraically closed field k of characteristic p > 0, and let k'/k be an extension of algebraically closed fields. Then the restriction map H ^ q (X_étale, 𝐙/p𝐙) ⟶ H ^ q (X_{k'}, 𝐙/p𝐙) to the scalar extension X_{k'} = X ×_{Spec k} Spec k' is bijective.

public theorem bijective_etaleCohomologyBaseChangeMap_constantZMod {p : ℕ} (hp : 0 < p)
    [IsAlgClosed k] [IsAlgClosed k'] [CharP k p] [IsProper f]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})]
    [HasExt.{w} (Sheaf (scalarExtension k k' f).smallEtaleTopology AddCommGrpCat.{u + 1})]
    (q : ℕ) :
    Function.Bijective
      (etaleCohomologyBaseChangeMap.{u, 0, w} k k' f (etaleConstantZMod X p) q)

Stacks.ArtinSchreier.finite_etaleH_constantZMod_of_isProper_of_isAlgClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperFiniteness.lean, line 36. The attribute's comment: “part (1)”.

[Stacks, Tag 0A3P] (1). Let X be a proper scheme over an algebraically closed field k of characteristic p > 0. Then H ^ q (X_étale, 𝐙/p𝐙) is finite for every q.

theorem finite_etaleH_constantZMod_of_isProper_of_isAlgClosed {p : ℕ} (hp : p.Prime)
    (k : Type u) [Field k] [IsAlgClosed k] [CharP k p] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsProper f]
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1})] (q : ℕ) :
    Finite (Sheaf.H.{w, u + 1} (etaleConstantZMod X p) q)

Stacks.ArtinSchreier.bijective_etaleCohomologyRestrictionMap_constantZMod, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ArtinSchreierSequence/ProperScalarExtension.lean, line 166. The attribute's comment: “part (2)”.

[Stacks, Tag 0A3P] (2). Let k ⊆ k' be an extension of algebraically closed fields of characteristic p > 0 and let X be a proper scheme over k. Then restriction along X_{k'} ⟶ X is bijective on H^q(X_étale, 𝐙/p𝐙) for every q.

The target of the restriction map is the cohomology of the inverse image of the constant sheaf, which is the constant sheaf 𝐙/p𝐙 on X_{k'} by Stacks.EtaleCohomology.etaleAbelianInverseImageConstantIso.

theorem bijective_etaleCohomologyRestrictionMap_constantZMod {p : ℕ} (hp : 0 < p)
    [IsAlgClosed k] [IsAlgClosed k'] [CharP k p] [IsProper f] (q : ℕ) :
    Function.Bijective (etaleCohomologyRestrictionMap.{u, 0, w} (scalarExtensionFst k k' f)
      (etaleConstantZMod X p) q)
Sources
LeanStacks.ArtinSchreier.constantArtinSchreierSequence_shortExact · Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_unconditional · Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_isAffine_constantSequence · Stacks.ArtinSchreier.subsingleton_etaleH_constantZMod_of_topologicalKrullDim_le_constantSequence · fixedPoints_finiteDimensional_of_frobenius_semilinear · finrank_fixedPoints_le_of_frobenius_semilinear · frobeniusSemilinear_sub_id_surjective · AlgebraicGeometry.finiteDimensional_cohomologyOverField_of_finiteType_of_dimension_zero

Section59.64 Locally constant sheaves#

Section 59.64 of the Stacks Project, Tag 09Y8. 8 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03RU, a definition

Tag 03RU in the Stacks Project.

Stacks.ConstantSheaf.IsLocallyConstant, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Defs.lean, line 73. The attribute's comment: “finite locally constant sheaves of sets and of abelian groups”. References: EGA 0 (3.6.1), “locally simple”; SGA 3 X (9.2.1), “(2), (4)”; SGA 4 IX (2.0), “locally constant”.

Stacks 093Q (2). A sheaf is locally constant if every object of the site has a covering on each member of which its restriction is a constant sheaf.

class IsLocallyConstant [∀ U : C, HasWeakSheafify (J.over U) D] (F : Sheaf J D) : Prop

Stacks.ConstantSheaf.IsFiniteLocallyConstant, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/LocallyConstant/Defs.lean, line 86. The attribute's comment: “finite locally constant sheaves of sets and of abelian groups”.

Stacks 093Q (3). A sheaf with values in a concrete category is finite locally constant if every object of the site has a covering on each member of which it is a constant sheaf with finite underlying value. For Type and Grp, this is respectively the source's notion for sheaves of sets and sheaves of groups.

class IsFiniteLocallyConstant {FD : D → D → Type*} {CD : D → Type w}
    [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{w} D FD]
    [∀ U : C, HasWeakSheafify (J.over U) D] (F : Sheaf J D) : Prop

Declarations registered for the tag:

Tag 095A, a lemma

Tag 095A in the Stacks Project.

AlgebraicGeometry.isLocallyConstant_smallEtaleSheafPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantPullback/SmallEtaleInverseImage.lean, line 129. The attribute's comment: “small étale inverse image”.

Tag 093R for small étale sites. The inverse image of a locally constant sheaf along a morphism of small étale sites is locally constant, for arbitrary coefficients.

public theorem isLocallyConstant_smallEtaleSheafPullback
    (F : Sheaf (SmallEtale.topology B S.obj S.property) A)
    [Stacks.ConstantSheaf.IsLocallyConstant (SmallEtale.topology B S.obj S.property) F] :
    Stacks.ConstantSheaf.IsLocallyConstant (SmallEtale.topology B T.obj T.property)
      (((smallEtaleBaseChange B f).sheafPullback A
        (SmallEtale.topology B S.obj S.property)
        (SmallEtale.topology B T.obj T.property)).obj F)
Tag 095B, a lemma

Tag 095B in the Stacks Project.

Stacks.ConstantSheaf.isLocallyConstant_finiteEtalePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 486. The attribute's comment: “locally constant sheaves of sets”.

Direct image of a locally constant étale sheaf of sets along a finite étale morphism is locally constant.

public theorem isLocallyConstant_finiteEtalePushforward {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    (F : Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)))
    [Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology X) F] :
    Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        (Type (max (u + 1) v)) (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)

Stacks.ConstantSheaf.isFiniteLocallyConstant_finiteEtalePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 502. The attribute's comment: “finite locally constant sheaves of sets”.

Direct image of a finite locally constant étale sheaf of sets along a finite étale morphism is finite locally constant.

public theorem isFiniteLocallyConstant_finiteEtalePushforward {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    (F : Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)))
    [Stacks.ConstantSheaf.IsFiniteLocallyConstant (smallEtaleTopology X) F] :
    Stacks.ConstantSheaf.IsFiniteLocallyConstant (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        (Type (max (u + 1) v)) (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)

Stacks.ConstantSheaf.isLocallyConstant_finiteEtalePushforward_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 518. The attribute's comment: “locally constant sheaves of abelian groups”.

Direct image of a locally constant étale sheaf of abelian groups along a finite étale morphism is locally constant.

public theorem isLocallyConstant_finiteEtalePushforward_abelian {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) AddCommGrpCat.{max (u + 1) v}]
    [∀ V : Y.Etale, HasWeakSheafify ((smallEtaleTopology Y).over V) AddCommGrpCat.{max (u + 1) v}]
    (F : Sheaf (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v})
    [Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology X) F] :
    Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        AddCommGrpCat.{max (u + 1) v} (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)

Stacks.ConstantSheaf.isFiniteLocallyConstant_finiteEtalePushforward_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 536. The attribute's comment: “finite locally constant sheaves of abelian groups”.

Direct image of a finite locally constant étale sheaf of abelian groups along a finite étale morphism is finite locally constant.

public theorem isFiniteLocallyConstant_finiteEtalePushforward_abelian {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) AddCommGrpCat.{max (u + 1) v}]
    [∀ V : Y.Etale, HasWeakSheafify ((smallEtaleTopology Y).over V) AddCommGrpCat.{max (u + 1) v}]
    (F : Sheaf (smallEtaleTopology X) AddCommGrpCat.{max (u + 1) v})
    [Stacks.ConstantSheaf.IsFiniteLocallyConstant (smallEtaleTopology X) F] :
    Stacks.ConstantSheaf.IsFiniteLocallyConstant (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        AddCommGrpCat.{max (u + 1) v} (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)

Stacks.ConstantSheaf.isLocallyConstant_finiteEtalePushforward_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 554. The attribute's comment: “locally constant sheaves of modules”.

Direct image of a locally constant étale sheaf of modules along a finite étale morphism is locally constant.

public theorem isLocallyConstant_finiteEtalePushforward_modules {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    (R : Type r) [Ring R]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) (ModuleCat.{max (u + 1) v} R)]
    [∀ V : Y.Etale, HasWeakSheafify ((smallEtaleTopology Y).over V) (ModuleCat.{max (u + 1) v} R)]
    (F : Sheaf (smallEtaleTopology X) (ModuleCat.{max (u + 1) v} R))
    [Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology X) F] :
    Stacks.ConstantSheaf.IsLocallyConstant (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{max (u + 1) v} R) (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)

Stacks.ConstantSheaf.isFiniteTypeLocallyConstant_finiteEtalePushforward_modules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/FiniteEtalePushforward/LocallyQConstant.lean, line 573. The attribute's comment: “finite-type locally constant sheaves of modules”.

Direct image of a finite-type locally constant étale sheaf of modules along a finite étale morphism is finite-type locally constant.

public theorem isFiniteTypeLocallyConstant_finiteEtalePushforward_modules {X Y : Scheme.{u}}
    (f : X ⟶ Y) [IsFinite f] [Etale f]
    (R : Type r) [Ring R]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) (ModuleCat.{max (u + 1) v} R)]
    [∀ V : Y.Etale, HasWeakSheafify ((smallEtaleTopology Y).over V) (ModuleCat.{max (u + 1) v} R)]
    (F : Sheaf (smallEtaleTopology X) (ModuleCat.{max (u + 1) v} R))
    (hF : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant R (smallEtaleTopology X) F) :
    Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant R (smallEtaleTopology Y)
      (((Stacks.EtaleCohomology.smallEtaleBaseChange f).sheafPushforwardContinuous
        (ModuleCat.{max (u + 1) v} R) (smallEtaleTopology Y) (smallEtaleTopology X)).obj F)
Tag 03RV, a lemma

Tag 03RV in the Stacks Project.

Stacks.EtaleCohomology.isFiniteLocallyConstant_iff_finiteEtaleRepresentable_of_descent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/EtaleLocalRepresentability.lean, line 179.

A sheaf of sets on the small étale site of X is finite locally constant if and only if it is represented by an object of the site whose structure morphism is finite, that is, by a scheme finite étale over X. It takes a binder hdesc : EtaleDescentForFiniteEtaleRepresentability B, which defaults to the theorem Stacks.EtaleCohomology.etaleDescentForFiniteEtaleRepresentability, so the statement applies to B X F alone.

public theorem isFiniteLocallyConstant_iff_finiteEtaleRepresentable_of_descent
    (B : AlgebraicGeometry.BigEtaleSite.{u}) (X : B.Scheme)
    (F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1)))
    (hdesc : EtaleDescentForFiniteEtaleRepresentability B :=
      etaleDescentForFiniteEtaleRepresentability B) :
    Stacks.ConstantSheaf.IsFiniteLocallyConstant (SmallEtale.topology B X.1 X.property) F ↔
      ∃ U : SmallEtale B X.1 X.property,
        IsFinite (B.inclusion.map U.obj.hom) ∧
          Nonempty (F ≅
            (Sheaf.sheafifiedYoneda (SmallEtale.topology B X.1 X.property)).obj U)

Stacks.EtaleCohomology.isFiniteLocallyConstant_iff_finiteEtaleRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/RepresentabilityDescent.lean, line 1316. References: SGA 4 IX (2.2).

Stacks Project, Tag 03RV. A sheaf of sets on the small étale site of X is finite locally constant if and only if it is represented by an object of the site whose structure morphism is finite — that is, by a scheme finite étale over X.

The reverse implication is Stacks.EtaleCohomology.isFiniteLocallyConstant_of_finiteEtaleRepresentable. The forward one is the étale-local representability of Stacks.EtaleCohomology.exists_sliceRepresentatives_of_isFiniteLocallyConstant followed by effective descent for schemes affine over the base along an fpqc covering, Stacks 0245, in the form AlgebraicGeometry.DescentData.isFamilyEffective_of_isAffineHom_of_anyIndex.

public theorem isFiniteLocallyConstant_iff_finiteEtaleRepresentable
    (B : BigEtaleSite.{u}) (X : B.Scheme)
    (F : Sheaf (SmallEtale.topology B X.1 X.2) (Type (u + 1))) :
    Stacks.ConstantSheaf.IsFiniteLocallyConstant (SmallEtale.topology B X.1 X.2) F ↔
      ∃ U : SmallEtale B X.1 X.2,
        IsFinite (B.inclusion.map U.obj.hom) ∧
          Nonempty (F ≅
            (Sheaf.sheafifiedYoneda (SmallEtale.topology B X.1 X.2)).obj U)

AlgebraicGeometry.finiteLocallyConstantFiniteEtaleEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FundamentalGroupLocallyConstant/Sets.lean, line 67. The attribute's comment: “the equivalence of categories; the object-level statement is Stacks.EtaleCohomology.isFiniteLocallyConstant_iff_finiteEtaleRepresentable”.

The equivalence between the finite locally constant sheaves of sets on the small étale site of X and the finite étale covers of X.

public noncomputable def finiteLocallyConstantFiniteEtaleEquivalence :
    FiniteLocallyConstantSheaf B X ≌ FiniteEtaleOver X.1
Tag 095C, a lemma

Tag 095C in the Stacks Project.

Stacks.ConstantSheaf.exists_etaleCover_restrict_eq_constantSheaf_map, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleLocallyConstantMorphisms.lean, line 68. The attribute's comment: “sheaves of sets”. References: SGA 4 IX (2.1), “(i), étale site”.

Stacks 095C (1). A morphism of locally constant sheaves of sets on the small étale site of a scheme, whose source is finite locally constant, is on an étale covering of any object the morphism of constant sheaves attached to a map of sets.

lemma exists_etaleCover_restrict_eq_constantSheaf_map
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) (Type w)]
    (F G : Sheaf (smallEtaleTopology X) (Type w)) (φ : F ⟶ G)
    [IsFiniteLocallyConstant (smallEtaleTopology X) F]
    [IsLocallyConstant (smallEtaleTopology X) G] (U : X.Etale) :
    ∃ (I : Type (u + 1)) (V : I → X.Etale) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ smallEtaleTopology X U ∧ ∀ i,
        ∃ (A B : Type w), Finite A ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf ((smallEtaleTopology X).over (V i)) (Type w)).obj A ≅
              ((smallEtaleTopology X).overPullback (Type w) (V i)).obj F)
            (eG : (constantSheaf ((smallEtaleTopology X).over (V i)) (Type w)).obj B ≅
              ((smallEtaleTopology X).overPullback (Type w) (V i)).obj G),
              (constantSheaf ((smallEtaleTopology X).over (V i)) (Type w)).map g ≫ eG.hom =
                eF.hom ≫ ((smallEtaleTopology X).overPullback (Type w) (V i)).map φ

Stacks.ConstantSheaf.exists_etaleCover_restrict_eq_constantSheaf_map_abelian, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleLocallyConstantMorphisms.lean, line 89. The attribute's comment: “sheaves of abelian groups”. References: SGA 4 IX (2.1), “(ii) map, étale abelian”.

Stacks 095C (2). A morphism of locally constant sheaves of abelian groups on the small étale site of a scheme, whose source is finite locally constant, is on an étale covering of any object the morphism of constant sheaves attached to a homomorphism of abelian groups.

lemma exists_etaleCover_restrict_eq_constantSheaf_map_abelian [UnivLE.{u + 1, w}]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) Ab.{w}]
    (F G : Sheaf (smallEtaleTopology X) Ab.{w}) (φ : F ⟶ G)
    [IsFiniteLocallyConstant (smallEtaleTopology X) F]
    [IsLocallyConstant (smallEtaleTopology X) G] (U : X.Etale) :
    ∃ (I : Type (u + 1)) (V : I → X.Etale) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ smallEtaleTopology X U ∧ ∀ i,
        ∃ (A B : Ab.{w}), Finite (A : Type w) ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf ((smallEtaleTopology X).over (V i)) Ab.{w}).obj A ≅
              ((smallEtaleTopology X).overPullback Ab.{w} (V i)).obj F)
            (eG : (constantSheaf ((smallEtaleTopology X).over (V i)) Ab.{w}).obj B ≅
              ((smallEtaleTopology X).overPullback Ab.{w} (V i)).obj G),
              (constantSheaf ((smallEtaleTopology X).over (V i)) Ab.{w}).map g ≫ eG.hom =
                eF.hom ≫ ((smallEtaleTopology X).overPullback Ab.{w} (V i)).map φ

Stacks.ConstantSheaf.exists_etaleCover_restrict_eq_constantSheaf_map_modules, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleLocallyConstantMorphisms.lean, line 110. The attribute's comment: “sheaves of modules”. References: SGA 4 IX (2.1), “(ii) map, étale site”.

Stacks 095C (3). A morphism of locally constant sheaves of R-modules on the small étale site of a scheme, whose source is locally constant of finite type, is on an étale covering of any object the morphism of constant sheaves attached to a homomorphism of R-modules.

lemma exists_etaleCover_restrict_eq_constantSheaf_map_modules {R : Type r} [Ring R]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) (ModuleCat.{w} R)]
    (F G : Sheaf (smallEtaleTopology X) (ModuleCat.{w} R)) (φ : F ⟶ G)
    (hF : IsFiniteTypeLocallyConstant R (smallEtaleTopology X) F)
    [IsLocallyConstant (smallEtaleTopology X) G] (U : X.Etale) :
    ∃ (I : Type (u + 1)) (V : I → X.Etale) (f : ∀ i, V i ⟶ U),
      Sieve.ofArrows V f ∈ smallEtaleTopology X U ∧ ∀ i,
        ∃ (A B : ModuleCat.{w} R), ModuleCat.isFG R A ∧
          ∃ (g : A ⟶ B)
            (eF : (constantSheaf ((smallEtaleTopology X).over (V i)) (ModuleCat.{w} R)).obj A ≅
              ((smallEtaleTopology X).overPullback (ModuleCat.{w} R) (V i)).obj F)
            (eG : (constantSheaf ((smallEtaleTopology X).over (V i)) (ModuleCat.{w} R)).obj B ≅
              ((smallEtaleTopology X).overPullback (ModuleCat.{w} R) (V i)).obj G),
              (constantSheaf ((smallEtaleTopology X).over (V i)) (ModuleCat.{w} R)).map g ≫
                  eG.hom =
                eF.hom ≫ ((smallEtaleTopology X).overPullback (ModuleCat.{w} R) (V i)).map φ
Tag 03RX, a lemma

Tag 03RX in the Stacks Project.

Declarations registered for the tag:

Tag 095D, a lemma

Tag 095D in the Stacks Project.

Stacks.ConstantSheaf.isLocallyConstant_tensor_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantSheaves/TensorProduct.lean, line 66. References: SGA 5 VI (1.4.5), “locally constant claim”.

Stacks 095D. The tensor product of two locally constant sheaves of Λ-modules on the small étale site of a scheme is a locally constant sheaf of Λ-modules.

theorem isLocallyConstant_tensor_smallEtale {X : Scheme.{u}} (Λ : Type w) [CommRing Λ]
    [UnivLE.{u + 1, w}]
    [HasWeakSheafify (smallEtaleTopology X) (ModuleCat.{w} Λ)]
    [∀ U : X.Etale, HasWeakSheafify ((smallEtaleTopology X).over U) (ModuleCat.{w} Λ)]
    (F G : Sheaf (smallEtaleTopology X) (ModuleCat.{w} Λ))
    [IsLocallyConstant (smallEtaleTopology X) F]
    [IsLocallyConstant (smallEtaleTopology X) G] :
    IsLocallyConstant (smallEtaleTopology X) (F ⊗ G)
Tag 09BF, a lemma

Tag 09BF in the Stacks Project.

AlgebraicGeometry.exists_etaleCover_constant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocallyConstantSheaves/ConnectedTrivialization.lean, line 238.

Stacks 09BF. On a connected scheme, a locally constant sheaf of modules becomes the constant sheaf associated to one fixed module after an étale covering.

public theorem exists_etaleCover_constant
    (X : Scheme.{u}) [ConnectedSpace X]
    (Λ : Type v) [Ring Λ]
    [HasWeakSheafify X.smallEtaleTopology (ModuleCat.{v} Λ)]
    [∀ U : X.Etale, HasWeakSheafify (X.smallEtaleTopology.over U) (ModuleCat.{v} Λ)]
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{v} Λ))
    [Stacks.ConstantSheaf.IsLocallyConstant X.smallEtaleTopology F] :
    ∃ (M : ModuleCat.{v} Λ) (I : Type (u + 1)) (U : I → X.Etale),
      ((⋃ i, Set.range (fun x : (U i).left =>
        (((U i).hom : (U i).left ⟶ X) x))) : Set X) = Set.univ ∧
        ∀ i, Nonempty
          ((X.smallEtaleTopology.overPullback (ModuleCat.{v} Λ) (U i)).obj F ≅
            (X.smallEtaleTopology.overPullback (ModuleCat.{v} Λ) (U i)).obj
              ((constantSheaf X.smallEtaleTopology (ModuleCat.{v} Λ)).obj M))
Sources
LeanStacks.ConstantSheaf.IsLocallyConstant · Stacks.ConstantSheaf.IsFiniteLocallyConstant · CategoryTheory.Sheaf.IsConstant · AlgebraicGeometry.isLocallyConstant_smallEtaleSheafPullback · Stacks.ConstantSheaf.isLocallyConstant_finiteEtalePushforward · Stacks.ConstantSheaf.isFiniteLocallyConstant_finiteEtalePushforward · Stacks.ConstantSheaf.isLocallyConstant_finiteEtalePushforward_abelian · Stacks.ConstantSheaf.isFiniteLocallyConstant_finiteEtalePushforward_abelian

Section59.65 Locally constant sheaves and the fundamental group#

Section 59.65 of the Stacks Project, Tag 0DV4. 3 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DV5, a lemma

Tag 0DV5 in the Stacks Project.

AlgebraicGeometry.finiteLocallyConstantAbelianSheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FundamentalGroupLocallyConstant/Abelian.lean, line 69. The attribute's comment: “(2) finite locally constant sheaves of abelian groups are the finite π₁(X, x)-modules”.

Stacks Project, Tag 0DV5, part (2). For a connected scheme X with a geometric point x, the finite locally constant sheaves of abelian groups on X_étale are equivalent to the finite π₁(X, x)-modules, that is, to the finite abelian groups with a continuous action of the étale fundamental group.

Part (1) of the tag is AlgebraicGeometry.finiteLocallyConstantSetsEquivalence and part (3) is AlgebraicGeometry.finiteTypeLocallyConstantModuleSheafEquivalence.

public noncomputable def finiteLocallyConstantAbelianSheafEquivalence :
    (isFiniteLocallyConstantAbelianSheaf.{u, u + 1, u + 1}
        (SmallEtale.topology B X.1 X.2)).FullSubcategory ≌
      (ContinuousGAddCommGrp.isFinite.{u + 1, u + 1}
        (EtaleFundamentalGroup X.1 x)).FullSubcategory

AlgebraicGeometry.finiteTypeLocallyConstantModuleSheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FundamentalGroupLocallyConstant/Modules.lean, line 82. The attribute's comment: “(3) finite type locally constant sheaves of Λ-modules, for Λ a finite ring, are the finite π₁(X, x)-modules with commuting Λ-module structure”.

For a connected scheme X with a geometric point x and a finite ring Λ, the finite type locally constant sheaves of Λ-modules on X_étale are equivalent to the finite Λ-modules endowed with a commuting continuous action of π₁(X, x).

public def finiteTypeLocallyConstantModuleSheafEquivalence :
    ObjectProperty.FullSubcategory
        (fun F : Sheaf (SmallEtale.topology B X.1 X.2) (ModuleCat.{u + 1} Λ) ↦
          IsFiniteTypeLocallyConstant Λ (SmallEtale.topology B X.1 X.2) F) ≌
      FiniteTypeContinuousModule.{r, u + 1, u + 1} Λ (EtaleFundamentalGroup X.1 x)

AlgebraicGeometry.finiteLocallyConstantSetsEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FundamentalGroupLocallyConstant/Sets.lean, line 82. The attribute's comment: “(1) finite locally constant sheaves of sets are the finite continuous π₁(X, x)-sets”.

For a connected scheme X with a geometric point x, the equivalence between the finite locally constant sheaves of sets on the small étale site of X and the finite sets with a continuous action of the étale fundamental group π₁(X, x). It is finiteLocallyConstantFiniteEtaleEquivalence followed by finiteEtaleEquivalenceOfIsGaloisCategory and the change of universe contActionUniverseEquivalence.

public noncomputable def finiteLocallyConstantSetsEquivalence :
    FiniteLocallyConstantSheaf B X ≌
      ContAction FintypeCat.{u + 1} (EtaleFundamentalGroup X.1 x)
Tag 0GIY, a lemma

Tag 0GIY in the Stacks Project.

AlgebraicGeometry.finiteTypeLocallyConstantEquivContinuousModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/UnibranchContinuousModules.lean, line 368. The attribute's comment: “the equivalence, with the geometric input carried as hypotheses. Proved here: the source's reduction along the normalization — geometric unibranchness yields the universal homeomorphism of Tag 0GIQ, at which the hypothesis on the locally constant categories is instantiated; the fundamental group comparison is derived from the hypothesis that base change on finite étale covers along the normalization is an equivalence, which is the content of Tag 0BQN, by Tag 0BQA part (2); and the category of finite type continuous modules is transported along that comparison. Carried as hypotheses, none of them proved in this library: that base change on finite étale covers along a universal homeomorphism is an equivalence (Tag 0BQN, of which only faithfulness is available, the rest resting on Tag 0BTP), that a universal homeomorphism induces an equivalence of the finite type locally constant module categories (Tag 04DZ), the existence of a lift of the geometric point to the normalization, and the tag itself for the normalization, i.e. for an integral normal scheme (Tags 0BQM, 0BTD, 0BQI, 03RV, 0245, 03QW)”.

Stacks Project, Tag 0GIY. Let X be an irreducible, geometrically unibranch scheme, let x be a geometric point of X and let Λ be a ring. The finite type locally constant sheaves of Λ-modules on X_étale are equivalent to the finite Λ-modules endowed with a continuous π₁(X, x)-action.

The source proves this by reducing to the case of an integral normal scheme along the normalization ν : X^ν → X, which is a universal homeomorphism by Tag 0GIQ precisely because X is irreducible and geometrically unibranch. That reduction is what is carried out here: the geometric unibranchness is used to produce the universal homeomorphism, the equivalence of the finite type locally constant module categories of X and X^ν is instantiated at it, the isomorphism π₁(X^ν, x^ν) ≅ π₁(X, x) is obtained from the hypothesis that base change along ν is an equivalence of finite étale covers — the content of Tag 0BQN — through Tag 0BQA part (2), and the tag itself for the normalization is a hypothesis. See the module docstring for the gaps by tag number.

public def finiteTypeLocallyConstantEquivContinuousModule
    (B : BigEtaleSite.{u}) (X : B.Scheme) [IrreducibleSpace X.obj]
    (hX : IsGeometricallyUnibranch X.obj) (x : GeometricPoint X.obj)
    (Λ : Type r) [Ring Λ]
    [∀ V : SmallEtale B X.obj X.property,
      HasWeakSheafify ((SmallEtale.topology B X.obj X.property).over V) (ModuleCat.{w} Λ)]
    (hν : B.Contains (Scheme.normalizationSchemeOfIrreducible X.obj))
    [ConnectedSpace (Scheme.normalizationSchemeOfIrreducible X.obj)]
    [∀ V : SmallEtale B (Scheme.normalizationSchemeOfIrreducible X.obj) hν,
      HasWeakSheafify
        ((SmallEtale.topology B (Scheme.normalizationSchemeOfIrreducible X.obj) hν).over V)
        (ModuleCat.{w} Λ)]
    [(finiteEtaleBaseChange (Scheme.normalizationOfIrreducible X.obj)).IsEquivalence]
    (xν : GeometricPoint (Scheme.normalizationSchemeOfIrreducible X.obj))
    (hx : xν.map (Scheme.normalizationOfIrreducible X.obj) = x)
    (hinvariance : UniversalHomeomorphism (Scheme.normalizationOfIrreducible X.obj) →
      (FiniteTypeLocallyConstantModuleCategory Λ (SmallEtale.topology B X.obj X.property) ≌
        FiniteTypeLocallyConstantModuleCategory Λ
          (SmallEtale.topology B (Scheme.normalizationSchemeOfIrreducible X.obj) hν)))
    (hnormal : FiniteTypeLocallyConstantModuleCategory Λ
        (SmallEtale.topology B (Scheme.normalizationSchemeOfIrreducible X.obj) hν) ≌
      FiniteTypeContinuousModule Λ
        (EtaleFundamentalGroup (Scheme.normalizationSchemeOfIrreducible X.obj) xν)) :
    FiniteTypeLocallyConstantModuleCategory Λ (SmallEtale.topology B X.obj X.property) ≌
      FiniteTypeContinuousModule Λ (EtaleFundamentalGroup X.obj x)

AlgebraicGeometry.finiteTypeLocallyConstantEquivContinuousModuleUniv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/UnibranchEquivalence.lean, line 73.

Stacks Project, Tag 0GIY. Let X be an irreducible, geometrically unibranch scheme, let x be a geometric point of X and let Λ be a ring. The finite type locally constant sheaves of Λ-modules on X_étale are equivalent to the finite Λ-modules endowed with a continuous π₁(X, x)-action.

The functor sends a sheaf F to its monodromy module colim_{(A, a)} F(A) over the pointed Galois covers of X.

public def finiteTypeLocallyConstantEquivContinuousModuleUniv (X : Scheme.{u}) [IrreducibleSpace X]
    (hX : IsGeometricallyUnibranch X) (x : GeometricPoint X) (Λ : Type r) [Ring Λ] :
    Stacks.ConstantSheaf.FiniteTypeLocallyConstantModuleCategory.{max (u + 1) r, u + 1, u, r} Λ
        X.smallEtaleTopology ≌
      Stacks.GroupCohomology.FiniteTypeContinuousModule.{r, u + 1, max (u + 1) r} Λ
        (EtaleFundamentalGroup X x)
Tag 0DV6, a remark

Tag 0DV6 in the Stacks Project.

AlgebraicGeometry.finiteSmallEtaleToFiniteLocallyConstantBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/BaseChangeRepresentable.lean, line 199. The attribute's comment: “the sets case, first leg: the dictionary of Stacks 03RV between the finite objects of the small etale site and the finite locally constant sheaves of sets commutes with pullback. The second leg, Stacks 0BND (3), is proved separately as AlgebraicGeometry.exists_finiteEtaleEquivalence_mapIso; the two legs are not composed here, which would need the comparison of AlgebraicGeometry.finiteSmallEtaleBaseChange with AlgebraicGeometry.finiteEtaleBaseChange across AlgebraicGeometry.finiteEtaleSiteEquivalence”.

Stacks Project, Tag 0DV6, the first leg of the sets case. The inverse image of the finite locally constant sheaf represented by a finite étale cover is the one represented by its base change: the square of AlgebraicGeometry.finiteSmallEtaleToFiniteLocallyConstant against base change on the site and inverse image on sheaves commutes.

The equivalence of Tag 0DV5 (1) between the finite locally constant sheaves of sets on X_étale and the finite continuous π₁(X, x)-sets is the composite of two legs, the dictionary of Tag 03RV with finite étale covers and the equivalence of Tag 0BND (1). This is the compatibility of the first leg with pullbacks.

public def finiteSmallEtaleToFiniteLocallyConstantBaseChangeIso :
    finiteSmallEtaleToFiniteLocallyConstant B X ⋙ finiteLocallyConstantSheafPullback B f ≅
      finiteSmallEtaleBaseChange B f ⋙ finiteSmallEtaleToFiniteLocallyConstant B Y

AlgebraicGeometry.nonempty_finiteLocallyConstantSetsEquivalence_pullbackIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/BaseChangeRepresentable.lean, line 281. The attribute's comment: “for sheaves of sets: the equivalence of Stacks 0DV5 (1) commutes with pullback, the action being reindexed along the induced homomorphism of fundamental groups”.

Stacks Project, Tag 0DV6 for sheaves of sets. Let f : Y ⟶ X be a morphism of connected schemes and let y be a geometric point of Y, with image x = f(y). Then the square

  finite locally constant sheaves of sets on X_étale  ──→  finite π₁(X, x)-sets
                        │                                          │
                     f^{-1}                                   restriction
                        ↓                                          ↓
  finite locally constant sheaves of sets on Y_étale  ──→  finite π₁(Y, y)-sets

commutes, where the horizontal arrows are the equivalence of Stacks Tag 0DV5 (1) and the right vertical arrow reindexes the action along the homomorphism π₁(Y, y) ⟶ π₁(X, x) induced by f.

The equivalence of Tag 0DV5 (1) is the composite of the dictionary of Tag 03RV with the finite étale covers, the equivalence of Tag 0BND (1) and a change of universe. The first factor commutes with pullback by AlgebraicGeometry.finiteLocallyConstantFiniteEtaleEquivalenceBaseChangeIso, the second by Tag 0BND (3), that is AlgebraicGeometry.exists_finiteEtaleEquivalence_mapIso, and the third on the nose. Only the existence of the comparison is asserted, because Tag 0BND (3) is available in that form.

public theorem nonempty_finiteLocallyConstantSetsEquivalence_pullbackIso
    [ConnectedSpace X.1] [ConnectedSpace Y.1] (y : GeometricPoint Y.1) :
    Nonempty ((finiteLocallyConstantSetsEquivalence B X (y.map f.hom)).functor ⋙
        ContAction.res FintypeCat.{u + 1} (etaleFundamentalGroupMap f.hom y) ≅
      finiteLocallyConstantSheafPullback B f ⋙
        (finiteLocallyConstantSetsEquivalence B Y y).functor)

AlgebraicGeometry.nonempty_finiteLocallyConstantAbelianSheafEquivalence_pullbackIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/BaseChangeRepresentable.lean, line 392. The attribute's comment: “for sheaves of abelian groups: the equivalence of Stacks 0DV5 (2) commutes with pullback, the action being reindexed along the induced homomorphism of fundamental groups”.

Stacks Project, Tag 0DV6 for sheaves of abelian groups. Let f : Y ⟶ X be a morphism of connected schemes and let y be a geometric point of Y, with image x = f(y). Then the square

  finite locally constant abelian sheaves on X_étale  ──→  finite π₁(X, x)-modules
                        │                                          │
                     f^{-1}                                   restriction
                        ↓                                          ↓
  finite locally constant abelian sheaves on Y_étale  ──→  finite π₁(Y, y)-modules

commutes, where the horizontal arrows are the equivalence of Stacks Tag 0DV5 (2), the left vertical arrow is the inverse image of abelian sheaves (AlgebraicGeometry.finiteLocallyConstantAbelianSheafPullback_comp_ι) and the right vertical arrow reindexes the action along the homomorphism π₁(Y, y) ⟶ π₁(X, x) induced by f (CategoryTheory.ContinuousGAddCommGrp.resIsFinite_comp_ι).

The equivalence of Tag 0DV5 (2) is the transport of commutative group objects along the equivalence of Tag 0DV5 (1), and the only factor of that transport which depends on the latter is CategoryTheory.Functor.mapCommGrp applied to it, so the sets case of Tag 0DV6 transports: Stacks.ConstantSheaf.finiteLocallyConstantAbelianPullbackSquare. Its two remaining inputs are the compatibility of each dictionary with the two vertical arrows, and for the sheaf side that is the identification of the inverse image of abelian sheaves with the inverse image of the underlying sheaves of sets together with the induced group operations, Stacks.Sites.AbelianPullback.internalSheafPullbackSquare. Only the existence of the comparison is asserted, because the sets case is available in that form.

public theorem nonempty_finiteLocallyConstantAbelianSheafEquivalence_pullbackIso
    [ConnectedSpace X.1] [ConnectedSpace Y.1] (y : GeometricPoint Y.1) :
    Nonempty ((finiteLocallyConstantAbelianSheafEquivalence B X (y.map f.hom)).functor ⋙
        ContinuousGAddCommGrp.resIsFinite (etaleFundamentalGroupMap f.hom y) ≅
      finiteLocallyConstantAbelianSheafPullback B f ⋙
        (finiteLocallyConstantAbelianSheafEquivalence B Y y).functor)

AlgebraicGeometry.nonempty_finiteTypeLocallyConstantModuleSheafEquivalence_pullbackIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/BaseChangeRepresentable.lean, line 551. The attribute's comment: “for sheaves of modules over a finite ring: the equivalence of Stacks 0DV5 (3) commutes with pullback, the action being reindexed along the induced homomorphism of fundamental groups”.

Stacks Project, Tag 0DV6 for sheaves of modules. Let Λ be a finite ring, let f : Y ⟶ X be a morphism of connected schemes and let y be a geometric point of Y, with image x = f(y). Then the square

  finite type locally constant Λ-module sheaves on X_étale  ──→  finite Λ-π₁(X, x)-modules
                        │                                                 │
                     f^{-1}                                          restriction
                        ↓                                                 ↓
  finite type locally constant Λ-module sheaves on Y_étale  ──→  finite Λ-π₁(Y, y)-modules

commutes, where the horizontal arrows are the equivalence of Stacks Tag 0DV5 (3), the left vertical arrow is the inverse image of sheaves of Λ-modules (AlgebraicGeometry.finiteTypeLocallyConstantModuleSheafPullback_comp_ι) and the right vertical arrow reindexes the action along the homomorphism π₁(Y, y) ⟶ π₁(X, x) induced by f (Stacks.GroupCohomology.finiteTypeContinuousModuleRes_comp_ι together with Stacks.GroupCohomology.continuousModuleRes_comp_ι).

The equivalence of Tag 0DV5 (3) is the equivalence of Tag 0DV5 (2) read on additive functors out of the one-object category of Λ, and the only factor of that reading which depends on the latter is postcomposition with it, so the abelian case of Tag 0DV6 transports: CategoryTheory.scalarActionTransportSquare. Only the existence of the comparison is asserted, because the abelian case is available in that form.

public theorem nonempty_finiteTypeLocallyConstantModuleSheafEquivalence_pullbackIso
    (y : GeometricPoint Y.1) :
    Nonempty ((finiteTypeLocallyConstantModuleSheafEquivalence B X (y.map f.hom) Λ).functor ⋙
        finiteTypeContinuousModuleRes Λ (etaleFundamentalGroupMap f.hom y) ≅
      finiteTypeLocallyConstantModuleSheafPullback B f Λ ⋙
        (finiteTypeLocallyConstantModuleSheafEquivalence B Y y Λ).functor)

AlgebraicGeometry.finiteTypeLocallyConstantEquivContinuousModuleUnivPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteLocallyConstant/BaseChangeUnibranch.lean, line 542. The attribute's comment: “the square for the equivalence of Stacks 0GIY; the squares for the equivalences of Stacks 0DV5 are in BaseChangeRepresentable and BaseChangeEtaleSite”.

Stacks Project, Tag 0DV6, for the equivalence of Tag 0GIY. Let f : Y ⟶ X be a morphism of irreducible, geometrically unibranch schemes, let y be a geometric point of Y and let Λ be a ring. The equivalences of Tag 0GIY for X at f(y) and for Y at y are compatible with pullback: the square

  finite type loc. const. Λ-module sheaves on X_étale  ──→  finite Λ-π₁(X, f(y))-modules
                      │                                               │
                   f^{-1}                                        restriction
                      ↓                                               ↓
  finite type loc. const. Λ-module sheaves on Y_étale  ──→  finite Λ-π₁(Y, y)-modules

commutes up to the natural isomorphism given here, the right-hand vertical arrow restricting the action along the homomorphism π₁(Y, y) ⟶ π₁(X, f(y)) of Tag 0BND (3).

The comparison sends the image of a section s over a pointed Galois cover A of X to the image of the restriction of f^{-1}s to a pointed Galois cover of Y dominating A ×_X Y; it is bijective because f^{-1} carries a trivialization of F over A to one of f^{-1}F over A ×_X Y, compatibly with the sections.

public def finiteTypeLocallyConstantEquivContinuousModuleUnivPullbackIso :
    (finiteTypeLocallyConstantEquivContinuousModuleUniv X hX (y.map f) Λ).functor ⋙
        finiteTypeContinuousModuleRes Λ (etaleFundamentalGroupMap f y) ≅
      etaleFiniteTypeLocallyConstantModulePullback f Λ ⋙
        (finiteTypeLocallyConstantEquivContinuousModuleUniv Y hY y Λ).functor
Sources
LeanAlgebraicGeometry.finiteLocallyConstantAbelianSheafEquivalence · AlgebraicGeometry.finiteTypeLocallyConstantModuleSheafEquivalence · AlgebraicGeometry.finiteLocallyConstantSetsEquivalence · AlgebraicGeometry.finiteTypeLocallyConstantEquivContinuousModule · AlgebraicGeometry.finiteTypeLocallyConstantEquivContinuousModuleUniv · AlgebraicGeometry.finiteSmallEtaleToFiniteLocallyConstantBaseChangeIso · AlgebraicGeometry.nonempty_finiteLocallyConstantSetsEquivalence_pullbackIso · AlgebraicGeometry.nonempty_finiteLocallyConstantAbelianSheafEquivalence_pullbackIso

Section59.66 Méthode de la trace#

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

Tag 03SH, the section

Tag 03SH in the Stacks Project.

Stacks.EtaleCohomology.mono_etaleModuleCohomology_map_unit_of_finiteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleTraceCohomology.lean, line 78. The attribute's comment: “the méthode de la trace: H^n(X, F) → H^n(Y, f⁻¹F) is injective when multiplication by the degree is an isomorphism of F”. References: SGA 5 IIIB (3.2), “partial”.

Stacks 03SH, the méthode de la trace. For f : T ⟶ S finite étale of degree d and a sheaf of Λ-modules F on which multiplication by d is an isomorphism, the map H^n(S, F) ⟶ H^n(T, f⁻¹ F) — induced by the restriction F ⟶ f_* f⁻¹ F, followed by the identification H^n(S, f_* f⁻¹ F) = H^n(T, f⁻¹ F) — is injective: the restriction has a left inverse, the trace divided by d.

theorem mono_etaleModuleCohomology_map_unit_of_finiteEtale [IsIso (d • 𝟙 F)] (n : ℕ) :
    Mono (((etaleModuleGlobalSections.{u, r} Λ S).rightDerived n).map
        ((etaleModuleInverseImageAdj.{u, r} Λ f).unit.app F) ≫
      (etaleModuleCohomologyDirectImageIsoOfIsIntegralHom Λ f n
        ((etaleModuleInverseImage.{u, r} Λ f).obj F)).hom)

Stacks.EtaleCohomology.isZero_etaleModuleCohomology_of_finiteEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleTraceCohomology.lean, line 96. The attribute's comment: “if H^q(Y, f⁻¹F) = 0 then H^q(X, F) = 0, when multiplication by the degree is an isomorphism of F”.

Stacks 03SH, the vanishing consequence of the méthode de la trace. For f : T ⟶ S finite étale of degree d and a sheaf of Λ-modules F on which multiplication by d is an isomorphism, H^q(T, f⁻¹ F) = 0 implies H^q(S, F) = 0.

theorem isZero_etaleModuleCohomology_of_finiteEtale [IsIso (d • 𝟙 F)] (q : ℕ)
    (h : IsZero (((etaleModuleGlobalSections.{u, r} Λ T).rightDerived q).obj
      ((etaleModuleInverseImage.{u, r} Λ f).obj F))) :
    IsZero (((etaleModuleGlobalSections.{u, r} Λ S).rightDerived q).obj F)

AlgebraicGeometry.moduleTrace_app_eq_sum_of_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleTraceDegree.lean, line 142. The attribute's comment: “if Y is a disjoint union of copies of the base, the trace is the sum map, for sheaves of Λ-modules”.

Stacks 03SH, the trace on a split cover is the sum map. If over the étale object Q of T the morphism f is described by the pairwise disjoint morphisms φ i : Q ⟶ T' whose graphs cover Q ×_T T', so that (f_* f^{-1} ℱ)(Q) = ℱ(Q ×_T T') = ⨁ᵢ ℱ(Q), then the trace sends a section to the sum of its restrictions to the sheets φ i, each read on Q.

theorem moduleTrace_app_eq_sum_of_cover
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (ModuleCat.{max (u + 1) v} Λ))
    (Q : SmallEtale B T.1 T.property) {ι : Type u} [Fintype ι]
    (φ : ι → (Q ⟶ SmallEtale.ofEtaleHom B f))
    (hcov : ∀ z : ((smallEtaleBaseChange B (SmallEtale.ofEtaleHom B f).obj.hom).obj Q).obj.left.1,
      ∃ i, z ∈ Set.range (B.inclusion.map
        (smallEtaleLiftGraph B T.1 T.property (SmallEtale.ofEtaleHom B f) Q (φ i)).hom.left))
    (hd : Pairwise (fun i j => smallEtaleArrowsDisjoint B T.1 T.property
      (SmallEtale.ofEtaleHom B f) Q (φ i) (φ j)))
    (s : F.obj.obj (op ((smallEtalePostcompose B T.1 T.property (SmallEtale.ofEtaleHom B f)).obj
      ((smallEtaleBaseChange B (SmallEtale.ofEtaleHom B f).obj.hom).obj Q)))) :
    ((moduleTrace B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).app F).hom.app (op Q) s =
      ∑ i, F.obj.map (smallEtaleLiftPostIso B T.1 T.property (SmallEtale.ofEtaleHom B f) Q
        (φ i)).inv.op
        (((moduleRestriction B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).obj F).obj.map
          (smallEtaleLiftGraph B T.1 T.property (SmallEtale.ofEtaleHom B f) Q (φ i)).op s)

AlgebraicGeometry.eq_moduleTrace_app_of_sum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleTraceDegree.lean, line 210. The attribute's comment: “the trace is characterized by being the sum map étale locally on the base, for sheaves of Λ-modules”.

Stacks 03SH, the trace is characterized by the sum formula. A morphism τ : f_* f^{-1} ℱ ⟶ ℱ which, over every étale neighbourhood Q on which f is a disjoint union of copies of Q (pairwise disjoint sheets φ i : Q ⟶ T' whose graphs cover Q ×_T T'), sends a section to the sum of its restrictions to the sheets is the trace: such neighbourhoods cover T (Stacks 04HN), and two morphisms of sheaves agreeing on a covering agree.

theorem eq_moduleTrace_app_of_sum
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (ModuleCat.{max (u + 1) v} Λ))
    (τ : (B.smallPushforward f (ModuleCat.{max (u + 1) v} Λ)).obj
      ((moduleRestriction B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).obj F) ⟶ F)
    (hτ : ∀ (Q : SmallEtale B T.1 T.property) {ι : Type u} [Fintype ι]
      (φ : ι → (Q ⟶ SmallEtale.ofEtaleHom B f)),
      (∀ z : ((smallEtaleBaseChange B (SmallEtale.ofEtaleHom B f).obj.hom).obj Q).obj.left.1,
        ∃ i, z ∈ Set.range (B.inclusion.map
          (smallEtaleLiftGraph B T.1 T.property (SmallEtale.ofEtaleHom B f) Q (φ i)).hom.left)) →
      Pairwise (fun i j => smallEtaleArrowsDisjoint B T.1 T.property
        (SmallEtale.ofEtaleHom B f) Q (φ i) (φ j)) →
      ∀ s : F.obj.obj (op ((smallEtalePostcompose B T.1 T.property (SmallEtale.ofEtaleHom B f)).obj
        ((smallEtaleBaseChange B (SmallEtale.ofEtaleHom B f).obj.hom).obj Q))),
      τ.hom.app (op Q) s =
        ∑ i, F.obj.map (smallEtaleLiftPostIso B T.1 T.property (SmallEtale.ofEtaleHom B f) Q
          (φ i)).inv.op
          (((moduleRestriction B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).obj F).obj.map
            (smallEtaleLiftGraph B T.1 T.property (SmallEtale.ofEtaleHom B f) Q (φ i)).op s)) :
    τ = (moduleTrace B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).app F

AlgebraicGeometry.unit_comp_moduleTrace_eq_nsmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/ModuleTraceDegree.lean, line 257. The attribute's comment: “restriction followed by the trace is multiplication by the degree, for sheaves of Λ-modules”. References: SGA 4 XVII (6.2.3), “Var 4 (normalization)”; SGA 4 XVIII (2.9), “Var 4 (I)”.

Stacks 03SH, the trace of a finite étale morphism of degree d on sheaves of modules. For f finite étale and finite locally free of rank d, the restriction map ℱ ⟶ f_* f^{-1} ℱ (the unit of f^{-1} ⊣ f_*) followed by the trace f_* f^{-1} ℱ ⟶ ℱ of Definition 03SE is multiplication by d.

theorem unit_comp_moduleTrace_eq_nsmul (d : ℕ)
    [Stacks.Morphisms.IsFiniteLocallyFreeOfRank (B.inclusion.map f) d]
    (F : Sheaf (SmallEtale.topology B T.1 T.property) (ModuleCat.{max (u + 1) v} Λ)) :
    (smallEtalePostcomposePushforwardAdjunction B f
        (ModuleCat.{max (u + 1) v} Λ)).unit.app F ≫
        (moduleTrace B T.1 T.property (SmallEtale.ofEtaleHom B f) Λ).app F = d • 𝟙 F
Tag 03SE, a definition

Tag 03SE in the Stacks Project.

AlgebraicGeometry.abelianTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Trace.lean, line 114. The attribute's comment: “abelian sheaves”.

Stacks 03SE. The trace map of the finite étale morphism U ⟶ X on abelian étale sheaves: the counit j_!j^{-1} ⟶ id of the extension-by-zero adjunction, read as a map j_*j^{-1} ⟶ id through the comparison isomorphism j_! ≅ j_* of Stacks 03S7.

public def abelianTrace :
    let := smallEtaleBaseChange_isContinuous B U.obj.hom
    abelianRestriction B X hX U ⋙
        (smallEtaleBaseChange B U.obj.hom).sheafPushforwardContinuous
          AddCommGrpCat.{u + 1}
          (SmallEtale.topology B X hX)
          (SmallEtale.topology B U.obj.left.1 U.obj.left.property) ⟶
      𝟭 (Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u + 1})

AlgebraicGeometry.moduleTrace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ExtensionByZeroBaseChange/Trace.lean, line 216. The attribute's comment: “sheaves of modules”.

Stacks 03SE. The trace map of the finite étale morphism U ⟶ X on étale sheaves of Λ-modules, constructed exactly as in the abelian case.

public def moduleTrace :
    let := smallEtaleBaseChange_isContinuous B U.obj.hom
    moduleRestriction B X hX U Λ ⋙
        (smallEtaleBaseChange B U.obj.hom).sheafPushforwardContinuous
          (ModuleCat.{max (u + 1) v} Λ)
          (SmallEtale.topology B X hX)
          (SmallEtale.topology B U.obj.left.1 U.obj.left.property) ⟶
      𝟭 (Sheaf (SmallEtale.topology B X hX) (ModuleCat.{max (u + 1) v} Λ))
Tag 0A3R, a lemma

Tag 0A3R in the Stacks Project.

Stacks.EtaleCohomology.exists_primeToEll_finiteEtale_constantFiltration_unconditional, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/PrimeToEllCover.lean, line 806.

Stacks Project, Tag 0A3R. Let S be a connected scheme, let ℓ be a prime number and let F be a finite type locally constant sheaf of F_ℓ-vector spaces on S_étale. Then there is a finite étale morphism f : T → S of degree prime to ℓ such that f⁻¹F has a finite filtration whose successive quotients are the constant sheaf Z/ℓZ_T.

The filtration is a chain of subobjects of f⁻¹F running from the zero subobject to the whole sheaf, each step having the constant sheaf as its quotient. The local constancy of F enters through the dictionary of Tag 0DV5 (3), which is Stacks.EtaleCohomology.nonempty_fundamentalGroupFGModuleDictionary.

The dictionary is read at a geometric point, which the statement does not mention: a connected space is nonempty, and AlgebraicGeometry.GeometricPoint.ofPoint puts a geometric point of S above any of its points, so one is produced inside the proof rather than assumed. NeZero ℓ, which the dictionary needs for the finiteness of F_ℓ[K], comes from the primality of ℓ likewise.

theorem exists_primeToEll_finiteEtale_constantFiltration_unconditional {ℓ : ℕ} (hℓ : ℓ.Prime)
    {S : Scheme.{u}} [ConnectedSpace S]
    (F : Sheaf (smallEtaleTopology S) (ModuleCat.{max (u + 1) v} (ZMod ℓ)))
    (_hF : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant (ZMod ℓ) (smallEtaleTopology S) F) :
    ∃ (T : Scheme.{u}) (f : T ⟶ S) (d : ℕ), IsFinite f ∧ Etale f ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d ∧ ¬ ℓ ∣ d ∧
      ∃ X : RelSeries (ConstantRankOneStep ℓ ((smallEtalePullbackZMod ℓ f).obj F)),
        IsZero (Subobject.underlying.obj X.head) ∧ IsIso X.last.arrow

Stacks.EtaleCohomology.exists_primeToEll_finiteEtale_relSeries_constantRankOneStep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/PrimeToEllFiltration.lean, line 389.

Stacks Project, Tag 0A3R. Let S be a connected scheme, ℓ a prime number and F a finite type locally constant sheaf of F_ℓ-vector spaces on S_étale. Then there is a finite étale morphism f : T → S of degree prime to ℓ such that f⁻¹F has a finite filtration whose successive quotients are isomorphic to Z/ℓZ_T.

The filtration is a chain of subobjects of f⁻¹F running from the zero subobject to the whole sheaf, each step having the constant sheaf Z/ℓZ_T as its quotient.

theorem exists_primeToEll_finiteEtale_relSeries_constantRankOneStep {ℓ : ℕ} (hℓ : ℓ.Prime)
    {S : Scheme.{u}} [ConnectedSpace S]
    (F : Sheaf S.smallEtaleTopology (ModuleCat.{u + 1} (ZMod ℓ)))
    (hF : IsFiniteTypeLocallyConstant (ZMod ℓ) S.smallEtaleTopology F) :
    ∃ (T : Scheme.{u}) (f : T ⟶ S) (d : ℕ), IsFinite f ∧ Etale f ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d ∧ ¬ ℓ ∣ d ∧
      ∃ X : RelSeries (ConstantRankOneStep.{0} ℓ ((smallEtalePullbackZMod.{0} ℓ f).obj F)),
        IsZero (Subobject.underlying.obj X.head) ∧ IsIso X.last.arrow
Tag 0GIZ, a lemma

Tag 0GIZ in the Stacks Project.

Module.exists_relSeries_trivial_action_subquotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/PGroupFiltration.lean, line 384. References: SGA 5 I (App.1.3.1), “trivial action quotients”.

A module over the group ring of a finite ℓ-group, annihilated by a power of ℓ, has a finite filtration by group-ring submodules with trivial group action on every successive quotient.

theorem Module.exists_relSeries_trivial_action_subquotient
    (Λ H M : Type*) [CommRing Λ] [Group H] [Finite H]
    (ℓ n : ℕ) (hℓ : ℓ.Prime) (hH : IsPGroup ℓ H)
    [AddCommGroup M] [Module (MonoidAlgebra Λ H) M]
    (hM : ∀ x : M, (ℓ ^ n) • x = 0) :
    ∃ X : RelSeries {p : Submodule (MonoidAlgebra Λ H) M ×
        Submodule (MonoidAlgebra Λ H) M |
      p.1 ≤ p.2 ∧ ∀ (g : H) (x : p.2),
        MonoidAlgebra.single g (1 : Λ) • (x : M) - x ∈ p.1},
      X.head = ⊥ ∧ X.last = ⊤
Tag 0GJ0, a lemma

Tag 0GJ0 in the Stacks Project.

Stacks.EtaleCohomology.exists_primeToEll_finiteEtale_finiteModuleFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/ConstantModuleFiltration.lean, line 563. The attribute's comment: “granted hypothesis D, the Stacks 0GIY dictionary in finite-module form”.

Stacks Project, Tag 0GJ0. Let S be an irreducible, geometrically unibranch scheme, let ℓ be a prime number, let n ≥ 1, let Λ be a Noetherian ring and let F be a finite type locally constant sheaf of Λ-modules on S_étale annihilated by ℓ ^ n. Then there is a finite étale morphism f : T → S of degree prime to ℓ such that f⁻¹F has a finite filtration whose successive quotients are of the form M_T for finite Λ-modules M.

The filtration is a chain of subobjects of f⁻¹F running from the zero subobject to the whole sheaf, each step having the constant sheaf of a finite Λ-module as its quotient.

The irreducibility and geometric unibranchness of S and the local constancy of F are the hypotheses under which the dictionary D of Stacks Tag 0GIY is available. The annihilation of F by ℓ ^ n is stated twice: on the sections of F, as _hann, because the source states it there, and on the module the dictionary attaches to F, as the field D.annihilated, because that is the form Tag 0GIZ consumes. Transporting the first to the second is part of Tag 0GIY and so is part of what D carries; nothing here derives one from the other.

theorem exists_primeToEll_finiteEtale_finiteModuleFiltration {ℓ n : ℕ} (hℓ : ℓ.Prime)
    (_hn : 1 ≤ n) {Λ : Type v} [CommRing Λ] [IsNoetherianRing Λ]
    {S : Scheme.{u}} [IrreducibleSpace S] (_hS : IsGeometricallyUnibranch S)
    (s : GeometricPoint S)
    (F : Sheaf (smallEtaleTopology S) (ModuleCat.{max (u + 1) v} Λ))
    (_hF : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant Λ (smallEtaleTopology S) F)
    (_hann : ∀ (U : S.Etale) (x : F.obj.obj (Opposite.op U)), (ℓ ^ n) • x = 0)
    (D : FiniteModuleMonodromyDictionary Λ ℓ n s F) :
    ∃ (T : Scheme.{u}) (f : T ⟶ S) (d : ℕ), IsFinite f ∧ Etale f ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d ∧ ¬ ℓ ∣ d ∧
      ∃ X : RelSeries (ConstantFiniteModuleStep Λ
          ((smallEtalePullbackModuleCat Λ f).obj F)),
        IsZero (Subobject.underlying.obj X.head) ∧ IsIso X.last.arrow

Stacks.EtaleCohomology.exists_primeToEll_finiteEtale_finiteModuleFiltration_general, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/ConstantModuleFiltrationUnconditional.lean, line 234.

Stacks Project, Tag 0GJ0. Let S be an irreducible, geometrically unibranch scheme, let ℓ be a prime number, let n ≥ 1, let Λ be a Noetherian ring and let F be a finite type locally constant sheaf of Λ-modules on S_étale annihilated by ℓ ^ n. Then there is a finite étale morphism f : T → S of degree prime to ℓ such that f⁻¹F has a finite filtration whose successive quotients are of the form M_T for finite Λ-modules M.

The filtration is a chain of subobjects of f⁻¹F running from the zero subobject to the whole sheaf, each step having the constant sheaf of a finite Λ-module as its quotient. The degree of f is the rank of the finite locally free morphism f (Tag 02KA).

theorem exists_primeToEll_finiteEtale_finiteModuleFiltration_general {ℓ n : ℕ} (hℓ : ℓ.Prime)
    (_hn : 1 ≤ n) {Λ : Type v} [CommRing Λ] [IsNoetherianRing Λ]
    {S : Scheme.{u}} [IrreducibleSpace S] (hS : IsGeometricallyUnibranch S)
    (s : GeometricPoint S)
    (F : Sheaf (smallEtaleTopology S) (ModuleCat.{max (u + 1) v} Λ))
    (hF : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant Λ (smallEtaleTopology S) F)
    (hann : ∀ (U : S.Etale) (x : F.obj.obj (Opposite.op U)), (ℓ ^ n) • x = 0) :
    ∃ (T : Scheme.{u}) (f : T ⟶ S) (d : ℕ), IsFinite f ∧ Etale f ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d ∧ ¬ ℓ ∣ d ∧
      ∃ X : RelSeries (ConstantFiniteModuleStep Λ
          ((smallEtalePullbackModuleCat Λ f).obj F)),
        IsZero (Subobject.underlying.obj X.head) ∧ IsIso X.last.arrow

Stacks.EtaleCohomology.exists_finiteEtale_primeToEll_constantModuleFiltration, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MethodeDeLa/UnibranchConstantModuleFiltration.lean, line 275. The attribute's comment: “the filtration after a finite étale cover of degree prime to ℓ, for S irreducible and geometrically unibranch”.

Stacks, Tag 0GJ0. Let S be an irreducible, geometrically unibranch scheme, let ℓ be a prime number and n ≥ 1, let Λ be a Noetherian ring and let F be a finite type, locally constant sheaf of Λ-modules on S_étale annihilated by ℓ ^ n. Then there is a finite étale morphism f : T ⟶ S of degree d prime to ℓ such that f⁻¹ F has a finite filtration whose successive quotients are of the form M̲_T for finite Λ-modules M.

The filtration is a chain of subobjects of f⁻¹ F from the zero subobject to the whole sheaf, each step having the constant sheaf of a finite Λ-module as its quotient. The degree is the rank d of f as a finite locally free morphism.

The unibranch hypothesis of the source is necessary: it cannot be dropped even for S irreducible (a fortiori it cannot be replaced by connectedness). Let S be the nodal cubic over an algebraically closed field k: it is irreducible but not geometrically unibranch at the node, and its étale fundamental group is ℤ̂. It is ℙ¹_k with 0 and ∞ glued, and the infinite chain of copies of ℙ¹_k, the i-th glued at ∞ to the (i+1)-st at 0, is an étale covering S̃ ⟶ S with deck group ℤ. Let Λ = 𝔽_ℓ[t, t⁻¹], a Noetherian domain annihilated by ℓ, and let F = S̃ ×^ℤ Λ be the sheaf of Λ-modules obtained by letting the generator of ℤ act on Λ by multiplication by t. It is locally constant (constant on S̃), of finite type (stalks Λ) and annihilated by ℓ. For every finite étale f : T ⟶ S and every connected component T₀ of T (a cycle of m ≥ 1 copies of ℙ¹_k), the pullback of S̃ to T₀ is the ℤ-cover with monodromy m, so Γ(T₀, f⁻¹ F) = {v ∈ Λ | t ^ m v = v} = 0, t ^ m - 1 being a nonzero divisor. A constant subsheaf M̲_{T₀} of f⁻¹ F|_{T₀} therefore has M ⊆ Γ(T₀, M̲) = 0; by induction along a filtration with constant successive quotients every term restricted to T₀ is 0, while f⁻¹ F|_{T₀} has stalks Λ ≠ 0. So the conclusion fails for every finite étale f.

theorem exists_finiteEtale_primeToEll_constantModuleFiltration {ℓ n : ℕ} (hℓ : ℓ.Prime)
    (_hn : 1 ≤ n) {Λ : Type r} [CommRing Λ] [IsNoetherianRing Λ]
    {S : Scheme.{u}} [IrreducibleSpace S] (hS : IsGeometricallyUnibranch S)
    (F : EtaleModules.{u, r} Λ S)
    (hF : Stacks.ConstantSheaf.IsFiniteTypeLocallyConstant Λ S.smallEtaleTopology F)
    (hann : ∀ (U : S.Etale) (y : F.obj.obj (op U)), (ℓ ^ n) • y = 0) :
    ∃ (T : Scheme.{u}) (f : T ⟶ S) (d : ℕ), IsFinite f ∧ Etale f ∧
      Stacks.Morphisms.IsFiniteLocallyFreeOfRank f d ∧ ¬ ℓ ∣ d ∧
      ∃ X : RelSeries (ConstantFiniteModuleStep Λ ((etaleModuleInverseImage.{u, r} Λ f).obj F)),
        IsZero (Subobject.underlying.obj X.head) ∧ IsIso X.last.arrow
Sources
LeanStacks.EtaleCohomology.mono_etaleModuleCohomology_map_unit_of_finiteEtale · Stacks.EtaleCohomology.isZero_etaleModuleCohomology_of_finiteEtale · AlgebraicGeometry.moduleTrace_app_eq_sum_of_cover · AlgebraicGeometry.eq_moduleTrace_app_of_sum · AlgebraicGeometry.unit_comp_moduleTrace_eq_nsmul · AlgebraicGeometry.abelianTrace · AlgebraicGeometry.moduleTrace · Stacks.EtaleCohomology.exists_primeToEll_finiteEtale_constantFiltration_unconditional

Section59.67 Galois cohomology#

Section 59.67 of the Stacks Project, Tag 0A2M. 12 tags here are carried by 22 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DV7, a lemma

Tag 0DV7 in the Stacks Project.

Stacks.EtaleCohomology.isPrimePowerTorsion_nontrivial_sheafH_smallEtalePushforwardAb_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/FiniteEtaleLimit.lean, line 104. The attribute's comment: “given F on X, take G = g_* F”.

[Stacks, Tag 0DV7], from the limit to the base. For a directed limit X = lim Xᵢ of schemes finite over S, an ℓ-power torsion sheaf F on X with Hⁿ(X, F) ≠ 0 gives the ℓ-power torsion sheaf g_* F on S with Hⁿ(S, g_* F) ≠ 0.

theorem isPrimePowerTorsion_nontrivial_sheafH_smallEtalePushforwardAb_of_isLimit
    [IsDirected I (· ≤ ·)] [Nonempty I] [∀ i, IsFinite (ι i)] (hc : IsLimit c) {ℓ : ℕ}
    {F : Sheaf (smallEtaleTopology c.pt) Ab.{u + 1}}
    (hF : Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology c.pt) ℓ F) {n : ℕ}
    (hn : Nontrivial (Sheaf.H.{u + 1} F n)) :
    Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology S) ℓ
        ((smallEtalePushforwardAb g).obj F) ∧
      Nontrivial (Sheaf.H.{u + 1} ((smallEtalePushforwardAb g).obj F) n)

Stacks.EtaleCohomology.isPrimePowerTorsion_nontrivial_sheafH_smallEtalePullbackAb_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/FiniteEtaleLimit.lean, line 266. The attribute's comment: “given G on S, take F = g⁻¹ G”.

[Stacks, Tag 0DV7], from the base to the limit. In the situation of Stacks.EtaleCohomology.injective_etaleCohomologyPullback_of_isLimit, an ℓ-power torsion sheaf G on S with Hⁿ(S, G) ≠ 0 gives the ℓ-power torsion sheaf g⁻¹ G on X with Hⁿ(X, g⁻¹ G) ≠ 0.

theorem isPrimePowerTorsion_nontrivial_sheafH_smallEtalePullbackAb_of_isLimit
    [IsDirected I (· ≤ ·)] [Nonempty I] [CompactSpace S] [QuasiSeparatedSpace S]
    [∀ i, IsFinite (ι i)] [∀ i, Etale (ι i)] (d : Iᵒᵖ → ℕ)
    [∀ i, Stacks.Morphisms.IsFiniteLocallyFreeOfRank (ι i) (d i)] {ℓ : ℕ}
    (hd : ∀ i, (d i).Coprime ℓ) (hc : IsLimit c) {G : Sheaf (smallEtaleTopology S) Ab.{u + 1}}
    (hG : Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology S) ℓ G) {n : ℕ}
    (hn : Nontrivial (Sheaf.H.{u + 1} G n)) :
    Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology c.pt) ℓ
        ((smallEtalePullbackAb g).obj G) ∧
      Nontrivial (Sheaf.H.{u + 1} ((smallEtalePullbackAb g).obj G) n)

Stacks.EtaleCohomology.exists_isPrimePowerTorsion_nontrivial_sheafH_iff_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/FiniteEtaleLimit.lean, line 288. The attribute's comment: “(1) ⇔ (2)”.

[Stacks, Tag 0DV7]. Let S be a quasi-compact and quasi-separated scheme and let X = lim Xᵢ be the limit of a directed system of S-schemes ιᵢ : Xᵢ ⟶ S, each finite étale of constant degree dᵢ prime to ℓ, with structure morphism g : X ⟶ S. Then there is an ℓ-power torsion sheaf G on S_étale with Hⁿ(S, G) ≠ 0 if and only if there is an ℓ-power torsion sheaf F on X_étale with Hⁿ(X, F) ≠ 0.

The source assumes that ℓ is prime and that n > 0; the proof uses neither.

theorem exists_isPrimePowerTorsion_nontrivial_sheafH_iff_of_isLimit [IsDirected I (· ≤ ·)]
    [Nonempty I] [CompactSpace S] [QuasiSeparatedSpace S] [∀ i, IsFinite (ι i)]
    [∀ i, Etale (ι i)] (d : Iᵒᵖ → ℕ) [∀ i, Stacks.Morphisms.IsFiniteLocallyFreeOfRank (ι i) (d i)]
    {ℓ : ℕ} (hd : ∀ i, (d i).Coprime ℓ) (hc : IsLimit c) (n : ℕ) :
    (∃ G : Sheaf (smallEtaleTopology S) Ab.{u + 1},
        Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology S) ℓ G ∧
          Nontrivial (Sheaf.H.{u + 1} G n)) ↔
      ∃ F : Sheaf (smallEtaleTopology c.pt) Ab.{u + 1},
        Stacks.Torsion.IsPrimePowerTorsion (smallEtaleTopology c.pt) ℓ F ∧
          Nontrivial (Sheaf.H.{u + 1} F n)
Tag 0DV8, a lemma

Tag 0DV8 in the Stacks Project.

AlgebraicGeometry.subsingleton_sheafH_iff_of_isMaximalProPSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MaximalProEllVanishing.lean, line 139.

Stacks Project, Tag 0DV8. Let ℓ be a prime, K a field with separable closure Kˢᵉᵖ, H a maximal pro-ℓ subgroup of Gal(Kˢᵉᵖ/K) and L its fixed field. Then Hⁿ_ét(Spec K, 𝓕) vanishes for every ℓ-power torsion abelian sheaf 𝓕 on the small étale site of Spec K if and only if Hⁿ_ét(Spec L, ℤ/ℓℤ) vanishes.

theorem subsingleton_sheafH_iff_of_isMaximalProPSubgroup (hℓ : ℓ.Prime) (n : ℕ)
    (hH : IsMaximalProPSubgroup ℓ H)
    [HasExt (Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    [HasExt (Sheaf (Spec (.of (fixedField H))).smallEtaleTopology
      AddCommGrpCat.{max (u + 1) v})] :
    (∀ 𝓕 : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{max (u + 1) v},
      Stacks.Torsion.IsPrimePowerTorsion _ ℓ 𝓕 → Subsingleton (Sheaf.H 𝓕 n)) ↔
      Subsingleton (Sheaf.H ((constantSheaf (Spec (.of (fixedField H))).smallEtaleTopology
        AddCommGrpCat.{max (u + 1) v}).obj (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod ℓ))))
          n)
Tag 0DV9, a lemma

Tag 0DV9 in the Stacks Project.

AlgebraicGeometry.tfae_subsingleton_sheafH_of_isMaximalProPSubgroup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MaximalProEllVanishing.lean, line 170. The attribute's comment: “both readings of ℓ-torsion: ℓ-power torsion (1) and killed by ℓ (2)”.

Stacks Project, Tag 0DV9. Let ℓ be a prime, K a field with separable closure Kˢᵉᵖ, H a maximal pro-ℓ subgroup of Gal(Kˢᵉᵖ/K) and L its fixed field. The following are equivalent: 1. H^q_ét(Spec K, 𝓕) vanishes for every q ≥ n and every ℓ-power torsion abelian sheaf 𝓕 on the small étale site of Spec K; 2. H^q_ét(Spec K, 𝓕) vanishes for every q ≥ n and every abelian sheaf 𝓕 on the small étale site of Spec K killed by ℓ; 3. Hⁿ_ét(Spec L, ℤ/ℓℤ) vanishes.

theorem tfae_subsingleton_sheafH_of_isMaximalProPSubgroup (hℓ : ℓ.Prime) (n : ℕ)
    (hH : IsMaximalProPSubgroup ℓ H)
    [HasExt (Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    [HasExt (Sheaf (Spec (.of (fixedField H))).smallEtaleTopology
      AddCommGrpCat.{max (u + 1) v})] :
    List.TFAE [
      ∀ q, n ≤ q → ∀ 𝓕 : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{max (u + 1) v},
        Stacks.Torsion.IsPrimePowerTorsion _ ℓ 𝓕 → Subsingleton (Sheaf.H 𝓕 q),
      ∀ q, n ≤ q → ∀ 𝓕 : Sheaf (Spec (.of K)).smallEtaleTopology AddCommGrpCat.{max (u + 1) v},
        ℓ • 𝟙 𝓕 = 0 → Subsingleton (Sheaf.H 𝓕 q),
      Subsingleton (Sheaf.H ((constantSheaf (Spec (.of (fixedField H))).smallEtaleTopology
        AddCommGrpCat.{max (u + 1) v}).obj (AddCommGrpCat.of (ULift.{max (u + 1) v} (ZMod ℓ))))
          n)]
Tag 03R8, a proposition

Tag 03R8 in the Stacks Project.

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units_of_forall_brauer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupVanishingAllDegrees.lean, line 68. The attribute's comment: “part (1) IN FULL, for the DERIVED-FUNCTOR groups continuousGroupCohomology of Stacks 04JR: H^q(Gal(Ω/K), Ωˣ) = 0 for EVERY q ≥ 1, where Ω is any separably closed field Galois over K, so at Ω = K^sep this is exactly the tag's part (1). The Brauer hypothesis is the source's own -- Br(K') = 0 for every finite extension K'/K -- and the degree range is the source's. Degrees one and two are the two earlier registrations in MultiplicativeGroupVanishingCriterion (Hilbert 90 through the degree-one comparison, and the crossed-product argument through the degree-two comparison, the latter needing only Br(K) = 0). Degrees q ≥ 3 are part (2), the registration in TorsionGaloisVanishing, through isZero_continuousGroupCohomology_of_forall_isAddTorsion: multiplication by a positive integer n on a discrete module has kernel and cokernel killed by n, so part (2) and two passes of the long exact sequence of the δ-functor of Stacks 010Q make it injective on H^q for q ≥ 3, while every class is killed by some positive integer by Stacks 0DV3 part (1). This registration is part (1); part (2) is the registration in TorsionGaloisVanishing and the degree-one and degree-two statements keep their own registrations in MultiplicativeGroupVanishingCriterion”. References: SGA 4½ Arcata (3.1.6).

Let Ω be a separably closed Galois extension of a field K and assume Br(K') = 0 for every finite extension K'/K. Then H^q(Gal(Ω/K), Ωˣ) = 0 for every q ≥ 1, the group being the continuous group cohomology of the discrete Galois module Stacks.GaloisCohomology.unitsContinuousGModule.

theorem isZero_continuousGroupCohomology_units_of_forall_brauer (K Ω : Type u) [Field K]
    [Field Ω] [Algebra K Ω] [IsGalois K Ω] [IsSepClosed Ω]
    (hBr : ∀ (K' : Type u) [Field K'] [Algebra K K'] [Module.Finite K K']
      (y : BrauerGroup K'), y = 1)
    (q : ℕ) (hq : 1 ≤ q) :
    IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) q (unitsContinuousGModule K Ω))

Stacks.GaloisCohomology.isMulCoboundary₂_of_brauerGroup_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupVanishingCriterion.lean, line 211. The attribute's comment: “part (1) in degree two, in explicit cocycle form, UNCONDITIONAL -- nothing is carried. Under the tag's Brauer hypothesis every locally constant 2-cocycle of the Galois group with values in the units is a coboundary, which is the vanishing of H^2(Gal(Ω/K), Ωˣ); at Ω = K^sep this is the tag's degree-two case. Proved from isMulCoboundary₂_of_forall_finiteGalois fed with the crossed-product argument isMulCoboundary₂_of_brauer, whose premise the tag's hypothesis discharges at once since Br(K) = 0 forces every relative Brauer group Br(L/K) to vanish. The hypothesis used here is only Br(K) = 0, which is weaker than the tag's, and Ω is an arbitrary Galois extension rather than the separable closure, so this is more general than the tag's degree-two case rather than narrower. NOT proved here: the other degrees of part (1), for which see isZero_continuousGroupCohomology_units, and part (2)”.

Stacks Project, Tag 03R8, part (1) in degree two, in explicit cocycle form and with no carried hypothesis: if Br(K) = 0 then every locally constant 2-cocycle on Gal(Ω/K) with values in Ωˣ is a coboundary, which is the vanishing of H^2(Gal(Ω/K), Ωˣ). At Ω = Kˢᵉᵖ this is the degree-two case of the tag.

The hypothesis is weaker than the tag's, which asks for the Brauer group of every finite extension of K: only Br(K) = 0 is used, because it already makes every relative Brauer group Br(L/K) vanish, which is the premise of Stacks.GaloisCohomology.isMulCoboundary₂_of_brauer at each finite Galois subextension L of Ω.

theorem isMulCoboundary₂_of_brauerGroup_eq_one (hBr : ∀ y : BrauerGroup K, y = 1)
    (f : Gal(Ω/K) × Gal(Ω/K) → Ωˣ) (hloc : IsLocallyConstant f) (hf : IsMulCocycle₂ f) :
    IsMulCoboundary₂ f

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupVanishingCriterion.lean, line 261. The attribute's comment: “part (1), the full degree range q ≥ 1, over three carried hypotheses, and for an arbitrary Galois extension Ω/K rather than only the separable closure. CARRIED as h03QU₁ and h03QU₂: the comparison in degrees one and two between the explicit cocycle description of Galois cohomology and the derived-functor description continuousGroupCohomology of Stacks 04JR -- the two are not related anywhere in this library above degree zero, where the comparison is invariantsIsoZerothCohomology; this is the standard comparison of the standard complex with the right derived functor and not a Stacks tag of its own. CARRIED as hhigh: the vanishing in degrees q ≥ 3, which is the one part of part (1) assumed wholesale; the source gets it from part (2) of this tag together with the four-term sequence 0 → A → M → M ⊗ Q → B → 0, whose divisible-coefficient input IS proved (isZero_continuousGroupCohomology_of_module_rat, Stacks 0DV3 part (2)) but whose remaining ingredients -- part (2), the construction of M ⊗ Q as a discrete Galois module, and the long exact sequence of continuousGroupCohomology -- are not. PROVED: degrees one and two, where the cocycle premises of h03QU₁ and h03QU₂ are discharged from proved results -- Hilbert 90 for an infinite Galois extension (isMulCoboundary₁_of_isLocallyConstant_of_isMulCocycle₁, which needs no hypothesis) and the crossed-product argument (isMulCoboundary₂_of_brauerGroup_eq_one above), the latter consuming the Brauer hypothesis. So the hypothesis is genuinely used and the tag's content in degrees one and two is established, not assumed. Also PROVED, and new: the coefficient module itself, unitsContinuousGModule, the units of Ω as a discrete Galois module in the sense of Stacks 04JP, together with the continuity of the Galois action on them. NOT proved: part (2) of the tag, for which the library has none of the inputs -- see this file's module documentation”.

Stacks Project, Tag 03R8, part (1). Let K be a field with Br(K) = 0 and let Ω/K be a Galois extension. Then

H^q(Gal(Ω/K), Ωˣ) = 0 for every q ≥ 1,

the groups being this library's continuous group cohomology of Stacks 04JR evaluated at the discrete Galois module Stacks.GaloisCohomology.unitsContinuousGModule. At Ω = Kˢᵉᵖ this is part (1) of the tag.

Three inputs are carried. h03QU₁ and h03QU₂ are the comparison, in degrees one and two, between the cocycle description of Galois cohomology and the derived-functor description: the vanishing of the cocycle quotient implies the vanishing of continuousGroupCohomology. The two descriptions are not related anywhere in this library above degree zero. hhigh is the vanishing in degrees q ≥ 3, which the source deduces from part (2) of the tag through the four-term sequence 0 → A → M → M ⊗ 𝐐 → B → 0; part (2) is not formalized here.

What is proved is degrees one and two: in degree one the cocycle premise of h03QU₁ is Hilbert's theorem 90 for an infinite Galois extension, Stacks.GaloisCohomology.isMulCoboundary₁_of_isLocallyConstant_of_isMulCocycle₁, which needs no hypothesis at all; in degree two it is Stacks.GaloisCohomology.isMulCoboundary₂_of_brauerGroup_eq_one, which consumes the Brauer hypothesis. So the Brauer hypothesis is genuinely used, and the tag's content in degrees one and two is established rather than assumed.

theorem isZero_continuousGroupCohomology_units (hBr : ∀ y : BrauerGroup K, y = 1)
    (h03QU₁ : (∀ f : Gal(Ω/K) → Ωˣ, IsLocallyConstant f → IsMulCocycle₁ f →
          IsMulCoboundary₁ f) →
        IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) 1 (unitsContinuousGModule K Ω)))
    (h03QU₂ : (∀ f : Gal(Ω/K) × Gal(Ω/K) → Ωˣ, IsLocallyConstant f → IsMulCocycle₂ f →
          IsMulCoboundary₂ f) →
        IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) 2 (unitsContinuousGModule K Ω)))
    (hhigh : ∀ q : ℕ, 3 ≤ q →
      IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) q (unitsContinuousGModule K Ω)))
    (q : ℕ) (hq : 1 ≤ q) :
    IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) q (unitsContinuousGModule K Ω))

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupVanishingCriterionUnconditional.lean, line 131. The attribute's comment: “part (1) at q = 1, for the derived-functor groups H^q(Gal(Ω/K), Ωˣ) of Stacks 04JR, with NO HYPOTHESIS WHATSOEVER -- STRONGER than the proposition at q = 1 in two independent ways. First, the proposition assumes Br(K') = 0 uniformly over every finite extension K'/K and this assumes nothing about Brauer groups at all: the cocycle statement at q = 1 is Hilbert 90 for an infinite Galois extension, namely isMulCoboundary₁_of_isLocallyConstant_of_isMulCocycle₁, which is unconditional, so the proposition's hypothesis is not used and is not needed. Second, Ω is an arbitrary Galois extension rather than the separable closure; at Ω = K^sep this is exactly the tag's q = 1 case. Nothing is carried: the comparison between the cocycle and derived-functor descriptions is Stacks.GroupCohomology.isZero_continuousGroupCohomology_one_of_forall_isCoboundary, which is a theorem, not a hypothesis. NOT proved here: the degrees q ≥ 2 of part (1) -- q = 2 is isZero_continuousGroupCohomology_units_two just below, over the tag's own hypothesis in the weaker form Br(K) = 0, and the degrees q ≥ 3 are isZero_continuousGroupCohomology_units_of_fourTerm and isZero_continuousGroupCohomology_units_of_annihilated, which still carry part (2) -- and part (2) itself”. References: SGA 4½ Arcata (1.5.3), “more general”.

For a Galois extension Ω/K, the continuous group cohomology H¹(Gal(Ω/K), Ωˣ) of the discrete Galois module Stacks.GaloisCohomology.unitsContinuousGModule vanishes.

theorem isZero_continuousGroupCohomology_units_one :
    IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) 1 (unitsContinuousGModule K Ω))

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupVanishingCriterionUnconditional.lean, line 159. The attribute's comment: “part (1) at q = 2, for the derived-functor groups H^q(Gal(Ω/K), Ωˣ) of Stacks 04JR. Nothing is carried: no comparison between the cocycle and derived-functor descriptions is assumed, and the only hypothesis is Br(K) = 0. That is STRICTLY WEAKER than the proposition's own hypothesis, which assumes Br(K') = 0 uniformly over every finite extension K'/K -- Br(K) = 0 is one instance of it, and it already forces every relative Brauer group Br(L/K) to vanish, which is what the crossed-product argument needs at each finite Galois subextension. Ω is an arbitrary Galois extension rather than the separable closure, so this is more general than the tag's degree-two case in that respect too; at Ω = K^sep it is exactly that case. The cocycle input is isMulCoboundary₂_of_brauer, assembled by exists_isLocallyConstant_isMulCoboundary₂_of_forall_finiteGalois (which records that the trivialising 1-cochain, being inflated from a finite level, is locally constant -- strictly more than Mathlib's IsMulCoboundary₂ gives, and exactly what the comparison consumes); the comparison itself is Stacks.GroupCohomology.isZero_continuousGroupCohomology_two_of_forall_isCoboundary, which is a theorem, not a hypothesis. NOT proved here: q = 1 of part (1), which is isZero_continuousGroupCohomology_units_one above and needs no Brauer hypothesis at all; the degrees q >= 3, which are isZero_continuousGroupCohomology_units_of_fourTerm and isZero_continuousGroupCohomology_units_of_annihilated and still carry part (2); and part (2) itself”. References: SGA 4½ Arcata (3.1.6), “clause i), degree q=2”.

Let K be a field with Br(K) = 0 and let Ω/K be a Galois extension. Then the continuous group cohomology H²(Gal(Ω/K), Ωˣ) of the discrete Galois module Stacks.GaloisCohomology.unitsContinuousGModule vanishes.

theorem isZero_continuousGroupCohomology_units_two (hBr : ∀ y : BrauerGroup K, y = 1) :
    IsZero (continuousGroupCohomology.{u, u} Gal(Ω/K) 2 (unitsContinuousGModule K Ω))

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units_and_torsion_of_forall_brauer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/SeparableClosureVanishing.lean, line 84. The attribute's comment: “the WHOLE proposition at Ω = K^sep: part (1) and part (2) together, as one statement, under exactly the source's hypothesis -- Br(K') = 0 for every finite extension K'/K. The first conjunct is H^q(Gal(K^sep/K), (K^sep)ˣ) = 0 for every q ≥ 1, at the discrete Galois module unitsContinuousGModule; the second is H^q(Gal(K^sep/K), M) = 0 for every torsion discrete Galois module M and every q ≥ 2. Both are values of the derived-functor groups continuousGroupCohomology of Stacks 04JR. This is an assembly of the two theorems of this chapter that each prove one part in full: isZero_continuousGroupCohomology_units_of_forall_brauer, in StacksFrontier.AlgebraicGeometry.EtaleCohomology.GaloisCohomology.MultiplicativeGroupVanishingAllDegrees, which takes the same Brauer hypothesis verbatim and gives every degree q ≥ 1; and isZero_continuousGroupCohomology_of_isAddTorsion, in StacksFrontier.AlgebraicGeometry.EtaleCohomology.GaloisCohomology.TorsionGaloisVanishing, which gives every degree q ≥ 2 for every torsion discrete module, and whose hypothesis -- Br(L) = 0 for the intermediate fields L of K^sep/K finite over K -- is an instance of the source's at K' = ↥L, every such L being a finite extension of K. Every clause of the proposition is established here. The per-part registrations elsewhere in the chapter are retained: part (1) in every degree in MultiplicativeGroupVanishingAllDegrees, part (2) in TorsionGaloisVanishing, and the degree-one and degree-two statements of part (1) in MultiplicativeGroupVanishingCriterion”. References: SGA 4½ Arcata (3.1.6).

Stacks Project, Tag 03R8. Let K be a field with separable algebraic closure Kˢᵉᵖ, and assume that Br(K') = 0 for every finite extension K'/K. Then

  1. H ^q(Gal(Kˢᵉᵖ/K), (Kˢᵉᵖ)ˣ) = 0 for every q ≥ 1, and
  2. H ^q(Gal(Kˢᵉᵖ/K), M) = 0 for every torsion discrete Gal(Kˢᵉᵖ/K)-module M and every q ≥ 2,

the groups being this library's continuous group cohomology of Stacks 04JR, and the module of the first conjunct being the discrete Galois module Stacks.GaloisCohomology.unitsContinuousGModule.

theorem isZero_continuousGroupCohomology_units_and_torsion_of_forall_brauer (K : Type u)
    [Field K]
    (hBr : ∀ (K' : Type u) [Field K'] [Algebra K K'] [Module.Finite K K']
      (y : BrauerGroup K'), y = 1) :
    (∀ q : ℕ, 1 ≤ q → IsZero (continuousGroupCohomology.{u, u} Gal(SeparableClosure K/K) q
        (unitsContinuousGModule K (SeparableClosure K)))) ∧
      ∀ (M : ContinuousGModule.{u, max u v} Gal(SeparableClosure K/K)),
        IsAddTorsion M.obj.obj.V → ∀ q : ℕ, 2 ≤ q →
          IsZero (continuousGroupCohomology.{u, v} Gal(SeparableClosure K/K) q M)

Stacks.GaloisCohomology.isZero_continuousGroupCohomology_of_isAddTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/TorsionGaloisVanishing.lean, line 60. The attribute's comment: “part (2) in full, for the DERIVED-FUNCTOR groups continuousGroupCohomology of Stacks 04JR: H^q(Gal(Ω/K), M) = 0 for EVERY torsion discrete Galois module M and EVERY q ≥ 2, where Ω is any separably closed field Galois over K, so at Ω = K^sep this is exactly the tag's part (2). The Brauer hypothesis is the one the source states, and in fact less: only the finite SEPARABLE extensions of K inside Ω are used, whereas the tag asks for every finite extension, so this statement implies the tag's rather than specialising it. The proof is the source's dévissage carried out on locally constant cochains. A locally constant 2-cocycle on a profinite group takes finitely many values, so it is a cocycle with values in a finite submodule; a finite module is reduced to a module killed by a prime p along its p-torsion subgroup; a finite module killed by p is handled over an open subgroup of index prime to p -- the preimage of a p-Sylow subgroup of a finite quotient -- where the action factors through a p-group and the module is filtered by copies of Z/p with trivial action, and the restriction-corestriction identity cor o res = n, written out on cochains, carries the trivialization back to the whole group; and Z/p with trivial action is the Kummer sequence of Stacks 03PL away from the characteristic and the Artin-Schreier sequence of Stacks 0A3J in the characteristic, each fed by the two degrees of part (1) proved in MultiplicativeGroupVanishingCriterion. Degrees above two come from dimension shifting along the module of locally constant functions into a torsion divisible hull, which is an injective object of the category of Stacks 04JP whose cokernel is again torsion. This registration is part (2); part (1) has its own three registrations in MultiplicativeGroupVanishingCriterion”. References: SGA 4½ Arcata (3.1.6), “more general”.

If the Brauer group of every finite subextension of a separably closed Galois extension Ω/K vanishes, then H^q(Gal(Ω/K), M) = 0 for every torsion discrete Gal(Ω/K)-module M and every q ≥ 2, the groups being the continuous group cohomology.

theorem isZero_continuousGroupCohomology_of_isAddTorsion (K Ω : Type u) [Field K] [Field Ω]
    [Algebra K Ω] [IsGalois K Ω] [IsSepClosed Ω]
    (hBr : ∀ L : IntermediateField K Ω, FiniteDimensional K L → ∀ y : BrauerGroup L, y = 1)
    (M : ContinuousGModule.{u, max u v} Gal(Ω/K)) (hM : IsAddTorsion M.obj.obj.V)
    (q : ℕ) (hq : 2 ≤ q) :
    IsZero (continuousGroupCohomology.{u, v} Gal(Ω/K) q M)
Tag 03R9, a definition

Tag 03R9 in the Stacks Project.

IsCField, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/CFields.lean, line 40. References: SGA 4½ Arcata (3.2.1), “more general”.

A field K is a \(C_r\) field if every homogeneous polynomial of degree d ≥ 1 in n variables has a nonzero solution when d ^ r < n.

The degree bound is 0 < d, not 0 < d ^ r. The two agree for every r ≥ 1, but at r = 0 they do not: d ^ 0 = 1 even for d = 0, so 0 < d ^ r is satisfied by the constant polynomial 1, which is homogeneous of degree 0 and has no nonzero root. With that spelling IsCField K 0 is false for every field, which is not what \(C_0\) means.

abbrev IsCField (K : Type*) [Field K] (r : ℕ) : Prop
Tag 03RA, an example

Tag 03RA in the Stacks Project.

exists_nonzero_common_zero_of_isHomogeneous, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/HomogeneousZeros.lean, line 40. The attribute's comment: “an algebraically closed field is C_r: the one-polynomial case s = 1”.

Stacks Project, Tag 03RB. Over an algebraically closed field, a family of s < n homogeneous polynomials of positive degree in n variables has a common nonzero zero.

lemma exists_nonzero_common_zero_of_isHomogeneous
    (k : Type*) [Field k] [IsAlgClosed k] {s n : ℕ}
    (d : Fin s → ℕ) (f : (i : Fin s) → MvPolynomial (Fin n) k)
    (hd : ∀ i, 0 < d i) (hf : ∀ i, (f i).IsHomogeneous (d i)) (hsn : s < n) :
    ∃ α : Fin n → k, α ≠ 0 ∧ ∀ i, MvPolynomial.eval α (f i) = 0
Tag 03RB, a lemma

Tag 03RB in the Stacks Project.

exists_nonzero_common_zero_of_isHomogeneous, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/HomogeneousZeros.lean, line 40.

Stacks Project, Tag 03RB. Over an algebraically closed field, a family of s < n homogeneous polynomials of positive degree in n variables has a common nonzero zero.

lemma exists_nonzero_common_zero_of_isHomogeneous
    (k : Type*) [Field k] [IsAlgClosed k] {s n : ℕ}
    (d : Fin s → ℕ) (f : (i : Fin s) → MvPolynomial (Fin n) k)
    (hd : ∀ i, 0 < d i) (hf : ∀ i, (f i).IsHomogeneous (d i)) (hsn : s < n) :
    ∃ α : Fin n → k, α ≠ 0 ∧ ∀ i, MvPolynomial.eval α (f i) = 0
Tag 03RC, a theorem

Tag 03RC in the Stacks Project.

brauerGroup_eq_one_of_isCField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/BrauerGroupCField.lean, line 313. References: SGA 4½ Arcata (3.2.2).

Every Brauer class over a C₁ field is trivial.

theorem brauerGroup_eq_one_of_isCField (K : Type u) [Field K]
    (hK : IsCField K 1) (x : BrauerGroup K) : x = 1
Tag 03RE, a definition

Tag 03RE in the Stacks Project.

AlgebraicGeometry.IsCurve, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Curve/Defs.lean, line 46. The attribute's comment: “the curve clause”. References: EGA II (7.4.2), “special case”.

Stacks Project, Tag 0A23. A curve over a field is a variety of Krull dimension one.

public class IsCurve (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) : Prop
    extends IsVariety k f

AlgebraicGeometry.IsVariety, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Variety/Defs/Basic.lean, line 50. The attribute's comment: “the variety clause”.

A scheme over a field is a variety when it is integral and its structure morphism is separated and of finite type.

class IsVariety (k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) : Prop
    extends IsIntegral X, IsSeparated f, LocallyOfFiniteType f, QuasiCompact f
Tag 03RD, a theorem

Tag 03RD in the Stacks Project.

AlgebraicGeometry.isCField_functionField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/TsenFunctionField.lean, line 86.

Stacks Project, Tag 03RD (Tsen's theorem). The function field of a variety of dimension r over an algebraically closed field k is a \(C_r\) field.

theorem isCField_functionField (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}}
    (f : X ⟶ Spec (.of k)) [IsVariety k f] {r : ℕ} (hr : topologicalKrullDim X = r) :
    IsCField X.functionField r
Tag 03RF, a lemma

Tag 03RF in the Stacks Project.

AlgebraicGeometry.brauerGroup_functionField_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/BrauerGroupFunctionField.lean, line 84. References: SGA 4½ Arcata (3.2.4), “q = 2 (Brauer group)”; SGA 4½ Arcata (3.2.2), “special case”.

The Brauer group of the function field of a curve over an algebraically closed field is trivial.

theorem brauerGroup_functionField_eq_one (k : Type u) [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) [IsCurve k f]
    (y : BrauerGroup X.functionField) : y = 1
Tag 03RG, a lemma

Tag 03RG in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_spec_of_trdeg_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupTranscendenceDegreeOneVanishing.lean, line 67. References: SGA 4½ Arcata (3.1.6), “clause i), special case”; SGA 4½ Arcata (3.2.4).

Stacks Project, Tag 03RG. Let k be an algebraically closed field and K/k a field extension of transcendence degree one. Then

H^q_étale(Spec K, 𝐆_m) = 0 for every q ≥ 1.

The criterion of Stacks 03R8 read through Stacks 03QU, AlgebraicGeometry.subsingleton_sheafH_multiplicativeSheaf_of_forall_brauer, reduces this to the triviality of the Brauer group of every finite extension K'/K; such a K' has transcendence degree one over k, so Br(K') = 0 by Stacks.EtaleCohomology.brauerGroup_eq_one_of_module_finite_of_trdeg_eq_one.

theorem subsingleton_sheafH_multiplicativeSheaf_spec_of_trdeg_eq_one (k : Type u) [Field k]
    [IsAlgClosed k] (K : Type u) [Field K] [Algebra k K] (hK : Algebra.trdeg k K = 1)
    (q : ℕ) (hq : 1 ≤ q) :
    Subsingleton (Sheaf.H.{u + 1, u + 1}
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec (.of K))) q)

Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_of_trdeg_eq_one, an alias in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GaloisCohomology/MultiplicativeGroupTranscendenceDegreeOneVanishing.lean, line 110. The attribute's comment: “vanishing of the positive-degree étale cohomology of 𝐆_m over a transcendence-degree-one extension of an algebraically closed field, over Tag 03R8 and Tag 03QU as the hypothesis h03RG”.

Stacks Project, Tag 03RG, under its earlier name: an alias of Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_spec_of_trdeg_eq_one. Let k be an algebraically closed field and K/k a field extension of transcendence degree one. Then H^q_étale(Spec K, 𝐆_m) = 0 for every q ≥ 1.

alias subsingleton_sheafH_multiplicativeSheaf_of_trdeg_eq_one
Sources
LeanStacks.EtaleCohomology.isPrimePowerTorsion_nontrivial_sheafH_smallEtalePushforwardAb_of_isLimit · Stacks.EtaleCohomology.isPrimePowerTorsion_nontrivial_sheafH_smallEtalePullbackAb_of_isLimit · Stacks.EtaleCohomology.exists_isPrimePowerTorsion_nontrivial_sheafH_iff_of_isLimit · AlgebraicGeometry.subsingleton_sheafH_iff_of_isMaximalProPSubgroup · AlgebraicGeometry.tfae_subsingleton_sheafH_of_isMaximalProPSubgroup · Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units_of_forall_brauer · Stacks.GaloisCohomology.isMulCoboundary₂_of_brauerGroup_eq_one · Stacks.GaloisCohomology.isZero_continuousGroupCohomology_units

Section59.68 Higher vanishing for the multiplicative group#

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

Tag 03RI, a theorem

Tag 03RI in the Stacks Project.

Stacks.EtaleCohomology.epi_divisorSequenceSecondMapOfCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorEpi.lean, line 472. The attribute's comment: “the right-hand exactness of the sequence for a smooth curve over a field: the second map, as constructed here, is an epimorphism of étale sheaves; the exactness in the middle is proved separately, as Stacks.EtaleCohomology.exact_divisorSequenceOfCurve”.

The second map of the fundamental exact sequence of Stacks 03RI is an epimorphism, for a smooth curve over a field: j_* 𝐆_{m,η} ⟶ ⨁_{x ∈ X_0} (i_x)_* 𝐙 ⟶ 0 is exact. This is the right-hand exactness of the source, with the algebraically closed base field of the source weakened to an arbitrary field.

It is Stacks.EtaleCohomology.epi_divisorSequenceSecondMapOfCurve_of_forall_imageSieve_ι_mem with its hypothesis discharged by Stacks.EtaleCohomology.imageSieve_ι_mem_of_isCurve.

Together with the left end, Stacks.EtaleCohomology.mono_multiplicativeDirectImageComparison_genericPointInclusion, and the vanishing of the composite, Stacks.EtaleCohomology.multiplicativeDirectImageComparison_comp_divisorSequenceSecondMapOfCurve, what remains of Stacks 03RI is the exactness in the middle, Stacks.EtaleCohomology.exact_divisorSequenceOfCurve; the four together are the short exactness of the sequence, Stacks.EtaleCohomology.shortExact_divisorSequenceOfCurve, which is what discharges the short exactness hypothesis of Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_smoothCurve.

theorem epi_divisorSequenceSecondMapOfCurve {k : Type u} [Field k] {X : Scheme.{u}}
    (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g] :
    Epi (divisorSequenceSecondMapOfCurve.{u, v} g)

Stacks.EtaleCohomology.exact_divisorSequenceOfCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorMiddleExactness.lean, line 280. The attribute's comment: “the exactness in the middle of the sequence for a smooth curve over a field: a section of j_* G_m killed by the divisor map is étale locally an invertible global function”.

For a smooth curve X over a field, the fundamental exact sequence 0 → 𝐆_{m,X} → j_* 𝐆_{m,η} → ⨁_{x ∈ X_0} (i_x)_* 𝐙 → 0 is exact in the middle: the kernel of the divisor map j_* 𝐆_{m,η} ⟶ ⨁_{x ∈ X_0} (i_x)_* 𝐙 is the image of 𝐆_{m,X}.

theorem exact_divisorSequenceOfCurve {k : Type u} [Field k] {X : Scheme.{u}}
    (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g] :
    (ShortComplex.mk
      (multiplicativeDirectImageComparison.{u, u + 1} (genericPointInclusion X))
      (divisorSequenceSecondMapOfCurve.{u, u + 1} g)
      (multiplicativeDirectImageComparison_comp_divisorSequenceSecondMapOfCurve.{u, u + 1}
        g)).Exact

Stacks.EtaleCohomology.shortExact_divisorSequenceOfCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorMiddleExactness.lean, line 299. The attribute's comment: “the fundamental exact sequence for a smooth curve over a field, as a short exact sequence of étale sheaves”.

Let X be a smooth curve over a field k, let η be its generic point with inclusion j : η ⟶ X, and let X_0 be its set of closed points with inclusions i_x. Then

0 → 𝐆_{m,X} → j_* 𝐆_{m,η} → ⨁_{x ∈ X_0} (i_x)_* 𝐙 → 0

is a short exact sequence of étale sheaves on X.

theorem shortExact_divisorSequenceOfCurve {k : Type u} [Field k] {X : Scheme.{u}}
    (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g] :
    (ShortComplex.mk
      (multiplicativeDirectImageComparison.{u, u + 1} (genericPointInclusion X))
      (divisorSequenceSecondMapOfCurve.{u, u + 1} g)
      (multiplicativeDirectImageComparison_comp_divisorSequenceSecondMapOfCurve.{u, u + 1}
        g)).ShortExact

Stacks.EtaleCohomology.closedPointDivisorSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSections.lean, line 273. The attribute's comment: “the second map on sections over an arbitrary étale X-scheme, for X integral and normal”.

The second map of the fundamental exact sequence 0 → 𝐆_{m,X} → j_* 𝐆_{m,η} → ⨁_{x ∈ X_0} (i_x)_* 𝐙 → 0, on sections over an arbitrary étale X-scheme U: an invertible global function on the generic fibre η ×_X U is sent to the finitely supported family of its orders of vanishing in ⨁_{x ∈ X_0} ((i_x)_* 𝐙)(U), the member at a closed point x being the locally constant 𝐙-valued map on the fibre x ×_X U recording the order of vanishing at each point of U over x.

def closedPointDivisorSections :
    Additive ((Γ(pullback U.hom (genericPointInclusion X), ⊤))ˣ) →+
      DirectSum ↥(closedPoints X)
        fun x : closedPoints X => (integerSkyscraper.{u, v} X x.1).obj.obj (op U)

Stacks.EtaleCohomology.closedPointDivisorSections_restrict_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSections.lean, line 300. The attribute's comment: “the sequence on sections over an arbitrary étale X-scheme is a complex, for X integral and normal”.

The fundamental exact sequence is a complex on sections over an arbitrary étale X-scheme U: the restriction to the generic fibre of an invertible global function on U has zero family of orders of vanishing.

theorem closedPointDivisorSections_restrict_eq_zero (a : (Γ(U.left, ⊤))ˣ) :
    closedPointDivisorSections.{u, v} U (Additive.ofMul (Units.map
      (pullback.fst U.hom (genericPointInclusion X)).appTop.hom.toMonoidHom a)) = 0

Stacks.EtaleCohomology.integerSkyscraperDivisorOfPoint_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafMap.lean, line 117. The attribute's comment: “the x-component of the second map is compatible with restriction along a morphism of étale X-schemes, read in the sections of i_{x,*} Z, for X integral and normal”.

The x-component of the second map of the fundamental exact sequence is compatible with restriction along a morphism of the small étale site, read in the sections of (i_x)_* 𝐙 over an étale X-scheme. Neither object is assumed irreducible.

theorem integerSkyscraperDivisorOfPoint_map {X : Scheme.{u}} [AlgebraicGeometry.IsIntegral X]
    [IsNormal X] {U V : X.Etale} [IsLocallyNoetherian U.left] [IsLocallyNoetherian V.left]
    (x : X) (φ : U ⟶ V) (a : (Γ(pullback V.hom (genericPointInclusion X), ⊤))ˣ) :
    ((integerSkyscraper.{u, v} X x).obj.map φ.op).hom
        (integerSkyscraperDivisorOfPoint.{u, v} V x (Additive.ofMul a)) =
      integerSkyscraperDivisorOfPoint.{u, v} U x
        (Additive.ofMul (Units.map (etaleGenericFibreMap φ).appTop.hom.toMonoidHom a))

Stacks.EtaleCohomology.closedPointDivisorPresheafSection_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafMap.lean, line 195. The attribute's comment: “the second map of the sequence is compatible with restriction along a morphism of étale X-schemes, read in the coproduct of the underlying presheaves of the skyscrapers, for X integral and normal”.

The second map on sections is compatible with restriction, read in the coproduct of the underlying presheaves of the skyscrapers: restricting the section attached to a unit on the generic fibre of V along a morphism φ : U ⟶ V of the small étale site gives the section attached to the restricted unit. Neither object is assumed irreducible.

theorem closedPointDivisorPresheafSection_map {U V : X.Etale} [IsLocallyNoetherian U.left]
    [NoetherianSpace U.left] [IsLocallyNoetherian V.left] [NoetherianSpace V.left]
    (φ : U ⟶ V) (a : (Γ(pullback V.hom (genericPointInclusion X), ⊤))ˣ) :
    ((∐ fun x : closedPoints X ↦ (closedPointSkyscraper.{u, v} X x).obj).map φ.op).hom
        (closedPointDivisorPresheafSection.{u, v} V (Additive.ofMul a)) =
      closedPointDivisorPresheafSection.{u, v} U (Additive.ofMul (Units.map
        ((smallEtaleBaseChange (genericPointInclusion X)).map
          φ).left.appTop.hom.toMonoidHom a))

Stacks.EtaleCohomology.closedPointDivisorPresheafSection_restrict_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafMap.lean, line 213. The attribute's comment: “the sequence is a complex on sections over an arbitrary étale X-scheme, read in the coproduct of the underlying presheaves of the skyscrapers, for X integral and normal”.

An invertible global function on U has trivial image under the second map, read in the presheaf coproduct: the sequence is a complex on sections over an étale X-scheme with Noetherian space, with no irreducibility hypothesis.

theorem closedPointDivisorPresheafSection_restrict_eq_zero (U : X.Etale)
    [IsLocallyNoetherian U.left] [NoetherianSpace U.left] (a : (Γ(U.left, ⊤))ˣ) :
    closedPointDivisorPresheafSection.{u, v} U (Additive.ofMul (Units.map
      (pullback.fst U.hom (genericPointInclusion X)).appTop.hom.toMonoidHom a)) = 0

Stacks.EtaleCohomology.closedPointDivisorSheafSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 250. The attribute's comment: “the second map on sections over an étale X-scheme with Noetherian space, valued in the sheaf ⨁_x i_{x,*} Z, for X integral and normal; no irreducibility is assumed”.

The second map of the fundamental exact sequence of Stacks 03RI over an arbitrary étale X-scheme with Noetherian space, valued in the sheaf ⨁_x (i_x)_* 𝐙 itself. This is Stacks.EtaleCohomology.closedPointDivisorSections followed by Stacks.EtaleCohomology.closedPointDivisorSheaf.sheafSectionOfDirectSum.

No irreducibility hypothesis is carried on U, which is the generality of the source.

def closedPointDivisorSheafSection (U : X.Etale) [IsLocallyNoetherian U.left]
    [NoetherianSpace U.left] :
    Additive ((Γ(pullback U.hom (genericPointInclusion X), ⊤))ˣ) →+
      (closedPointDivisorSheaf.{u, v} X).obj.obj (op U)

Stacks.EtaleCohomology.closedPointDivisorSheafSection_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 283. The attribute's comment: “the second map of the sequence is compatible with restriction along a morphism of étale X-schemes with Noetherian spaces, read in the sheaf ⨁_x i_{x,*} Z, for X integral and normal; no irreducibility is assumed”.

The commuting square that makes the second map of Stacks 03RI a map of presheaves, read in the sheaf ⨁_x (i_x)_* 𝐙: restricting the section attached to a unit on the generic fibre of V along a morphism φ : U ⟶ V of the small étale site gives the section attached to the restricted unit.

It is Stacks.EtaleCohomology.closedPointDivisorSections_map together with the naturality of the passage from the direct sum of the groups of sections to the sections of the sheaf, Stacks.EtaleCohomology.closedPointDivisorSheaf.map_comp_sheafSectionOfDirectSum. Neither object is assumed irreducible, so this is the square at the generality of the source.

theorem closedPointDivisorSheafSection_map {U V : X.Etale} [IsLocallyNoetherian U.left]
    [NoetherianSpace U.left] [IsLocallyNoetherian V.left] [NoetherianSpace V.left]
    (φ : U ⟶ V) (a : (Γ(pullback V.hom (genericPointInclusion X), ⊤))ˣ) :
    ((closedPointDivisorSheaf.{u, v} X).obj.map φ.op).hom
        (closedPointDivisorSheafSection.{u, v} V (Additive.ofMul a)) =
      closedPointDivisorSheafSection.{u, v} U (Additive.ofMul (Units.map
        ((smallEtaleBaseChange (genericPointInclusion X)).map
          φ).left.appTop.hom.toMonoidHom a))

Stacks.EtaleCohomology.closedPointDivisorSheafSection_restrict_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 301. The attribute's comment: “the sequence is a complex on sections over an étale X-scheme with Noetherian space, read in the sheaf ⨁_x i_{x,*} Z, for X integral and normal; no irreducibility is assumed”.

An invertible global function on U has trivial image under the second map of Stacks 03RI read in the sheaf ⨁_x (i_x)_* 𝐙: the sequence of the source is a complex over an arbitrary étale X-scheme with Noetherian space, with no irreducibility hypothesis.

theorem closedPointDivisorSheafSection_restrict_eq_zero (U : X.Etale)
    [IsLocallyNoetherian U.left] [NoetherianSpace U.left] (a : (Γ(U.left, ⊤))ˣ) :
    closedPointDivisorSheafSection.{u, v} U (Additive.ofMul (Units.map
      (pullback.fst U.hom (genericPointInclusion X)).appTop.hom.toMonoidHom a)) = 0

Stacks.EtaleCohomology.affineEtaleDivisorRestricted, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 493. The attribute's comment: “the second map of the sequence on the affine étale site, as a morphism of presheaves, for X integral, normal and locally Noetherian”.

The second map of the fundamental exact sequence of Stacks 03RI on the affine étale site, as a morphism of presheaves of abelian groups. Its component at an affine étale X-scheme W is Stacks.EtaleCohomology.affineEtaleDivisorApp, and its commuting square is Stacks.EtaleCohomology.affineEtaleDivisorApp_naturality.

def affineEtaleDivisorRestricted :
    (Scheme.AffineEtale.Spec X).op ⋙ ((genericPointDirectImage.{u, v} X).obj
        (Stacks.Kummer.multiplicativeSheaf.{u, v} (Spec X.functionField))).obj ⟶
      (Scheme.AffineEtale.Spec X).op ⋙ (closedPointDivisorSheaf.{u, v} X).obj

Stacks.EtaleCohomology.divisorSequenceSecondMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 523. The attribute's comment: “the second map of the sequence, as a morphism of étale sheaves, for X integral, normal and locally Noetherian; the exactness of the sequence is not proved at this generality”.

The second map of the fundamental exact sequence of Stacks 03RI, as a morphism of abelian sheaves on the small étale site of X: j_* 𝐆_{m,η} ⟶ ⨁_{x ∈ X_0} (i_x)_* 𝐙.

It is Stacks.EtaleCohomology.affineEtaleDivisorRestricted transferred along the inclusion of the affine étale site, which is cover dense and full and hence locally full, so CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom is a bijection. The source states the sequence for a smooth curve over an algebraically closed field; the hypotheses carried here — integral, normal, locally Noetherian — are all weaker, and are discharged in that setting by Stacks.EtaleCohomology.isLocallyNoetherian_of_isCurve and Stacks.EtaleCohomology.isNormal_of_isCurve_of_smooth.

Being data, this definition is not pinned down by its type: the zero morphism inhabits it too. What pins it down is Stacks.EtaleCohomology.whiskerLeft_divisorSequenceSecondMap together with Stacks.EtaleCohomology.divisorSequenceSecondMap_hom_app and Stacks.EtaleCohomology.affineEtaleDivisorApp_apply, which say that on sections over an affine étale X-scheme it is the family of orders of vanishing, and Stacks.EtaleCohomology.divisorSequenceSecondMap_eq_of_whiskerLeft, which says that no other morphism of sheaves does so.

def divisorSequenceSecondMap :
    (genericPointDirectImage.{u, v} X).obj
        (Stacks.Kummer.multiplicativeSheaf.{u, v} (Spec X.functionField)) ⟶
      closedPointDivisorSheaf.{u, v} X

Stacks.EtaleCohomology.multiplicativeDirectImageComparison_comp_divisorSequenceSecondMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 595. The attribute's comment: “the sequence is a complex: the two constructed maps compose to zero, for X integral, normal and locally Noetherian; the exactness of the sequence is not proved at this generality”.

The two maps of the fundamental exact sequence of Stacks 03RI compose to zero, so that 0 → 𝐆_{m,X} → j_* 𝐆_{m,η} → ⨁_{x ∈ X_0} (i_x)_* 𝐙 → 0 is a complex of abelian sheaves on the small étale site of X.

Both composites are morphisms into the sheaf ⨁_x (i_x)_* 𝐙, so restriction to the affine étale site is injective on them and it suffices to compare them there, where Stacks.EtaleCohomology.comparison_app_comp_affineEtaleDivisorApp applies.

theorem multiplicativeDirectImageComparison_comp_divisorSequenceSecondMap :
    multiplicativeDirectImageComparison.{u, v} (genericPointInclusion X) ≫
        divisorSequenceSecondMap.{u, v} X = 0

Stacks.EtaleCohomology.divisorSequenceSecondMapOfCurve, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 686. The attribute's comment: “the second map of the sequence for a smooth curve over a field, as a morphism of étale sheaves; the short exactness of the sequence is proved in the MiddleExactness file of this directory”.

The second map of the fundamental exact sequence of Stacks 03RI for a smooth curve over a field, which is the setting of the source. The three hypotheses of Stacks.EtaleCohomology.divisorSequenceSecondMap are discharged there: a curve is integral by AlgebraicGeometry.IsVariety and locally Noetherian by Stacks.EtaleCohomology.isLocallyNoetherian_of_isCurve, and a smooth curve is normal by Stacks.EtaleCohomology.isNormal_of_isCurve_of_smooth.

def divisorSequenceSecondMapOfCurve {k : Type u} [Field k] {X : Scheme.{u}}
    (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g] :
    (genericPointDirectImage.{u, v} X).obj
        (Stacks.Kummer.multiplicativeSheaf.{u, v} (Spec X.functionField)) ⟶
      closedPointDivisorSheaf.{u, v} X

Stacks.EtaleCohomology.multiplicativeDirectImageComparison_comp_divisorSequenceSecondMapOfCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/ClosedPointDivisorSheafSecondMap.lean, line 703. The attribute's comment: “the sequence is a complex for a smooth curve over a field: the two constructed maps compose to zero; the short exactness of the sequence is proved in the MiddleExactness file of this directory”.

The two maps of the fundamental exact sequence of Stacks 03RI compose to zero for a smooth curve over a field. This is Stacks.EtaleCohomology.multiplicativeDirectImageComparison_comp_divisorSequenceSecondMap with the hypotheses of that statement discharged as in Stacks.EtaleCohomology.divisorSequenceSecondMapOfCurve.

theorem multiplicativeDirectImageComparison_comp_divisorSequenceSecondMapOfCurve {k : Type u}
    [Field k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g] :
    multiplicativeDirectImageComparison.{u, v} (genericPointInclusion X) ≫
        divisorSequenceSecondMapOfCurve.{u, v} g = 0

Stacks.EtaleCohomology.fundamentalSequence_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/FundamentalExactSequence.lean, line 297.

Stacks Project, Tag 03RI. Let X be a smooth curve over a field, let η = Spec k(X) be its generic point with inclusion j : η ⟶ X, and let X_0 be the set of closed points of X with inclusions i_x : Spec κ(x) ⟶ X. Then

0 ⟶ 𝐆_{m,X} ⟶ j_* 𝐆_{m,η} ⟶ ⨁_{x ∈ X_0} (i_x)_* 𝐙 ⟶ 0

is a short exact sequence of abelian sheaves on the small étale site of X. The first map is the comparison morphism Stacks.EtaleCohomology.multiplicativeDirectImageComparison along j, which restricts an invertible global function on an étale X-scheme U to the generic fibre U ×_X η; the second is Stacks.EtaleCohomology.closedPointDivisorMap, the family of orders of vanishing.

Exactness at 𝐆_{m,X} is Stacks.EtaleCohomology.mono_multiplicativeDirectImageComparison_genericPointInclusion: the generic fibre is scheme-theoretically dense. Exactness in the middle is Stacks.EtaleCohomology.exact_fundamentalSequence, which rests on algebraic Hartogs on the normal scheme U. Exactness on the right is Stacks.EtaleCohomology.epi_closedPointDivisorMap: a divisor on a nonsingular curve is locally the divisor of a rational function, and the pullback of that function along an étale morphism has the prescribed orders of vanishing.

theorem fundamentalSequence_shortExact :
    (ShortComplex.mk (multiplicativeDirectImageComparison.{u, v} (genericPointInclusion X))
      (closedPointDivisorMap.{u, v} fX)
      (comparison_comp_closedPointDivisorMap.{u, v} fX)).ShortExact

Stacks.EtaleCohomology.injective_restrict_genericFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/FundamentalExactSequenceSections.lean, line 323. The attribute's comment: “exactness at Γ(U, 𝒪_U^*) of the sequence on sections over an étale X-scheme”.

Exactness of the fundamental exact sequence of Stacks 03RI at Γ(U, 𝒪_U^*), read on sections over an étale X-scheme U. On an integral scheme the generic fibre η ×_X U is scheme-theoretically dense in U, so an invertible global function on U is determined by its restriction to it.

This is the injectivity of the first map of the sequence 0 → Γ(U, 𝒪_U^*) → Γ(η ×_X U, 𝒪^*) → ⨁_{x ∈ X_0} Γ(x ×_X U, 𝐙) displayed in the proof of the source.

theorem injective_restrict_genericFibre :
    Function.Injective (Units.map
      (pullback.fst U.hom (genericPointInclusion X)).appTop.hom.toMonoidHom)

Stacks.EtaleCohomology.genericFibreDivisorSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/FundamentalExactSequenceSections.lean, line 346. The attribute's comment: “the second map on sections over an irreducible étale X-scheme”.

The second map of the fundamental exact sequence of Stacks 03RI, on sections over an irreducible étale X-scheme U: an invertible global function on the generic fibre η ×_X U is sent to the family of its orders of vanishing, the member at a closed point x being the locally constant 𝐙-valued map on the fibre x ×_X U recording the order of vanishing at each point of U over x.

The family has finite support, a rational function having finitely many zeros and poles, so it is an element of the direct sum ⨁_{x ∈ X_0} ((i_x)_* 𝐙)(U), the third term of the sequence displayed in the proof of the source.

def genericFibreDivisorSections :
    Additive ((Γ(pullback U.hom (genericPointInclusion X), ⊤))ˣ) →+
      DirectSum ↥(closedPoints X)
        fun x : closedPoints X => (integerSkyscraper.{u, v} X x.1).obj.obj (op U)

Stacks.EtaleCohomology.genericFibreDivisorSections_restrict_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/FundamentalExactSequenceSections.lean, line 376. The attribute's comment: “the sequence on sections over an irreducible étale X-scheme is a complex”.

The sequence of Stacks 03RI is a complex, read on sections over an irreducible étale X-scheme U: an invertible global function on U restricts to an invertible function on the generic fibre with no zeros and no poles, so its family of orders of vanishing is zero.

Together with Stacks.EtaleCohomology.injective_restrict_genericFibre this is the sequence 0 → Γ(U, 𝒪_U^*) → Γ(η ×_X U, 𝒪^*) → ⨁_{x ∈ X_0} Γ(x ×_X U, 𝐙) displayed in the proof of the source, exact at its left end and a complex at the middle.

theorem genericFibreDivisorSections_restrict_eq_zero (a : (Γ(U.left, ⊤))ˣ) :
    genericFibreDivisorSections.{u, v} U (Additive.ofMul (Units.map
      (pullback.fst U.hom (genericPointInclusion X)).appTop.hom.toMonoidHom a)) = 0

Stacks.EtaleCohomology.etaleGenericFibreOrd_appTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/GenericFibreFunctionFieldNaturality.lean, line 272. The attribute's comment: “the second map of the sequence is compatible with restriction along a morphism of étale X-schemes, read on the order of vanishing at a point”.

The order of vanishing of an invertible global function on the generic fibre is compatible with restriction along a morphism φ : U ⟶ V of the small étale site of X: restricting along Stacks.EtaleCohomology.etaleGenericFibreMap φ and taking the order of vanishing at a point y of U gives the order of vanishing at φ.left.base y.

theorem etaleGenericFibreOrd_appTop {X : Scheme.{u}} [IrreducibleSpace X] {U V : X.Etale}
    [IsIntegral U.left] [IsIntegral V.left] [IsLocallyNoetherian U.left]
    [IsLocallyNoetherian V.left] (φ : U ⟶ V) (y : U.left)
    (a : (Γ(pullback V.hom (genericPointInclusion X), ⊤))ˣ) :
    etaleGenericFibreOrd U y
        (Additive.ofMul (Units.map (etaleGenericFibreMap φ).appTop.hom.toMonoidHom a)) =
      etaleGenericFibreOrd V (φ.left.base y) (Additive.ofMul a)
Tag 03RJ, a lemma

Tag 03RJ in the Stacks Project.

Stacks.EtaleCohomology.isZero_rightDerived_genericPointDirectImage_multiplicativeSheaf_of_trdeg_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/GenericPointHigherDirectImageMultiplicative.lean, line 66. References: SGA 4½ Arcata (3.3.2), “more general”.

Stacks Project, Tag 03RJ. Let k be an algebraically closed field, let X be an integral scheme whose function field K = k(X) has transcendence degree one over k, and let j : Spec K ⟶ X be the inclusion of the generic point. Then

R^q j_* 𝐆_{m,K} = 0 for every q ≥ 1.

A smooth curve over k satisfies the hypotheses, by AlgebraicGeometry.trdeg_functionField_eq_one, so this is more general than the tag.

theorem isZero_rightDerived_genericPointDirectImage_multiplicativeSheaf_of_trdeg_eq_one
    (k : Type u) [Field k] [IsAlgClosed k] {X : Scheme.{u}} [IsIntegral X]
    [Algebra k X.functionField] (hK : Algebra.trdeg k X.functionField = 1)
    (q : ℕ) (hq : 1 ≤ q) :
    IsZero (((etaleAbelianDirectImage.{u, u + 1} (genericPointInclusion X)).rightDerived q).obj
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField)))

Stacks.EtaleCohomology.isZero_rightDerived_genericPointDirectImage_multiplicativeSheaf_smoothCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/GenericPointHigherDirectImageSmoothCurveVanishing.lean, line 82.

Stacks Project, Tag 03RJ. Let k be an algebraically closed field, X a smooth curve over k with structure morphism g, η = Spec k(X) its generic point and j : η ⟶ X the inclusion of the generic point. Then

R^q j_* 𝐆_{m,η} = 0 for every q ≥ 1.

No hypothesis is carried. The higher direct image is killed on the étale neighbourhoods by Stacks.EtaleCohomology.isZero_rightDerived_etaleAbelianDirectImage_multiplicativeSheaf_of_field, which leaves the vanishing of H^q_étale(Spec L, 𝐆_m) at each finite separable extension L of k(X). That is Stacks 03RG, since L has transcendence degree one over k.

Smoothness is in the statement because the source assumes it. The proof does not use it: the curve hypothesis is enough.

theorem isZero_rightDerived_genericPointDirectImage_multiplicativeSheaf_smoothCurve
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k))
    [IsCurve k g] [Smooth g] (q : ℕ) (hq : 1 ≤ q) :
    IsZero (((etaleAbelianDirectImage.{u, u + 1} (genericPointInclusion X)).rightDerived q).obj
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField)))
Tag 03RK, a lemma

Tag 03RK in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/MultiplicativeGroupHigherVanishing.lean, line 245. The attribute's comment: “vanishing of the positive-degree étale cohomology of the direct image of 𝐆_m along the generic point of a curve over an algebraically closed field”.

Stacks Project, Tag 03RK. Let X be a curve over an algebraically closed field k, with structure morphism g, let η = Spec k(X) be its generic point and j : η ⟶ X the inclusion of the generic point. Then

H^p_étale(X, j_* 𝐆_{m,η}) = 0 for every p ≥ 1.

The source assumes X smooth; the proof does not use smoothness, so it is not assumed and the statement is more general than the tag. The smooth case, with the source's hypotheses verbatim, is Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf_smoothCurve.

The source argues by the Leray spectral sequence E₂^{p,q} = H^p(X, R^q j_* 𝐆_{m,η}), whose q ≥ 1 rows vanish by Stacks 03RJ and whose abutment H^{p+q}(η, 𝐆_m) vanishes for p + q ≥ 1 by Stacks 03RG. The proof here is the edge isomorphism of that spectral sequence, Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf_of_isZero_rightDerived, with both inputs proved: Stacks 03RJ is Stacks.EtaleCohomology.isZero_rightDerived_genericPointDirectImage_multiplicativeSheaf_of_trdeg_eq_one, whose premise is AlgebraicGeometry.trdeg_functionField_eq_one, and Stacks 03RG at the function field of X is Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_spec_functionField.

theorem subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf {k : Type u} [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsCurve k g]
    (p : ℕ) (hp : 1 ≤ p) :
    Subsingleton (Sheaf.H.{u + 1, u + 1} ((genericPointDirectImage.{u, u + 1} X).obj
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField))) p)

Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf_smoothCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/MultiplicativeGroupSmoothCurveVanishing.lean, line 77.

Stacks Project, Tag 03RK. Let X be a smooth curve over an algebraically closed field k, let η = Spec k(X) be its generic point and j : η ⟶ X the inclusion. Then

H^p_étale(X, j_* 𝐆_{m,η}) = 0 for every p ≥ 1.

This is Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf, the collapse of the Leray spectral sequence to its edge isomorphism, with Stacks 03RJ and Stacks 03RG proved.

theorem subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf_smoothCurve
    {k : Type u} [Field k] [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k))
    [IsCurve k g] [Smooth g] (p : ℕ) (hp : 1 ≤ p) :
    Subsingleton (Sheaf.H.{u + 1, u + 1} ((genericPointDirectImage.{u, u + 1} X).obj
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField))) p)
Tag 03RL, a lemma

Tag 03RL in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_sheafH_sigma_closedPointPushforward_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedPointDirectSumCohomology.lean, line 178. The attribute's comment: “vanishing of the positive-degree étale cohomology of the direct sum over the closed points of the pushforwards of the constant integer sheaf”.

Stacks Project, Tag 03RL. Let X be a quasi-compact, quasi-separated scheme locally of finite type over an algebraically closed field — a smooth curve over an algebraically closed field, for instance. For every q ≥ 1 the degree-q étale cohomology of ⨁_{x ∈ X₀} (i_x)_* ℤ vanishes, the sum being over the closed points X₀ of X and i_x the inclusion of a closed point.

public theorem subsingleton_sheafH_sigma_closedPointPushforward_smallEtale {k : Type u} [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [LocallyOfFiniteType g]
    [CompactSpace X] [QuasiSeparatedSpace X] (q : ℕ) (hq : 1 ≤ q) :
    Subsingleton (Sheaf.H.{u + 1, u + 1}
      (∐ fun x : closedPoints X ↦
        (smallEtalePushforwardAb (X.fromSpecResidueField x.1)).obj
          ((constantSheaf (smallEtaleTopology (Spec (X.residueField x.1))) Ab.{u + 1}).obj
            (AddCommGrpCat.of (ULift.{u + 1} ℤ)))) q)
Tag 03RM, a theorem

Tag 03RM in the Stacks Project.

Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_smoothCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/MultiplicativeGroupHigherVanishing.lean, line 281. The attribute's comment: “vanishing of the degree ≥ 2 étale cohomology of 𝐆_m on a smooth curve over an algebraically closed field, over Tag 03RI, Tag 03RJ and Tag 03RG as hypotheses”.

Stacks Project, Tag 03RM. Let X be a smooth curve over an algebraically closed field k, let η = Spec k(X) be its generic point and j : η ⟶ X the inclusion of the generic point. Then

H^q_étale(X, 𝐆_m) = 0 for every q ≥ 2.

The proof is the long exact sequence of étale cohomology attached to the divisor sequence 0 → 𝐆_{m,X} → j_* 𝐆_{m,η} → ⨁_{x ∈ X_0} i_{x,*} 𝐙 → 0 of Stacks 03RI: the segment H^{q-1}(X, ⨁_x i_{x,*} 𝐙) → H^q(X, 𝐆_{m,X}) → H^q(X, j_* 𝐆_{m,η}) has both outer groups zero, the left one by Stacks 03RL since q - 1 ≥ 1, the right one by Stacks 03RK.

Stacks 03RL is used from the library, as Stacks.EtaleCohomology.subsingleton_sheafH_sigma_closedPointPushforward_smallEtale, and the vanishing of H^q(X, j_* 𝐆_{m,η}) is the edge argument Stacks.EtaleCohomology.subsingleton_sheafH_genericPointDirectImage_multiplicativeSheaf_of_isZero_rightDerived (which is how Stacks 03RK is proved above), applied to the hypotheses h03RJ (Stacks 03RJ) and h03RG (Stacks 03RG) carried here. The divisor sequence itself is carried as its second map d with hzero and hSE (Stacks 03RI); its first map is the comparison morphism Stacks.EtaleCohomology.multiplicativeDirectImageComparison along j, which restricts an invertible global function on an étale X-scheme U to the generic fibre U ×_X η.

theorem subsingleton_sheafH_multiplicativeSheaf_smoothCurve {k : Type u} [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g]
    (d : (genericPointDirectImage.{u, u + 1} X).obj
          (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField)) ⟶
        closedPointDivisorSheaf.{u, u + 1} X)
    (hzero : multiplicativeDirectImageComparison.{u, u + 1} (genericPointInclusion X) ≫ d = 0)
    (hSE : (ShortComplex.mk
      (multiplicativeDirectImageComparison.{u, u + 1} (genericPointInclusion X)) d
      hzero).ShortExact)
    (h03RJ : ∀ q : ℕ, 0 < q →
      IsZero (((etaleAbelianDirectImage.{u, u + 1} (genericPointInclusion X)).rightDerived q).obj
        (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField))))
    (h03RG : ∀ q : ℕ, 1 ≤ q → Subsingleton (Sheaf.H.{u + 1, u + 1}
      (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} (Spec X.functionField)) q))
    (q : ℕ) (hq : 2 ≤ q) :
    Subsingleton
      (Sheaf.H.{u + 1, u + 1} (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} X) q)

Stacks.EtaleCohomology.subsingleton_sheafH_multiplicativeSheaf_of_smoothCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/MultiplicativeGroupSmoothCurveVanishing.lean, line 94.

Stacks Project, Tag 03RM. Let X be a smooth curve over an algebraically closed field k. Then

H^q_étale(X, 𝐆_m) = 0 for every q ≥ 2.

The long exact sequence of the fundamental exact sequence of Stacks 03RI, Stacks.EtaleCohomology.shortExact_divisorSequenceOfCurve, places H^q(X, 𝐆_m) between H^{q-1}(X, ⨁_{x ∈ X_0} i_{x,*} 𝐙), zero by Stacks 03RL, and H^q(X, j_* 𝐆_{m,η}), zero by Stacks 03RK; the latter rests on Stacks 03RJ and Stacks 03RG, supplied here.

theorem subsingleton_sheafH_multiplicativeSheaf_of_smoothCurve {k : Type u} [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (g : X ⟶ Spec (.of k)) [IsCurve k g] [Smooth g]
    (q : ℕ) (hq : 2 ≤ q) :
    Subsingleton
      (Sheaf.H.{u + 1, u + 1} (Stacks.Kummer.multiplicativeSheaf.{u, u + 1} X) q)
Sources
LeanStacks.EtaleCohomology.epi_divisorSequenceSecondMapOfCurve · Stacks.EtaleCohomology.exact_divisorSequenceOfCurve · Stacks.EtaleCohomology.shortExact_divisorSequenceOfCurve · Stacks.EtaleCohomology.closedPointDivisorSections · Stacks.EtaleCohomology.closedPointDivisorSections_restrict_eq_zero · Stacks.EtaleCohomology.integerSkyscraperDivisorOfPoint_map · Stacks.EtaleCohomology.closedPointDivisorPresheafSection_map · Stacks.EtaleCohomology.closedPointDivisorPresheafSection_restrict_eq_zero

Section59.69 Picard groups of curves#

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

Tag 03RQ, a lemma

Tag 03RQ in the Stacks Project.

AlgebraicGeometry.etaleCohomology_rootsOfUnity_smoothProjectiveCurve_of_genus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/RootsOfUnityCurvesFinal.lean, line 91.

Stacks Project, Tag 03RQ. Let X be a smooth projective curve of genus g over an algebraically closed field k and let n ∈ k^*. Then H⁰_ét(X, μ_n) = μ_n(k), H¹_ét(X, μ_n) = Pic⁰(X)[n] ≅ (𝐙/n𝐙)^{2g}, H²_ét(X, μ_n) ≅ 𝐙/n𝐙 (by the degree), H^q_ét(X, μ_n) = 0 for q ≥ 3; and the same groups for the constant sheaf 𝐙/n𝐙: 𝐙/n𝐙, (𝐙/n𝐙)^{2g}, 𝐙/n𝐙 and 0 for q ≥ 3.

theorem etaleCohomology_rootsOfUnity_smoothProjectiveCurve_of_genus (hn : IsUnit (n : k)) :
    Function.Bijective (baseRootsToEtaleH0 E k X hX f n) ∧
      Function.Bijective (etaleH1RootsOfUnityToCurvePicardDegreeZeroTorsion k X f E hX n hn) ∧
      (∃ e : Sheaf.H (kummerSmallEtale E X hX n).X₁ 2 ≃+ ZMod n,
        ∀ x, e (etaleH2RootsOfUnityFromPicard k X f E hX n hn x) = picardDegreeZMod k X f n x) ∧
      (∀ q, 3 ≤ q → Subsingleton (Sheaf.H (kummerSmallEtale E X hX n).X₁ q)) ∧
      Nonempty (Sheaf.H (smallEtaleConstantZModSheaf E X hX n) 0 ≃+ ZMod n) ∧
      Nonempty (Sheaf.H (smallEtaleConstantZModSheaf E X hX n) 1 ≃+
        (Fin (2 * genus f) → ZMod n)) ∧
      Nonempty (Sheaf.H (smallEtaleConstantZModSheaf E X hX n) 2 ≃+ ZMod n) ∧
      ∀ q, 3 ≤ q → Subsingleton (Sheaf.H (smallEtaleConstantZModSheaf E X hX n) q)

Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/SecondCohomologyOfRootsOfUnity.lean, line 252. The attribute's comment: “the q = 2 clause, that H^2_etale(X, mu_n) of a smooth proper curve over an algebraically closed field is cyclic of order n, normalised by the degree through sheafHTwoRootsOfUnityAddEquivZMod_curveKummerCoboundary; the q = 0 clause is AlgebraicGeometry.baseRootsToEtaleH0_bijective_of_isCurve and the q > 2 clause is subsingleton_sheafH_rootsOfUnitySheaf_of_smoothCurve, while the q = 1 clause awaits Stacks 03P8 for the small etale site”. References: SGA 4½ Arcata (6.2.1), “partial”.

[Stacks, Tag 03RQ], the case q = 2. Let X be a smooth proper curve over an algebraically closed field k and let n be invertible in k. Then H²_étale(X, μ_n) is cyclic of order n.

The Kummer coboundary presents H²_étale(X, μ_n) as the quotient of H¹_étale(X, 𝐆_m) by its n-th multiples — it is onto because H²_étale(X, 𝐆_m) = 0 ([Stacks, Tag 03RM]) and its kernel is the n-th multiples because the preceding map of the long exact sequence is multiplication by n — and the degree identifies that quotient with 𝐙/n𝐙, by Stacks.EtaleCohomology.ker_curveKummerCoboundary_eq_ker_sheafHOneMultiplicativeDegreeMod.

The normalisation of this isomorphism is Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod_curveKummerCoboundary.

def sheafHTwoRootsOfUnityAddEquivZMod :
    Sheaf.H.{u + 1} (rootsOfUnitySheaf.{u, u + 1} X n) 2 ≃+ ZMod n

Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod_curveKummerCoboundary, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/SecondCohomologyOfRootsOfUnity.lean, line 269. The attribute's comment: “the normalisation of the q = 2 clause by the degree: the coordinate of the Kummer coboundary of a class of H^1_etale(X, G_m) is the degree of the corresponding divisor class modulo n”.

The normalisation of Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod: the coordinate of the Kummer coboundary of a class in H¹_étale(X, 𝐆_m) is the degree of that class modulo n. Together with Stacks.EtaleCohomology.exists_curveKummerCoboundary_eq, which says that every class in H²_étale(X, μ_n) is a coboundary, this fixes the isomorphism and not merely its existence.

theorem sheafHTwoRootsOfUnityAddEquivZMod_curveKummerCoboundary
    (a : Sheaf.H.{u + 1} (multiplicativeSheaf.{u, u + 1} X) 1) :
    sheafHTwoRootsOfUnityAddEquivZMod g hn (curveKummerCoboundary g hn a) =
      sheafHOneMultiplicativeDegreeMod g n a

AlgebraicGeometry.baseRootsToEtaleH0_bijective_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/RootsOfUnityCurve.lean, line 64. The attribute's comment: “the q = 0 clause, H^0_etale(X, mu_n) = mu_n(k); the clauses for q = 1, q = 2 and q >= 3 need Stacks 03P8 and 03RM, which the library does not have”.

Stacks Project, Tag 03RQ, the case q = 0. Let X be a smooth projective curve over an algebraically closed field k and let n be invertible in k. Pullback along the structure morphism is a bijection from the n-th roots of unity of k onto H⁰_étale(X, μ_n).

public theorem baseRootsToEtaleH0_bijective_of_isCurve
    (B : BigEtaleSite.{u}) (k : Type u) [Field k] [IsAlgClosed k]
    (X : Scheme.{u}) (hX : B.Contains X) (f : X ⟶ Spec (.of k))
    [IsCurve k f] [Smooth f] [IsProjectiveVariety k f] (n : ℕ) (hn : IsUnit (n : k))
    [HasSheafify (SmallEtale.topology B X hX) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u})] :
    Function.Bijective (baseRootsToEtaleH0 B k X hX f n)

Stacks.Kummer.subsingleton_sheafH_rootsOfUnitySheaf_of_isCurve, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Picard/RootsOfUnitySecondCohomology.lean, line 164. The attribute's comment: “the clause q >= 3: H^q_etale(X, mu_n) = 0 for every q >= 3”. References: SGA 4½ Arcata (3.3.5), “partial”.

Stacks Project, Tag 03RQ, the clause q ≥ 3. Let X be a smooth projective curve over an algebraically closed field k and let n ≥ 1 be invertible in k. Then H^q_étale(X, μ_n) = 0 for every q ≥ 3.

The Kummer sequence places H^q(X, μ_n) between H^{q-1}(X, 𝐆_m) and H^q(X, 𝐆_m), both zero by Stacks 03RM since q - 1 ≥ 2. Projectivity is not used.

theorem subsingleton_sheafH_rootsOfUnitySheaf_of_isCurve (q : ℕ) (hq : 3 ≤ q) :
    Subsingleton (Sheaf.H.{u + 1, u + 1} (rootsOfUnitySheaf.{u, u + 1} X n) q)
Tag 0AMB, a lemma

Tag 0AMB in the Stacks Project.

Stacks.EtaleCohomology.equiv_rootsOfUnityPullbackMap_eq_degreeOver_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/RootsOfUnityPullbackDegree.lean, line 226. The attribute's comment: “with two inputs carried as hypotheses, neither of them about the conclusion: SX/SY, the q = 2 clause of Stacks 03RQ with its normalisation, since the library has only the q = 0 clause and the q = 2 clause needs Stacks 03P8 and 03RM; and c, the class of a line bundle in H¹_ét(-, 𝐆_m) with its naturality, which is the Picard half of Stacks 03P8”.

[Stacks, Tag 0AMB]. Let k be an algebraically closed field, let π : X ⟶ Y be a nonconstant morphism of smooth proper curves over k, and let n ≥ 1 be invertible in k. In the coordinates of Stacks.EtaleCohomology.RootsOfUnityH2Degree, which identify both H²_ét(Y, μ_n) and H²_ét(X, μ_n) with ℤ/n, the pullback

π^* : H²_ét(Y, μ_n) ⟶ H²_ét(X, μ_n)

is multiplication by the degree of π, the degree deg(X/Y) = [R(X) : R(Y)] of the extension of function fields ([Stacks, Tag 02NY]).

The proof is the source's. A class in H²_ét(Y, μ_n) is the Kummer coboundary of the class of a line bundle L on Y. Restriction along π commutes with the Kummer coboundary, by Stacks.Kummer.etaleCohomologyRestrictionMap_kummerExtClass, and carries the class of L to the class of π^*L, so the coordinate of the restricted class is the degree of π^*L. That degree is deg(X/Y) times the degree of L by AlgebraicGeometry.curveDegree_pullback_eq_degreeOver_mul, which is where nonconstancy of π is used, and the degree of L is the coordinate of the original class.

theorem equiv_rootsOfUnityPullbackMap_eq_degreeOver_mul (c : LineBundleClass.{u, v, w})
    (k : Type u) [Field k] [IsAlgClosed k] {X Y : Scheme.{u}} (πX : X ⟶ Spec (.of k))
    (πY : Y ⟶ Spec (.of k)) [IsCurve k πX] [IsCurve k πY] [IsProper πX] [IsProper πY]
    [Smooth πX] [Smooth πY] (π : X ⟶ Y) (hπ : π ≫ πY = πX)
    (hnc : ¬ ∃ y : Y, ∀ x : X, π.base x = y) {n : ℕ} (hn0 : n ≠ 0) (hnk : IsUnit (n : k))
    [HasExt.{w} (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    [HasExt.{w} (Sheaf Y.smallEtaleTopology AddCommGrpCat.{max (u + 1) v})]
    (SX : RootsOfUnityH2Degree.{u, v, w} c k πX n)
    (SY : RootsOfUnityH2Degree.{u, v, w} c k πY n)
    (x : Sheaf.H.{w} (rootsOfUnitySheaf.{u, v} Y n) 2) :
    SX.equiv (rootsOfUnityPullbackMap.{u, v, w} π n 2 x) =
      ((@degreeOver X Y π _ _ (locallyOfFiniteType_of_isCurve_comp k πX πY π hπ)
          (isDominant_of_not_constant k πX πY π hnc) : ℕ) : ZMod n) * SY.equiv x

Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod_rootsOfUnityRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/SecondCohomologyPullbackDegree.lean, line 799. The attribute's comment: “pullback on the second etale cohomology of mu_n along a nonconstant morphism of smooth proper curves over an algebraically closed field is multiplication by the degree of the morphism, in the coordinates of the q = 2 clause of Stacks 03RQ (sheafHTwoRootsOfUnityAddEquivZMod), which identify both groups with Z/nZ and are normalised by the divisor-class degree”.

[Stacks, Tag 0AMB]. Let k be an algebraically closed field, let π : X ⟶ Y be a nonconstant morphism of smooth proper curves over k, and let n be invertible in k. In the coordinates of Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod, which identify both H²_étale(Y, μ_n) and H²_étale(X, μ_n) with 𝐙/n𝐙, the pullback

π^* : H²_étale(Y, μ_n) ⟶ H²_étale(X, μ_n)

is multiplication by the degree deg(X/Y) = [R(X) : R(Y)] of the extension of function fields ([Stacks, Tag 02NY]).

The proof is the source's. Every class of H²_étale(Y, μ_n) is the Kummer coboundary of a class a of H¹_étale(Y, 𝐆_m) ([Stacks, Tag 03RM]), and the coordinate of that coboundary is the degree of a modulo n. Restriction along π commutes with the Kummer coboundary (Stacks.Kummer.etaleCohomologyRestrictionMap_kummerExtClass), so the coordinate of the restricted class is the degree of the restriction of a, which is deg(X/Y) times the degree of a by Stacks.EtaleCohomology.sheafHOneMultiplicativeDegreeMod_multiplicativeRestriction — and that is where nonconstancy of π is used, through the rank-one case of [Stacks, Tag 0AYZ].

theorem sheafHTwoRootsOfUnityAddEquivZMod_rootsOfUnityRestriction
    (x : Sheaf.H.{u + 1} (Stacks.Kummer.rootsOfUnitySheaf.{u, u + 1} Y n) 2) :
    sheafHTwoRootsOfUnityAddEquivZMod gX hn
        (rootsOfUnityRestriction.{u, u + 1, u + 1} π n 2 x) =
      ((@degreeOver X Y π _ _ (locallyOfFiniteType_of_isCurve_comp k gX gY π hπ)
            (isDominant_of_not_constant k gX gY π hnc) : ℕ) : ZMod n) *
        sheafHTwoRootsOfUnityAddEquivZMod gY hn x
Tag 03RR, a lemma

Tag 03RR in the Stacks Project.

AlgebraicGeometry.etaleCohomology_rootsOfUnity_affineSmoothCurve_of_compactification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Curves/RootsOfUnityCurvesFinal.lean, line 66.

Stacks Project, Tag 03RR. Let X be an affine smooth curve over an algebraically closed field k, let n ∈ k^*, and let j : X ⟶ X̄ be a smooth projective compactification, with g the genus of X̄ and r the number of points of X̄ ∖ X. Then 1. H⁰_ét(X, μ_n) = μ_n(k); 2. H¹_ét(X, μ_n) ≅ (𝐙/n𝐙)^{2g + r - 1}; 3. H^q_ét(X, μ_n) = 0 for q ≥ 2.

theorem etaleCohomology_rootsOfUnity_affineSmoothCurve_of_compactification (hn : IsUnit (n : k))
    [IsAffine X] {Xbar : Scheme.{u}} (fbar : Xbar ⟶ Spec (.of k)) [IsCurve k fbar] [Smooth fbar]
    [IsProjectiveVariety k fbar] (j : X ⟶ Xbar) [IsOpenImmersion j] (hj : j ≫ fbar = f)
    (r : ℕ) (hr : Nat.card ↥(Set.range j.base)ᶜ = r) :
    Function.Bijective (baseRootsToEtaleH0 E k X hX f n) ∧
      Nonempty (Sheaf.H (kummerSmallEtale E X hX n).X₁ 1 ≃+
        (Fin (2 * genus fbar + r - 1) → ZMod n)) ∧
      ∀ q, 2 ≤ q → Subsingleton (Sheaf.H (kummerSmallEtale E X hX n).X₁ q)

AlgebraicGeometry.etaleH0EquivRootsOfUnitySections_val, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/RootsOfUnity.lean, line 189. The attribute's comment: “degree_zero”.

The comparison is the canonical evaluation of degree-zero cohomology at the final étale object, followed by the inclusion of the kernel into the units sheaf.

theorem etaleH0EquivRootsOfUnitySections_val
    (B : BigEtaleSite.{u}) (X : Scheme.{u}) (hX : B.Contains X)
    (n : ℕ)
    [HasSheafify (SmallEtale.topology B X hX) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u})]
    (x : Sheaf.H.{w, u}
      (rootsOfUnitySheaf (SmallEtale.topology B X hX)
        (SmallEtale.toScheme B X hX)
        (unitsPresheaf_isSheaf_smallEtale B X hX) n) 0) :
    (etaleH0EquivRootsOfUnitySections B X hX n x).1 =
      Additive.toMul
        ((Limits.kernel.ι
          (powerSheaf (SmallEtale.topology B X hX)
            (SmallEtale.toScheme B X hX)
            (unitsPresheaf_isSheaf_smallEtale B X hX) n)).hom.app
          (Opposite.op (SmallEtale.final B X hX))
          ((Sheaf.H.equiv₀
            (rootsOfUnitySheaf (SmallEtale.topology B X hX)
              (SmallEtale.toScheme B X hX)
              (unitsPresheaf_isSheaf_smallEtale B X hX) n)
            (SmallEtale.finalIsTerminal B X hX)) x))

AlgebraicGeometry.rootsOfUnitySections_bijective_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/RootsOfUnity.lean, line 230. The attribute's comment: “degree_zero”.

Roots of unity in global sections of an integral scheme over an algebraically closed field are precisely the constants.

theorem rootsOfUnitySections_bijective_of_isIntegral
    (k : Type u) [Field k] [IsAlgClosed k]
    {X : Scheme.{u}} [IsIntegral X] (f : X ⟶ Spec (.of k))
    (n : ℕ) (hn : 0 < n) :
    Function.Bijective
      ((rootsOfUnitySections n).map f.op)

AlgebraicGeometry.baseRootsToEtaleH0_bijective_of_isIntegral, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DegreeZero/RootsOfUnity.lean, line 270. The attribute's comment: “degree_zero”.

The canonical pullback from the field's roots of unity to degree-zero étale cohomology is bijective over an algebraically closed field.

theorem baseRootsToEtaleH0_bijective_of_isIntegral
    (B : BigEtaleSite.{u}) (k : Type u) [Field k] [IsAlgClosed k]
    (X : Scheme.{u}) [IsIntegral X] (hX : B.Contains X)
    (f : X ⟶ Spec (.of k)) (n : ℕ) (hn : 0 < n)
    [HasSheafify (SmallEtale.topology B X hX) AddCommGrpCat.{u}]
    [HasExt.{w} (Sheaf (SmallEtale.topology B X hX) AddCommGrpCat.{u})] :
    Function.Bijective (baseRootsToEtaleH0 B k X hX f n)
Sources
LeanAlgebraicGeometry.etaleCohomology_rootsOfUnity_smoothProjectiveCurve_of_genus · Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod · Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod_curveKummerCoboundary · AlgebraicGeometry.baseRootsToEtaleH0_bijective_of_isCurve · Stacks.Kummer.subsingleton_sheafH_rootsOfUnitySheaf_of_isCurve · Stacks.EtaleCohomology.equiv_rootsOfUnityPullbackMap_eq_degreeOver_mul · Stacks.EtaleCohomology.sheafHTwoRootsOfUnityAddEquivZMod_rootsOfUnityRestriction · AlgebraicGeometry.etaleCohomology_rootsOfUnity_affineSmoothCurve_of_compactification

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.