Module

FiniteTypeTilde.lean

Nyll.SchemeTheory.Modules.FiniteTypeTilde

1 declaration indexed from sourceView source ↗

Module documentation

Finite type of the sheaf associated to a finite module

Choose actual finite module generators, and use the native tilde presentation with exactly this generating set. Its relation module is allowed to be infinite. Restricting the finite family of generators to the slice sites gives the native finite-type condition.

Imports4

Mathlib.AlgebraicGeometry.Modules.Tilde
Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Mathlib.RingTheory.Finiteness.Basic

Imported by2

theorem

isFiniteType_tilde_of_finite

L31 ↗

AlgebraicGeometry.isFiniteType_tilde_of_finite

Documentation

A finite module gives an actual sheaf of finite type under tilde. No finite-presentation or Noetherian hypothesis is imposed.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory
namespace AlgebraicGeometry

Lean source · statement

theorem isFiniteType_tilde_of_finite {R : CommRingCat.{u}} (M : ModuleCat.{u} R)
    [Module.Finite R M] : (tilde M).IsFiniteType

Module documentation

Finite type of the sheaf associated to a finite module

Declarations

isFiniteType_tilde_of_finite