Module

FiniteTypeSchemeRestriction.lean

Nyll.SchemeTheory.Modules.FiniteTypeSchemeRestriction

6 declarations indexed from sourceView source ↗

Module documentation

Finite type under actual open restriction and slice equivalence

The native site-equivalence coefficient isomorphisms transport the actual finite local generating families in both directions. These comparisons connect slice-site finite type with the geometric restriction functor.

Imports7

Nyll.SchemeTheory.Modules.FiniteTypePushforward
Nyll.SchemeTheory.Modules.QuasicoherentLocal
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Topology.Sheaves.Module
Mathlib.CategoryTheory.Sites.CoverPreserving
Mathlib.CategoryTheory.Sites.Over
Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Imported by4

theorem

overPostContinuousOfDenseEquivalence

L29 ↗

Source context 3 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory

Lean source · statement

theorem overPostContinuousOfDenseEquivalence
    {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
    (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : C ⥤ D)
    [G.IsEquivalence] [G.IsDenseSubsite J K] (W : C) :
    (Over.post (X := W) G).IsContinuous (J.over W) (K.over (G.obj W))

theorem

isFiniteType_sheafOfModulesEquivOver

L41 ↗

TopologicalSpace.Opens.isFiniteType_sheafOfModulesEquivOver

Documentation

The actual slice-to-open equivalence preserves finite local generators.

Source context 4 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory
namespace TopologicalSpace.Opens

Lean source · statement

theorem isFiniteType_sheafOfModulesEquivOver
    {X : TopCat.{u}} (V : Opens X) (R : X.Sheaf RingCat.{u})
    (M : SheafOfModules.{u} (R.over V)) (hM : M.IsFiniteType) :
    ((V.sheafOfModulesEquivOver R).functor.obj M).IsFiniteType

theorem

isFiniteType_sheafOfModulesEquivOver_inverse

L61 ↗

TopologicalSpace.Opens.isFiniteType_sheafOfModulesEquivOver_inverse

Documentation

The actual open-to-slice inverse equivalence preserves finite local generators.

Source context 4 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory
namespace TopologicalSpace.Opens

Lean source · statement

theorem isFiniteType_sheafOfModulesEquivOver_inverse
    {X : TopCat.{u}} (V : Opens X) (R : X.Sheaf RingCat.{u})
    (M : SheafOfModules.{u} (V.sheafRestrict.obj R)) (hM : M.IsFiniteType) :
    ((V.sheafOfModulesEquivOver R).inverse.obj M).IsFiniteType

theorem

isFiniteType_restrict_of_over

L85 ↗

AlgebraicGeometry.Scheme.Modules.isFiniteType_restrict_of_over

Documentation

Finite type on the actual slice site gives finite type on the open subscheme.

Source context 4 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isFiniteType_restrict_of_over
    {X : Scheme.{u}} (M : X.Modules) (U : X.Opens)
    (hM : (M.over U).IsFiniteType) : (M.restrict U.ι).IsFiniteType

theorem

isFiniteType_over_of_restrict

L99 ↗

AlgebraicGeometry.Scheme.Modules.isFiniteType_over_of_restrict

Documentation

Finite type on the open subscheme gives finite type on the actual slice site.

Source context 4 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isFiniteType_over_of_restrict
    {X : Scheme.{u}} (M : X.Modules) (U : X.Opens)
    (hM : (M.restrict U.ι).IsFiniteType) : (M.over U).IsFiniteType

theorem

isFiniteType_restrictFunctor

L112 ↗

AlgebraicGeometry.Scheme.Modules.isFiniteType_restrictFunctor

Documentation

Restriction along an actual open immersion preserves finite type.

Source context 4 commands

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

noncomputable section
universe u v₁ u₁ v₂ u₂
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem isFiniteType_restrictFunctor
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules) (hM : M.IsFiniteType) : (M.restrict f).IsFiniteType

Module documentation

Finite type under actual open restriction and slice equivalence

Declarations

overPostContinuousOfDenseEquivalence

isFiniteType_sheafOfModulesEquivOver

isFiniteType_sheafOfModulesEquivOver_inverse

isFiniteType_restrict_of_over

isFiniteType_over_of_restrict

isFiniteType_restrictFunctor