Module

LocalIsomorphism.lean

Nyll.SchemeTheory.WeilRestriction.LocalIsomorphism

4 declarations indexed from sourceView source ↗

Module documentation

Detecting sheaf isomorphisms on an open cover of the base

A morphism of sheaves on schemes over S is an isomorphism if its components are bijective on every scheme over a member of an open cover of S. Pulling that cover back to each test scheme supplies the covering sieves needed for local injectivity and local surjectivity.

Imports4

Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Sites.BigZariski
Mathlib.CategoryTheory.Sites.LocallyBijective
Mathlib.CategoryTheory.Sites.Over

Imported by2

def

baseCoverPullbackObject

L37 ↗

SchemeTheory.WeilRestriction.baseCoverPullbackObject

Documentation

A member of the pullback cover, viewed as a scheme over the original base.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} S)

Lean source · statement

def baseCoverPullbackObject (T : Over S) (i : 𝒰.I₀) : Over S

def

baseCoverPullbackMap

L41 ↗

SchemeTheory.WeilRestriction.baseCoverPullbackMap

Documentation

The projection from a member of the pullback cover to the test scheme.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} S)

Lean source · statement

def baseCoverPullbackMap (T : Over S) (i : 𝒰.I₀) :
    baseCoverPullbackObject 𝒰 T i ⟶ T

lemma

baseCoverPullbackSieve_mem

L46 ↗

SchemeTheory.WeilRestriction.baseCoverPullbackSieve_mem

Documentation

The pullback cover is covering for the induced Zariski topology on Over S.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} S)

Lean source · statement

lemma baseCoverPullbackSieve_mem (T : Over S) :
    Sieve.ofArrows (baseCoverPullbackObject 𝒰 T) (baseCoverPullbackMap 𝒰 T) ∈
      (Scheme.zariskiTopology.over S) T

lemma

isIso_of_bijective_on_openCover

L55 ↗

SchemeTheory.WeilRestriction.isIso_of_bijective_on_openCover

Documentation

Bijectivity after restricting to every member of a base cover detects isomorphisms between sheaves on the relative big Zariski site.

Source context 6 commands

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

@[expose] public section
open CategoryTheory CategoryTheory.Limits Opposite AlgebraicGeometry
noncomputable section
universe u v w
namespace SchemeTheory.WeilRestriction
variable {S : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} S)

Lean source · statement

lemma isIso_of_bijective_on_openCover
    {F G : Sheaf (Scheme.zariskiTopology.over S) (Type w)} (η : F ⟶ G)
    (h : ∀ (i : 𝒰.I₀) (T : Over (𝒰.X i)),
      Function.Bijective (η.hom.app (op ((Over.map (𝒰.f i)).obj T)))) :
    IsIso η

Module documentation

Detecting sheaf isomorphisms on an open cover of the base

Declarations

baseCoverPullbackObject

baseCoverPullbackMap

baseCoverPullbackSieve_mem

isIso_of_bijective_on_openCover