Module

FiniteTypeIteratedSlice.lean

Nyll.SchemeTheory.Modules.FiniteTypeIteratedSlice

4 declarations indexed from sourceView source ↗

Module documentation

Finite type and quasicoherence on iterated slice sites

The actual equivalence between an iterated slice and the slice over its underlying object transports the local finite generating families. All site, ring and module structures here use the native slice projections.

The comparison through the iterated-slice equivalence follows the native quasicoherent-data construction at Mathlib revision 065356127b1dc0016f66b7283ce0ce2c4055aa55: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

Imports4

Nyll.SchemeTheory.Modules.FiniteTypePushforward
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.CategoryTheory.Sites.CoverPreserving
Mathlib.CategoryTheory.Sites.Over

Imported by2

theorem

post_continuous_of_equivalence

L34 ↗

SheafOfModules.post_continuous_of_equivalence

Source context 4 commands

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

noncomputable section
universe u v₁ v₂ u₁ u₂
open CategoryTheory Limits
namespace SheafOfModules

Lean source · statement

theorem post_continuous_of_equivalence
    {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
    (J : GrothendieckTopology C) (K : GrothendieckTopology D) (e : C ≌ D)
    [e.functor.IsDenseSubsite J K] (W : C) :
    (Over.post (X := W) e.functor).IsContinuous (J.over W) (K.over (e.functor.obj W))

theorem

iteratedSlice_forward

L51 ↗

SheafOfModules.IsFiniteType.iteratedSlice_forward

Documentation

Direct finite type transports to the actual iterated restriction.

Source context 5 commands

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

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

Lean source · statement

theorem IsFiniteType.iteratedSlice_forward (M : SheafOfModules.{u} R)
    {X : C} (f : Over X) (hM : (M.over f.left).IsFiniteType) :
    ((M.over X).over f).IsFiniteType

theorem

iteratedSlice_backward

L71 ↗

SheafOfModules.IsFiniteType.iteratedSlice_backward

Documentation

Actual iterated finite type transports to the direct restriction.

Source context 5 commands

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

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

Lean source · statement

theorem IsFiniteType.iteratedSlice_backward (M : SheafOfModules.{u} R)
    {X : C} (f : Over X) (hM : ((M.over X).over f).IsFiniteType) :
    (M.over f.left).IsFiniteType

theorem

isQuasicoherent_iteratedSlice_forward

L102 ↗

SheafOfModules.isQuasicoherent_iteratedSlice_forward

Documentation

Direct quasicoherence transports to the actual iterated restriction.

Source context 5 commands

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

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

Lean source · statement

theorem isQuasicoherent_iteratedSlice_forward (M : SheafOfModules.{u} R)
    {X : C} (f : Over X) (hM : (M.over f.left).IsQuasicoherent) :
    ((M.over X).over f).IsQuasicoherent

Module documentation

Finite type and quasicoherence on iterated slice sites

Declarations

post_continuous_of_equivalence

iteratedSlice_forward

iteratedSlice_backward

isQuasicoherent_iteratedSlice_forward