Module

QuasicoherentLocal.lean

Nyll.SchemeTheory.Modules.QuasicoherentLocal

5 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence from actual affine restrictions

The affine tilde presentation is transported to the open subscheme and then through the native equivalence with the slice site. These genuine local presentations form quasicoherent data on the canonical affine open cover.

Imports8

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Mathlib.Topology.Sheaves.Module
Mathlib.CategoryTheory.Adjunction.Limits

Imported by13

def

sheafOfModulesEquivalence

L34 ↗

AlgebraicGeometry.Scheme.Modules.sheafOfModulesEquivalence

Documentation

The identity action on modules and morphisms, with the scheme-module and native sheaf-module category structures made explicit.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · full declaration

def sheafOfModulesEquivalence (X : Scheme.{u}) :
    X.Modules ≌ SheafOfModules.{u} X.ringCatSheaf where
  functor :=
    { obj := fun M => M
      map := fun φ => φ
      map_id := fun _ => rfl
      map_comp := fun _ _ => rfl }
  inverse :=
    { obj := fun M => M
      map := fun φ => φ
      map_id := fun _ => rfl
      map_comp := fun _ _ => rfl }
  unitIso := NatIso.ofComponents (fun M => Iso.refl M) (by intros; rfl)
  counitIso := NatIso.ofComponents (fun M => Iso.refl M) (by intros; rfl)
  functor_unitIso_comp := fun _ => by rfl

def

presentationOfQuasicoherentSpec

L50 ↗

AlgebraicGeometry.Scheme.Modules.presentationOfQuasicoherentSpec

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

def presentationOfQuasicoherentSpec
    {R : CommRingCat.{u}} (M : (Spec R).Modules) [M.IsQuasicoherent] :
    M.Presentation

def

presentationOverOfRestrict

L69 ↗

AlgebraicGeometry.Scheme.Modules.presentationOverOfRestrict

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

def presentationOverOfRestrict
    {X : Scheme.{u}} (M : X.Modules) (U : X.Opens)
    (P : (M.restrict U.ι).Presentation) : (M.over U).Presentation

def

presentationOfAffineSpecRestriction

L85 ↗

AlgebraicGeometry.Scheme.Modules.presentationOfAffineSpecRestriction

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

def presentationOfAffineSpecRestriction
    {X : Scheme.{u}} (M : X.Modules) (U : X.Opens) (hU : IsAffineOpen U)
    (P : (M.restrict hU.fromSpec).Presentation) : (M.over U).Presentation

theorem

isQuasicoherent_of_affineSpecRestrictions

L105 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_of_affineSpecRestrictions

Documentation

Quasicoherence can be checked on the actual restrictions to the canonical spectra of the rings of affine-open sections.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isQuasicoherent_of_affineSpecRestrictions
    {X : Scheme.{u}} (M : X.Modules)
    (h : ∀ (U : X.Opens) (hU : IsAffineOpen U),
      (M.restrict hU.fromSpec).IsQuasicoherent) : M.IsQuasicoherent

Module documentation

Quasicoherence from actual affine restrictions

Declarations

sheafOfModulesEquivalence

presentationOfQuasicoherentSpec

presentationOverOfRestrict

presentationOfAffineSpecRestriction

isQuasicoherent_of_affineSpecRestrictions