Module

ImmersionOperations.lean

Nyll.EtaleCohomology.Constructible.ImmersionOperations

3 declarations indexed from sourceView source ↗

Module documentation

Constructibility of extension by zero and closed direct image

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 their open-closed factorization. All coefficient rings are allowed and no noetherian hypothesis on the base scheme is imposed.

Imports8

Nyll.EtaleCohomology.Constructible.Basic
Nyll.EtaleCohomology.Constructible.OpenClosed
Nyll.EtaleCohomology.Constructible.Support
Nyll.EtaleCohomology.Sites.OpenAdjunction
Nyll.EtaleCohomology.Sites.ClosedAdjunction
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.Topology.Constructible

Imported by1

Nyll.EtaleCohomology.Constructible.All

theorem

extensionByZero

L33 ↗

EtaleCohomology.IsEtaleConstructible.extensionByZero

Documentation

Extension by zero along a quasi-compact open immersion preserves constructibility.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleConstructible.extensionByZero
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    {G : Sheaf U.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsEtaleConstructible R G) :
    IsEtaleConstructible R ((etaleExtensionByZero j R).obj G)

theorem

closedPushforward

L54 ↗

EtaleCohomology.IsEtaleConstructible.closedPushforward

Documentation

Closed direct image preserves constructibility if the complementary open image is retrocompact. This condition is automatic for noetherian bases.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleConstructible.closedPushforward
    (i : Z ⟶ X) [IsClosedImmersion i] (hi : IsRetrocompact (Set.range i)ᶜ)
    {G : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsEtaleConstructible R G) :
    IsEtaleConstructible R ((etalePushforward i R).obj G)

theorem

locallyClosedExtension

L74 ↗

EtaleCohomology.IsEtaleConstructible.locallyClosedExtension

Documentation

Extension along an open-closed factorization of a locally closed immersion preserves constructibility under the corresponding image conditions.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X U Z : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleConstructible.locallyClosedExtension
    (i : Z ⟶ U) [IsClosedImmersion i] (hi : IsRetrocompact (Set.range i)ᶜ)
    (j : U ⟶ X) [IsOpenImmersion j] [QuasiCompact j]
    {G : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsEtaleConstructible R G) :
    IsEtaleConstructible R
      ((etaleExtensionByZero j R).obj ((etalePushforward i R).obj G))

Module documentation

Constructibility of extension by zero and closed direct image

Declarations

extensionByZero

closedPushforward

locallyClosedExtension