Module

OpenAdjunction.lean

Nyll.EtaleCohomology.Sites.OpenAdjunction

8 declarations indexed from sourceView source ↗

Module documentation

Fully faithful adjoints for an open immersion

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 ⟶ j^*j_!F is an isomorphism, by the general adjunction API.

The canonical counit j_!j^*F ⟶ F becomes an isomorphism after restriction. The pullback stalk formula transfers this fact to each geometric stalk inside the open subscheme. Outside, its source stalk is zero, so geometric stalks show that the counit is a monomorphism. This supplies the first map of the open-closed localization sequence with its actual adjunction, rather than just a comparison between the objects at each stalk.

The schemes and commutative coefficient ring are arbitrary.

Imports16

Nyll.EtaleCohomology.Sites.ExtensionByZero
Nyll.EtaleCohomology.Sites.ExtensionByZeroStalks
Nyll.EtaleCohomology.Sites.SheafAdjunction
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.EtaleCohomology.Sites.PullbackStalks
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Adjunction.Triple
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Sites.Point.Conservative

Imported by4

def

openEtalePushforwardFullyFaithful

L55 ↗

EtaleCohomology.openEtalePushforwardFullyFaithful

Documentation

Direct image along an open 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 CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

def openEtalePushforwardFullyFaithful : (etalePushforward j R).FullyFaithful

instance

openEtalePushforward_full

L61 ↗

EtaleCohomology.openEtalePushforward_full

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

instance openEtalePushforward_full : (etalePushforward j R).Full

instance

openEtalePushforward_faithful

L64 ↗

EtaleCohomology.openEtalePushforward_faithful

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

instance openEtalePushforward_faithful : (etalePushforward j R).Faithful

def

etaleExtensionByZeroFullyFaithful

L68 ↗

EtaleCohomology.etaleExtensionByZeroFullyFaithful

Documentation

Extension by zero is fully faithful, by the adjoint triple for an open immersion.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

def etaleExtensionByZeroFullyFaithful : (etaleExtensionByZero j R).FullyFaithful

instance

etaleExtensionByZero_full

L73 ↗

EtaleCohomology.etaleExtensionByZero_full

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

instance etaleExtensionByZero_full : (etaleExtensionByZero j R).Full

instance

etaleExtensionByZero_faithful

L76 ↗

EtaleCohomology.etaleExtensionByZero_faithful

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]

Lean source · statement

instance etaleExtensionByZero_faithful : (etaleExtensionByZero j R).Faithful

lemma

etaleExtensionByZero_counit_stalk_isIso

L82 ↗

EtaleCohomology.etaleExtensionByZero_counit_stalk_isIso

Documentation

The canonical counit is an isomorphism on stalks inside the open subscheme.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)

Lean source · statement

lemma etaleExtensionByZero_counit_stalk_isIso
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    IsIso ((Scheme.pointSmallEtale (s ≫ j)).sheafFiber.map
      ((etaleExtensionByZeroAdjunction j R).counit.app F))

instance

etaleExtensionByZero_counit_mono

L92 ↗

EtaleCohomology.etaleExtensionByZero_counit_mono

Documentation

The counit gives the monomorphism at the start of open-closed localization.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (R : Type u) [CommRing R]
variable {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ U)

Lean source · statement

instance etaleExtensionByZero_counit_mono
    (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    Mono ((etaleExtensionByZeroAdjunction j R).counit.app F)

Module documentation

Fully faithful adjoints for an open immersion

Declarations