Module

ClosedAdjunction.lean

Nyll.EtaleCohomology.Sites.ClosedAdjunction

4 declarations indexed from sourceView source ↗

Module documentation

Fully faithful direct image for a closed immersion

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. Consequently direct image is fully faithful. The canonical unit is an isomorphism on stalks inside the closed subscheme and an epimorphism globally.

The schemes and commutative coefficient ring are arbitrary.

Imports22

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.ClosedNeighborhoods
Nyll.EtaleCohomology.Sites.ClosedImmersionStalks
Nyll.EtaleCohomology.Sites.PullbackStalks
Nyll.EtaleCohomology.Sites.RestrictionAdjunction
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.SchemeTheory.Morphisms.ClosedImmersionLift
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Elements
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Sites.Point.Conservative

Imported by7

lemma

etalePushforwardClosed_counit_isIso

L54 ↗

EtaleCohomology.etalePushforwardClosed_counit_isIso

Documentation

The canonical counit of a closed immersion is an isomorphism.

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 Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Lean source · statement

lemma etalePushforwardClosed_counit_isIso
    (G : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)) :
    IsIso ((etalePullbackPushforwardAdjunction i R).counit.app G)

def

etalePushforwardClosedFullyFaithful

L73 ↗

EtaleCohomology.etalePushforwardClosedFullyFaithful

Documentation

Direct image along a closed immersion is fully faithful.

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 Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Lean source · statement

def etalePushforwardClosedFullyFaithful : (etalePushforward i R).FullyFaithful

lemma

etalePushforwardClosed_unit_stalk_isIso

L80 ↗

EtaleCohomology.etalePushforwardClosed_unit_stalk_isIso

Documentation

The canonical unit is an isomorphism on stalks inside the closed subscheme.

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 Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Lean source · statement

lemma etalePushforwardClosed_unit_stalk_isIso
    {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ Z)
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    IsIso ((Scheme.pointSmallEtale (s ≫ i)).sheafFiber.map
      ((etalePullbackPushforwardAdjunction i R).unit.app G))

instance

etalePushforwardClosed_unit_epi

L95 ↗

EtaleCohomology.etalePushforwardClosed_unit_epi

Documentation

The canonical unit gives the epimorphism at the end of open-closed localization.

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 Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Lean source · statement

instance etalePushforwardClosed_unit_epi
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    Epi ((etalePullbackPushforwardAdjunction i R).unit.app G)

Module documentation

Fully faithful direct image for a closed immersion

Declarations

etalePushforwardClosed_counit_isIso

etalePushforwardClosedFullyFaithful

etalePushforwardClosed_unit_stalk_isIso

etalePushforwardClosed_unit_epi