Module

ModulesLocallyFreeOfRank.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesLocallyFreeOfRank

1 declaration indexed from sourceView source ↗

Module documentation

Scheme modules locally free of a fixed rank

Defines local freeness by trivializations on neighborhoods of every point.

Imports2

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Imported by59

structure

IsLocallyFreeOfRank

L31 ↗

AlgebraicGeometry.Scheme.Modules.IsLocallyFreeOfRank

Documentation

A module that is locally isomorphic to a free sheaf with n generators.

Source context 4 commands

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

universe u
open CategoryTheory
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}}

Lean source · full declaration

structure IsLocallyFreeOfRank (n : ℕ) (M : X.Modules) : Prop where
  /-- Every point has an open neighborhood on which the module is free of rank n. -/
  exists_trivialization : ∀ x : X, ∃ U : X.Opens, x ∈ U ∧
    Nonempty ((Modules.pullback U.ι).obj M ≅ SheafOfModules.free.{u} (ULift.{u} (Fin n)))

Module documentation

Scheme modules locally free of a fixed rank

Declarations

IsLocallyFreeOfRank