Module

FiniteTypeLocality.lean

Nyll.SchemeTheory.Modules.FiniteTypeLocality

8 declarations indexed from sourceView source ↗

Module documentation

Locality of finite type for sheaves of modules

The native finite-type condition is preserved under isomorphisms and can be checked on a covering family. The proof composes the actual covers and transports the actual finite families of generating sections through the canonical equivalence between iterated slice sites.

The iterated-slice cover composition is adapted from the native quasicoherent-data construction at Mathlib revision 065356127b1dc0016f66b7283ce0ce2c4055aa55: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

Imports2

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Mathlib.CategoryTheory.Sites.CoversTop.Over

Imported by7

def

ofIso

L39 ↗

SheafOfModules.LocalGeneratorsData.ofIso

Documentation

Transport the actual local generating sections along an isomorphism.

Source context 5 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · full declaration

def LocalGeneratorsData.ofIso {M N : SheafOfModules.{u} R}
    (q : M.LocalGeneratorsData) (e : M ≅ N) : N.LocalGeneratorsData where
  I := q.I
  X := q.X
  coversTop := q.coversTop
  generators i := (q.generators i).ofEpi ((overFunctor R (q.X i)).mapIso e).hom

lemma

isFiniteType_ofIso

L47 ↗

SheafOfModules.LocalGeneratorsData.isFiniteType_ofIso

Documentation

Isomorphism transport keeps the same finite indexing family at each object.

Source context 5 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma LocalGeneratorsData.isFiniteType_ofIso {M N : SheafOfModules.{u} R}
    (q : M.LocalGeneratorsData) (e : M ≅ N) (hq : q.IsFiniteType) :
    (q.ofIso e).IsFiniteType

lemma

isFiniteType_shrink

L55 ↗

SheafOfModules.LocalGeneratorsData.isFiniteType_shrink

Documentation

Shrinking the cover does not change any chosen finite generating family.

Source context 5 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma LocalGeneratorsData.isFiniteType_shrink {M : SheafOfModules.{u} R}
    (q : M.LocalGeneratorsData) (hq : q.IsFiniteType) : q.shrink.IsFiniteType

lemma

isFiniteType

L62 ↗

SheafOfModules.LocalGeneratorsData.isFiniteType

Documentation

A finite family of actual local generators supplies the native finite-type predicate.

Source context 5 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma LocalGeneratorsData.isFiniteType {M : SheafOfModules.{u} R}
    (q : M.LocalGeneratorsData) (hq : q.IsFiniteType) : M.IsFiniteType

lemma

of_iso

L67 ↗

SheafOfModules.IsFiniteType.of_iso

Documentation

Finite type is preserved by an isomorphism of sheaves of modules.

Source context 5 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma IsFiniteType.of_iso {M N : SheafOfModules.{u} R}
    (e : M ≅ N) (hM : M.IsFiniteType) : N.IsFiniteType

def

bind

L79 ↗

SheafOfModules.LocalGeneratorsData.bind

Documentation

Compose a cover and the actual local generating data on its slice sites.

Source context 7 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
section Covers
variable [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
  [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · full declaration

def LocalGeneratorsData.bind (M : SheafOfModules.{u} R) {I : Type w}
    (X : I → C) (hX : J.CoversTop X)
    (q : ∀ i, (M.over (X i)).LocalGeneratorsData) : M.LocalGeneratorsData where
  I := (i : I) × (q i).I
  X ij := ((q ij.1).X ij.2).left
  coversTop := hX.over (fun i => (q i).coversTop)
  generators ij := by
    let e := pushforwardPushforwardEquivalence (Over.iteratedSliceEquiv ((q ij.1).X ij.2))
      (S := (R.over _).over _) (R := R.over _) (𝟙 _) (𝟙 _)
      (by ext : 2; exact R.1.map_id _) (by ext : 2; exact R.1.map_id _)
    let t := ((q ij.1).generators ij.2).map e.inverse (Iso.refl _)
    exact t.ofEpi (e.fullyFaithfulFunctor.preimageIso
      (by exact e.counitIso.app ((M.over (X ij.1)).over ((q ij.1).X ij.2)))).hom

lemma

isFiniteType_bind

L94 ↗

SheafOfModules.LocalGeneratorsData.isFiniteType_bind

Documentation

Composition of covers retains finiteness of every generating family.

Source context 7 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
section Covers
variable [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
  [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma LocalGeneratorsData.isFiniteType_bind (M : SheafOfModules.{u} R) {I : Type w}
    (X : I → C) (hX : J.CoversTop X)
    (q : ∀ i, (M.over (X i)).LocalGeneratorsData)
    (hq : ∀ i, (q i).IsFiniteType) : (LocalGeneratorsData.bind M X hX q).IsFiniteType

lemma

of_coversTop

L103 ↗

SheafOfModules.IsFiniteType.of_coversTop

Documentation

Finite type can be checked on any covering family of slice sites.

Source context 7 commands

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

noncomputable section
universe w u v₁ u₁
open CategoryTheory Limits
namespace SheafOfModules
variable {C : Type u₁} [Category.{v₁} C] {J : GrothendieckTopology C}
  {R : Sheaf J RingCat.{u}}
  [∀ X, HasSheafify (J.over X) AddCommGrpCat.{u}]
  [∀ X, (J.over X).WEqualsLocallyBijective AddCommGrpCat.{u}]
section Covers
variable [∀ X Y, HasSheafify ((J.over X).over Y) AddCommGrpCat.{u}]
  [∀ X Y, ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat.{u}]

Lean source · statement

lemma IsFiniteType.of_coversTop (M : SheafOfModules.{u} R) {I : Type w}
    (X : I → C) (hX : J.CoversTop X)
    (hM : ∀ i, (M.over (X i)).IsFiniteType) : M.IsFiniteType

Module documentation

Locality of finite type for sheaves of modules

Declarations