Module

Invertible.lean

Nyll.SchemeTheory.Modules.Invertible

5 declarations indexed from sourceView source ↗

Module documentation

Invertible scheme modules and the canonical pullback of the unit module.

Imports2

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

Imported by13

structure

IsInvertible

L27 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible

Documentation

A sheaf of modules locally isomorphic to the unit module around every point.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry

Lean source · full declaration

structure Scheme.Modules.IsInvertible {X : Scheme.{u}} (M : X.Modules) : Prop where
  /-- Every point has an open neighborhood on which the module is trivial. -/
  exists_trivialization : ∀ x : X, ∃ (U : X.Opens), x ∈ U ∧
    Nonempty ((Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit U.toScheme.ringCatSheaf)

instance

opensMapFinal

L32 ↗

AlgebraicGeometry.Scheme.Hom.opensMapFinal

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

instance Scheme.Hom.opensMapFinal {X Y : Scheme.{u}} (f : X ⟶ Y) :
    (TopologicalSpace.Opens.map f.base).Final

def

pullbackUnitIso

L37 ↗

AlgebraicGeometry.Scheme.Modules.pullbackUnitIso

Documentation

The canonical identification of the pullback of the unit module with the unit module.

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

def Scheme.Modules.pullbackUnitIso {X Y : Scheme.{u}} (f : X ⟶ Y) :
    (Scheme.Modules.pullback f).obj (SheafOfModules.unit Y.ringCatSheaf) ≅
      SheafOfModules.unit X.ringCatSheaf

theorem

isInvertible_unit

L53 ↗

AlgebraicGeometry.Scheme.Modules.isInvertible_unit

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Modules.isInvertible_unit (X : Scheme.{u}) :
    Scheme.Modules.IsInvertible (SheafOfModules.unit X.ringCatSheaf)

theorem

pullback

L57 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.pullback

Source context 4 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry

Lean source · statement

theorem Scheme.Modules.IsInvertible.pullback {X Y : Scheme.{u}} (f : X ⟶ Y) {L : Y.Modules}
    (hL : Scheme.Modules.IsInvertible L) :
    Scheme.Modules.IsInvertible ((Scheme.Modules.pullback f).obj L)

Module documentation

Declarations

IsInvertible

opensMapFinal

pullbackUnitIso

isInvertible_unit

pullback