Étale cohomology

Étale sites, coefficient sheaves and étale cohomology. Covers stalks, pullback and pushforward, constructible sheaves, monodromy and local comparison results.

The constant-sheaf inverse-image comparison is defined by uniqueness of left adjoints. Its adjoint sends each original constant section to the same section on the base-changed etale scheme. In particular it preserves the…

Transport the constructed exact inverse image of integer module sheaves through the equivalence with abelian sheaves. Direct image is the actual restriction along étale base change. This connects these functors to mathli…

Transport the proved module/set inverse-image comparison through the actual integer-module equivalence defining abelian inverse image. The comparison retains the original abelian sheaves and the existing set inverse imag…

Scalar endomorphisms of the coefficient group induce scalar endomorphisms of its image. This constructs the module structure and proves linearity of the induced maps, without changing the underlying additive groups.

The finite levels are the existing derived cohomology of the constant ℤ/ℓ^(n+1)ℤ sheaves on the small étale site. Coefficient reduction gives the transition maps. Classical integral ℓ-adic cohomology is the group of comp…

For every closed immersion i : Z ⟶ X, actual direct image induces Hⁿ(X, iF) ≃ Hⁿ(Z, F) in all degrees. This follows from the exact inverse-image/direct-image adjunction and its action on the constant integer sheaf. The r…

Restriction along ℤ → R and the equivalence between ℤ-modules and abelian groups supply both adjoints to the coefficient-forgetting functor. This also supplies sheaf composition on sites whose object universe is larger t…

All site and Ext hypotheses are supplied by the existing affine étale comparison and Grothendieck abelian category instances. The underlying groups are Sheaf.H on the small étale site.

The connecting morphism is mathlib's Ext connecting homomorphism. Its linearity follows from naturality under scalar multiplication on the short exact sequence. Exactness is inherited from the existing classical cohomolo…

Every positive-degree class in the actual Ext-defined cohomology presheaf over a field vanishes after a connected finite étale cover. The proof uses the actual injective presentation and the Ext long exact sequence. In d…

Contravariant pullback turns the opposite deck group into an action on actual sections. The existing finite-field/deck comparison identifies this action with the usual Galois action on units for the actual Gm sheaf. This…

A lift over a finite Galois field extension of a Galois-invariant quotient section can be corrected to an invariant lift when the kernel is the actual unit sheaf. The correction is obtained from its actual difference coc…

A closed global section of an exact complex of abelian sheaves over a field becomes an actual boundary after a connected finite étale cover. Applying this to an injective resolution supplies finite-cover local primitives…

We use the finite constant groups of circle elements killed by (n+1)!. Their inclusions define a cofinal system of finite cyclic coefficients. The groups below are the direct limit of the actual derived étale cohomology…

The free abelian sheaves used in mathlib's Sheaf.cohomologyPresheaf corepresent evaluation. We record this equivalence and its two naturalities so that local lifting of sections can be applied to the actual Ext groups.

For a complex K of abelian sheaves on the small étale site, the Hom complex from the constant integer sheaf in degree zero identifies naturally with the complex obtained by taking actual global sections degreewise. The r…

The already constructed lifting of global sections supplies preservation of epimorphisms by the actual global-sections functor. Its constant-sheaf adjunction supplies preservation of kernels, hence exactness. For abelian…

A given InjectiveResolution F is extended from nonnegative to integer degrees by the existing zero-extension functor. Its actual augmentation becomes a quasi-isomorphism from the single complex of F, and the extended res…

The cover is the spectrum of the actual monic quotient R[T]/(T^n-u). Its étaleness is reused from the algebraic-curve library. Lying over proves surjectivity, and the adjoined root is explicitly a unit. These are the geo…

A global unit has an nth root on an actual finite étale surjective cover when n is positive and invertible. We pull the explicit affine root cover back along the canonical map to the spectrum of global sections. Thus the…

For a closed immersion and its open complement, the localization short exact sequence gives a coefficient-linear long exact sequence Hⁿ(X, j!jF) → Hⁿ(X, F) → Hⁿ(Z, iF) → Hⁿ⁺¹(X, j!jF). The closed term is the actual class…

The underlying additive groups are mathlib's CategoryTheory.Sheaf.H. Scalar multiplication is induced by multiplication on the coefficient sheaf. The module structures are bundled in ModuleCat, avoiding competing global…

We restrict the existing fppf sheaf of units from the algebraic-curve library. Its descent proof is reused unchanged. Sections are the actual units of the actual scheme's global section ring, with ordinary pullback. The…

Mapping a zero-extended complex by a zero-preserving functor commutes with extension: the comparison uses extendXIso in nonnegative degrees and actual zero-object witnesses in negative degrees. This is a constructed chai…

The actual finite coefficients carry the action of ℤ[ℓ] by reduction. This induces actions on their ordinary étale cohomology groups. The transition maps are linear, so the inverse limit carries the same scalar action. R…

The inverse limit is a subgroup of the product. Keeping its group operations independent of the concrete Ext groups avoids unfolding cohomology constructions when checking the elementary compatibility equations.

A finite locally constant set sheaf on a quasi-compact scheme becomes represented by a finite étale scheme after ordinary restriction to one affine surjective étale cover. We combine a finite affine family of local repre…

A finite locally constant sheaf has a finite étale local representer over a faithfully flat affine étale cover. Its universal section constructs the full algebra descent data. The invariant algebra gives a finite étale s…

An actual representer on an affine étale cover supplies the geometric action. Tensor coordinates then construct the algebra overlap equivalence and prove its diagonal and full cocycle laws. These laws are derived from th…

A finite constructible stratification is adapted to a module sheaf when its inverse image on each actual locally closed stratum is finite type locally constant. Constructibility requires such a stratification on every af…

A morphism from a finite type constant module sheaf to a constant module sheaf is, on an actual étale covering, induced by a module homomorphism. The models and their commutative squares are constructed from finite local…

If an epimorphism onto the quotient of a short exact sequence lifts to its middle term, the middle term is a cokernel of a map from the kernel of that epimorphism to the sum of its source and the subobject. This supplies…

Over noetherian coefficients, finite type locally constant sheaves are closed under extensions. A finite free presentation of the quotient lifts on an actual étale cover. The middle term then has the cokernel presentatio…

Over a connected base, the Galois representative of the fiber of a finite étale scheme supplies a connected finite étale surjective cover. Evaluation of all morphisms from that representative becomes a coproduct decompos…

The existing category FiniteEtale X embeds fully faithfully into sheaves of sets on the actual small étale site. The geometric stalk of the represented sheaf is naturally isomorphic to the underlying finite set of EFG's…

A finite covering by constructible immersed pieces with finite type locally constant restrictions admits a disjoint adapted stratification. We first partition the images and then take actual fiber products with the origi…

The represented-sheaf functor gives an equivalence from finite étale schemes over an arbitrary scheme to the full subcategory of finite locally constant sheaves on its small étale site. Full faithfulness is the existing…

A sheaf is finite locally constant if it is a constant sheaf of a finite set on an actual étale cover. The model may depend on the member of the cover. This property is local for the étale topology and is preserved by ar…

On a connected scheme, a module sheaf with finite locally constant underlying set sheaf is trivialized by a connected finite étale surjective cover. The constant module is constructed from sections on that cover, and the…

A locally closed subset is closed in its open coborder. Its vanishing ideal therefore gives an actual closed subscheme of that open subscheme, and the composite immersion into the original scheme has precisely the given…

Local finite étale representers on a locally directed open cover have canonical transition maps preserving their universal sections. The small-site hypercover therefore glues those sections. Cartesian local comparisons i…

Zero extension along a quasi-compact open immersion preserves constructibility. Closed direct image does so when the complementary open image is retrocompact. Their composite treats locally closed immersions presented by…

A common finite adapted stratification reduces both operations to their finite type locally constant counterparts. The argument applies on every affine open without any noetherian hypothesis on the scheme.

The actual representing equivalences on the small étale sites determine all transition maps and their cartesian squares. Relative gluing then constructs a finite étale scheme on the whole base, whose restrictions are the…

An étale trivialization gives actual finite étale representers of the restricted presheaf. Its representing equivalence is natural on the local small site, so its universal section can be used to construct descent maps.…

On a qcqs scheme, affine-local constructibility is equivalent to a finite adapted stratification. On any scheme it is Zariski local. Pullback along any scheme morphism preserves constructibility: affine neighborhoods of…

Local constancy means that an actual étale cover trivializes the sheaf as a sheafification of a constant presheaf. A predicate on the constant models allows the same base-change and cover-refinement proofs to treat arbit…

The finite local models of the actual sheaf morphism give the kernel and cokernel models. Noetherian coefficients are needed for kernels; cokernels are finite type over any commutative ring.

Refining the two trivializing étale covers gives constant models for a binary product. Both inverse image and the constant-sheaf functor preserve binary products, and a product of finitely generated modules is finitely g…

Over a finite commutative coefficient ring, finite type locally constant étale module sheaves carry a continuous linear action of the étale fundamental group on their actual geometric stalks. The underlying set action is…

Over a finite coefficient ring, the underlying set sheaf of a finite type locally constant module sheaf is finite locally constant. The original trivializing étale cover works: inverse image commutes with forgetting the…

For a connected scheme with a geometric point, finite locally constant set sheaves are equivalent to finite sets with a continuous action of the étale fundamental group. The group is the existing EFG automorphism group o…

Finite adapted stratifications on complementary pieces give one on the whole scheme when the open image is retrocompact. Affine-local base change then proves the criterion on arbitrary schemes. The condition on the open…

Open retrocompact subsets correspond to quasi-compact open immersions. Stability of quasi-compactness under base change shows that arbitrary scheme morphisms preserve constructible subsets by inverse image. Hence the act…

Every finite locally constant sheaf of sets on the small étale site of an arbitrary scheme is represented by a finite étale scheme. Restricting to the directed affine open cover supplies affine representers by effective…

The universal section of a representer on an étale cover constructs its descent action. The unit and action laws follow from the actual naturality and uniqueness in the representing equivalence.

A cartesian local representer descends to a representer of the original sheaf when its projection is invariant under the actual descent action. The proof glues the universal section along a surjective étale morphism, the…

A finite étale representative of the restriction along an isomorphism gives a representative of the original sheaf. We use its base change along the inverse isomorphism, the map/pullback adjunction, and the natural compa…

Finite adapted stratifications transport along scheme isomorphisms. This identifies affine-local constructibility with finite stratifiability on an affine scheme and proves restriction to an arbitrary open subscheme pres…

An étale covering of the base detects isomorphisms of set-valued sheaves by bijectivity on the member sites. Pulling the cover back to each test scheme gives the local lifting and local equality conditions. This applies…

We replace an affine étale cover and its finite étale representing scheme by the spectra of their global section rings. The fully faithful spectrum functor supplies ring maps with these precise spectra. Restriction of th…

A stratification consists of finitely many actual locally closed subschemes whose constructible images partition the base. Strata need not be nonempty, which permits common refinements to retain all pairs of indices. The…

An inverse image disjoint from the image of an open or closed immersion annihilates extension by zero or closed direct image, respectively. These are statements about the actual sheaves, detected by geometric stalks.

A finite family of constructible subsets of an arbitrary topological space admits a common finite partition into locally closed constructible subsets. Each part is contained in, or disjoint from, each member of the origi…

Base change preserves finite limits and étale covering sieves. The covering statement follows from base change on the localized big étale sites, using the description of the small topology through the forgetful functors…

The two projections from a scheme's self-fiber product give section maps into the same chosen iterated inverse image. Their comparison uses the existing composition isomorphisms and the actual pullback square equation.

Initiality of pointed neighborhoods identifies restriction of maps to skyscraper sheaves. The general site result then proves that the actual counit of inverse image and direct image is an isomorphism on every stalk. Con…

The closed-immersion adjunction unit is an epimorphism. Its image sieve therefore supplies an actual lift near every point. The disjoint union of these neighborhoods is an actual surjective étale morphism, to which the f…

The finite refinement of the actual closed-unit lift cover locally factors through individual members of the original étale cover. Pulling their given sections through these factors produces actual sections of inverse im…

The concrete local preimages on a finite refinement glue on its closed fiber: the original unit, pulled back to that refinement, is injective on the relevant Zariski stalks. Proper henselian restriction then lifts this c…

At a geometric point inside the image, direct image has the original stalk. Outside the image, it has zero stalk. Geometric stalks therefore show that direct image preserves short exact sequences and finite colimits. The…

At a geometric point of the closed subscheme, the stalk of direct image is the original stalk. Initiality of the constructed neighborhood functor and the comparison of colimits supply the natural isomorphism. The result…

The geometric neighborhood lifting theorem supplies an ambient étale neighborhood and a map from its restriction to any prescribed pointed étale neighborhood of the closed subscheme. We construct the corresponding costru…

The module-valued closed adjunction unit is an isomorphism on geometric stalks inside the closed subscheme. The injective map from Zariski germs to geometric germs makes its underlying Zariski stalk map injective there.…

A section of a disjoint union of copies of a connected scheme lands in a unique component. Using the actual constant-sheaf adjunction unit and the representation by that disjoint union, the constant set-sheaf functor is…

A map from a constant presheaf of finitely generated modules locally factors through any locally bijective constant presentation of its target. A finite intersection of covering image sieves puts all generators in the im…

For a continuous functor preserving a terminal object, composition of its left adjoint with the constant-sheaf functor is left adjoint to global sections on the target site. Uniqueness of left adjoints gives the constant…

The disjoint union of copies of a scheme indexed by a set represents the constant sheaf with that set as value. The disjoint open covering gives a coproduct of represented sheaves, and the constant-sheaf adjunction ident…

The empty sieve covers an empty étale object. Its sheaf sections are terminal, and hence zero in any coefficient category with zero morphisms.

Composition with an étale morphism defines a continuous functor of small étale sites. Its adjunction with scheme base change identifies actual inverse image of set-valued sheaves with restriction of their underlying pres…

An object of the slice of X.Etale over U is an étale scheme over U.left. The structural map is étale by the existing cancellation theorem for maps between schemes étale over the same base. The inverse functor uses compos…

Composition with an open immersion gives a fully faithful, continuous inclusion of small étale sites. Its adjunction with base change identifies restriction of sheaves with the inverse image constructed in Sites.SheafFun…

For an open immersion, a geometric lift through an étale scheme over the open subscheme is already a lift over that subscheme. This gives the fiber comparison used by the general site result in Sites.StalkAdjunction. The…

Every covering sieve of the terminal object of the small étale site of a field contains a connected finite étale surjective cover. We select an actual spectrum of a finite separable field from the established geometric d…

For a finite surjection, lift an algebraically closed geometric point using the same field. Invert the actual pullback stalk map at one lift. The Čech equation on the pair of any two lifts shows that this germ works at e…

Finite intersections of image sieves lift a finite free basis along a sheaf epimorphism. The resulting maps on sections define actual sheaf morphisms on an étale cover, and the comparison with inverse image is tracked ex…

Equality of two étale sheaf sections is detected on an open subset of the underlying scheme. Closedness of a finite morphism then shrinks an ambient neighborhood around the whole fiber. This supplies the injective half o…

Pulling the original closed-fiber unit to the self-fiber product stays injective on global sections. Naturality and the actual Čech equation for the pulled-back target section therefore force compatibility of the constru…

Čech-compatible sections give germs downstairs. Injectivity of the actual finite direct-image stalk comparison puts the direct-image section in the unit's image on every stalk. The unit is a monomorphism, so these local…

Choose algebraically closed residue-field points on the target. Surjectivity and finiteness supply a lift of each of these points using the same field. The unit followed by its concrete stalk component is an isomorphism,…

A section on a finite etale Galois cover descends exactly when it is fixed by its deck transformations. The proof uses actual sheaf descent and the proved decomposition of the cover's self-product into deck graphs. No Ga…

Every covering sieve on the identity object of a strictly local spectrum is maximal: a neighborhood over its closed point has a section. Consequently an epimorphism of actual module sheaves is surjective on global sectio…

For a closed immersion and its complementary open immersion, the actual adjunction counit and unit give the short exact sequence 0 ⟶ j!j^G ⟶ G ⟶ ii^G ⟶ 0. The composite is zero and exactness is checked on all geometric s…

An open cover of a scheme étale over the base gives a covering hypercover in the small étale site. The overlap covers are supplied by the existing SchemeTheory.WeilRestriction.locallyDirectedCoverHypercover. Every scheme…

For a fixed square of right adjoints, changing the chosen left adjoints conjugates the inverse mate by the canonical comparison isomorphisms. Consequently, invertibility of the inverse mate is independent of these choice…

For a functor preserving sheafification and reflecting isomorphisms, the constant-sheaf counit is an isomorphism whenever its image sheaf is constant and the target constant-sheaf functor is fully faithful. The source co…

For an étale morphism, inverse image of modules is actual restriction of presheaves. The canonical map from the constant sheaf on the source to the restriction of the constant sheaf on the target is constructed from the…

Forgetting the module structure commutes with constant sheaves, direct image, and inverse image. The inverse-image comparison is the mate of the identity between the two direct-image composites. Its invertibility is prov…

The fully faithful inclusion of the small étale sites makes the direct image fully faithful. The adjoint triple j! ⊣ j^ ⊣ j then proves that extension by zero is fully faithful as well. Consequently the canonical unit F…

For any proper scheme over a henselian local ring, restriction to its actual closed fiber is bijective on global sections of every étale module sheaf. The section on a finite surjective refinement satisfies the actual Če…

The actual inverse-image/direct-image unit is an isomorphism on geometric stalks along a closed immersion. Equal images of two global sections therefore give equal germs at the closed fiber, and the filtered-colimit desc…

The original unit remains injective on global sections after any pullback whose source is proper over the henselian local base. Its actual Zariski stalk maps are injective along that source's closed fiber, and those germ…

At a point over the closed point of the original local base, its geometric point factors through the actual original closed fiber. The existing inverse-image stalk isomorphism and closed-unit stalk isomorphism therefore…

The pullback pasting isomorphism on the small étale sites gives the direct image composition isomorphism. The corresponding inverse image comparison follows from the constructed adjunctions and uniqueness of left adjoint…

The chosen inverse images compose through the existing adjoint-uniqueness isomorphism. Evaluating its unit equation and the actual base-change maps at identity objects proves the corresponding equation on global sections…

A commuting scheme square supplies an actual morphism into the small-site base change. Restricting the existing adjunction unit along this morphism pulls sections to the source. Naturality retains equations of local lift…

The actual adjunction units and direct-image component maps commute with composition of scheme morphisms. This identifies the two successive maps on stalks through the chosen inverse-image composition isomorphism.

The pullback adjunction for over categories identifies geometric lifts through base change. This identifies the corresponding points of the small étale site and supplies the smallness needed for their stalks. Taking mate…

The concrete direct-image stalk component agrees with the restriction of germs at the comapped point. Consequently the adjunction unit followed by this component is an isomorphism. No finiteness or closed-immersion assum…

For a continuous functor of sites, restricting a germ at the comapped point gives a germ at the original point. Composing this concrete comparison with the adjunction unit is an isomorphism. The proof uses the stalk/skys…

The base change of the identity object is canonically the identity object. Restriction through this isomorphism identifies global sections, and its geometric germs are the concrete direct-image stalk components.

An ambient pointed étale neighborhood pulls back to a pointed neighborhood at every lift of the geometric point. Passing to the defining stalk colimits constructs the canonical direct-image stalk map to the product of th…

The concrete maps on representing neighborhoods commute with the chosen pullback-pasting isomorphism. Passing to stalks retains this equation.

The existing objectwise isomorphism between the inverse image of a represented sheaf and the sheaf represented by scheme base change is natural in the represented object. Its adjoint is the identity section, which also p…

The colimit comparison for restriction agrees, under the stalk/skyscraper adjunctions, with restriction of maps into skyscraper sheaves. Initiality of the neighborhood functor therefore makes that restriction bijective o…

If a continuous functor is initial on the categories of pointed neighborhoods, restriction of sheaves preserves the corresponding stalk. The opposite neighborhood functor is final, so the result follows from the comparis…

This is the single-section version of the gluing argument in CategoryTheory.Sheaf.isLocallyBijectiveiffisIso', from Mathlib/CategoryTheory/Sites/LocallyBijective.lean by Joël Riou. Only the image sieve of the specified s…

Scheme-theoretic pullback pasting gives the comparison of direct images. The inverse image comparison follows from the constructed adjunctions and uniqueness of left adjoints. No conditions on the scheme morphisms are ne…

The stalk of the actual inverse image is the stalk at the composite geometric point. Since geometric stalks are conservative, inverse image preserves finite limits, including the fiber squares defining extension torsors.

The affine étale site supplies the small colimits for inverse image in the same universe as the values. The resulting functor is left adjoint to restriction along base change. Constant sheaves are preserved, and inverse…

For an adjunction of continuous functors of sites with fully faithful left adjoint, the induced adjunction on sheaves has invertible counit. On each object of the source site, this counit is obtained by applying the shea…

Direct image is precomposition with base change on the small étale site. Inverse image is constructed by restriction to the affine étale site, left Kan extension, and sheafification. Essential smallness of the affine sit…

Let G be a continuous functor of sites. A comparison of the fiber functors of two points induces a comparison of their skyscraper functors. If L is left adjoint to restriction along G, taking mates gives the correspondin…

At a point of a scheme, use the separable closure of its residue field to obtain a geometric point and its filtered-colimit stalk functor. The existing conservativity of this family of geometric points detects the vanish…

The big étale topology is coarser than the subcanonical fppf topology. The inclusion of the small étale site into the slice of the big site is fully faithful, preserves finite limits, and preserves covering sieves. Conse…

The cartesian square of an open subscheme and its inverse image compares the existing small-site base change with the inverse-image functor on opens. It induces the direct-image comparison on sheaves. Its adjunction mate…

The actual lift of a geometric point to each open neighborhood defines the map from the Zariski stalk to the geometric étale stalk. Equality in the latter occurs on an étale neighborhood. Descent to its open image proves…

The top open subscheme is identified with the identity object of the small étale site. The induced identification of sections commutes with restriction to every open subscheme.

Forgetting modules and restricting to opens gives an actual sheaf of sets. Direct image commutes with these operations. Taking mates compares its topological inverse image with the underlying Zariski sheaf of module-valu…

The existing open-subscheme functor lifts to the small étale site. Taking the open image of an étale morphism is left adjoint to this inclusion. The inclusion preserves covering sieves, hence is continuous, and ordinary…

An étale neighborhood covers its open image. The small-site sheaf separation axiom therefore turns equality on that neighborhood into equality on its actual open image in the original scheme.