Module

ConnectedConstants.lean

Nyll.EtaleCohomology.Sites.ConnectedConstants

3 declarations indexed from sourceView source ↗

Module documentation

Constant étale sheaves on connected schemes

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 fully faithful. The set can be infinite, and the scheme need not be locally noetherian or lie over a field.

Imports14

Nyll.EtaleCohomology.Sites.ConstantRepresentable
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Adjunction.FullyFaithful
Mathlib.CategoryTheory.Types.Basic
Mathlib.CategoryTheory.Limits.MorphismProperty
Mathlib.CategoryTheory.Limits.Shapes.Products
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.Logic.Function.Basic
Mathlib.Topology.Connected.TotallyDisconnected
Mathlib.Topology.Constructions

Imported by2

lemma

etaleCopiesInj_bijective

L40 ↗

EtaleCohomology.etaleCopiesInj_bijective

Documentation

Every section of the disjoint union of copies of a connected scheme is the inclusion of a unique component.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

lemma etaleCopiesInj_bijective (X : Scheme.{u}) [ConnectedSpace X] (ι : Type u) :
    Function.Bijective (etaleCopiesInj X ι)

lemma

etaleConstantSheaf_unit_isIso

L84 ↗

EtaleCohomology.etaleConstantSheaf_unit_isIso

Documentation

On a connected scheme, global sections recover the set defining a constant étale sheaf through the actual adjunction unit.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · full declaration

lemma etaleConstantSheaf_unit_isIso (X : Scheme.{u}) [ConnectedSpace X] (ι : Type u) :
    IsIso ((constantSheafAdj X.smallEtaleTopology (Type u)
      (MorphismProperty.Over.mkIdTerminal
        (show MorphismProperty Scheme.{u} from @Etale) X)).unit.app ι) := by
  let hT := MorphismProperty.Over.mkIdTerminal
    (show MorphismProperty Scheme.{u} from @Etale) X
  let η := (constantSheafAdj X.smallEtaleTopology (Type u) hT).unit.app ι
  let e := (etaleCopiesSheafIso X ι).inv.hom.app (op (etaleBaseObject X))
  have he : Function.Bijective e := (CategoryTheory.isIso_iff_bijective e).mp inferInstance
  have hc : (fun i => e (η i)) = etaleCopiesInj X ι :=
    funext (etaleCopiesSheafIso_inv_unit X ι)
  apply (CategoryTheory.isIso_iff_bijective η).mpr
  apply (Function.Bijective.of_comp_iff' he (fun i => η i)).mp
  change Function.Bijective (fun i => e (η i))
  rw [hc]
  exact etaleCopiesInj_bijective X ι

def

etaleConstantSheafFullyFaithful

L102 ↗

EtaleCohomology.etaleConstantSheafFullyFaithful

Documentation

The constant set-sheaf functor on a connected scheme is fully faithful.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

def etaleConstantSheafFullyFaithful (X : Scheme.{u}) [ConnectedSpace X] :
    (constantSheaf X.smallEtaleTopology (Type u)).FullyFaithful

Module documentation

Constant étale sheaves on connected schemes

Declarations

etaleCopiesInj_bijective

etaleConstantSheaf_unit_isIso

etaleConstantSheafFullyFaithful