Module

FiniteTypeTop.lean

Nyll.SchemeTheory.Modules.FiniteTypeTop

1 declaration indexed from sourceView source ↗

Module documentation

Recovering finite type from restriction to the top open

The singleton family consisting of the top open covers every open. The existing finite-type locality theorem therefore recovers global finite type from the actual top-slice module used by the open induction.

Imports4

Nyll.SchemeTheory.Modules.FiniteTypeLocality
Mathlib.Algebra.Category.Grp.FilteredColimits
Mathlib.CategoryTheory.Sites.LeftExact
Mathlib.Topology.Sheaves.SheafCondition.Sites

Imported by2

theorem

of_over_top

L29 ↗

SheafOfModules.IsFiniteType.of_over_top

Documentation

Finite type on the top slice is finite type on the original open-set site.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace
namespace SheafOfModules

Lean source · statement

theorem IsFiniteType.of_over_top {X : Type u} [TopologicalSpace X]
    {R : Sheaf (Opens.grothendieckTopology X) RingCat.{u}}
    (M : SheafOfModules.{u} R) (hM : (M.over (⊤ : Opens X)).IsFiniteType) :
    M.IsFiniteType

Module documentation

Recovering finite type from restriction to the top open

Declarations

of_over_top