Module

Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible

3 declarations indexed from sourceView source ↗

Module documentation

Local rank one and invertibility

Identifies modules locally free of rank one with invertible scheme modules.

Imports2

Imported by15

def

freeOneIsoUnit

L46 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible.AlgebraicGeometry.Scheme.Modules.RankOne.freeOneIsoUnit

Documentation

The canonical identification of the free rank-one module sheaf with the unit module.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace RankOne

Lean source · statement

def freeOneIsoUnit (Y : Scheme.{u}) :
    (SheafOfModules.free.{u} (ULift.{u} (Fin 1)) : Y.Modules) ≅ (SheafOfModules.unit
      Y.ringCatSheaf : Y.Modules)

theorem

iff

L52 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible.AlgebraicGeometry.Scheme.Modules.RankOne.iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace RankOne

Lean source · statement

theorem iff (X : Scheme.{u}) (M : X.Modules) : IsLocallyFreeOfRank 1 M ↔ IsInvertible M

theorem

isLocallyFreeOfRank_one_iff_isInvertible

L67 ↗

AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_one_iff_isInvertible

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_isLocallyFreeOfRank_one_iff_isInvertible
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.isLocallyFreeOfRank_one_iff_isInvertible {X :
  Scheme.{u}} (M : X.Modules) :
    Scheme.Modules.IsLocallyFreeOfRank 1 M ↔ Scheme.Modules.IsInvertible M

Module documentation

Local rank one and invertibility

Declarations

freeOneIsoUnit

iff

isLocallyFreeOfRank_one_iff_isInvertible