Module

Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free

10 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible nonempty iso unit of forall invertible free

Imports8

Imported by2

abbrev

X

L44 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.X

Documentation

The affine scheme associated to the base ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev X : Scheme.{u}

abbrev

N₀

L47 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.N₀

Documentation

The global sections of the associated module presheaf, viewed as an R-module.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · statement

abbrev N₀ (L : (X R).Modules) : ModuleCat.{u} R

def

Utop

L51 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.Utop

Documentation

The whole affine scheme as an affine open.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · statement

def Utop : (X R).affineOpens

def

σ

L54 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.σ

Documentation

The canonical identification of the base ring with global functions.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · statement

def σ : R ≃+* Γ(X R, ⊤)

def

modR

L58 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.modR

Documentation

The R-module structure on global sections supplied by the associated presheaf.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · statement

def modR (L : (X R).Modules) : Module R Γ(L, ⊤)

theorem

smul_eq

L61 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.smul_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]

Lean source · full declaration

theorem smul_eq (L : (X R).Modules) (r : R) (m : Γ(L, ⊤)) :
    (letI : Module R Γ(L, ⊤) := modR R L; r • m) = (σ R r) • m := rfl

theorem

invertibleTop

L69 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.invertibleTop

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]
variable (L : (X R).Modules)
  (htriv : ∀ x : X R, ∃ (V : (X R).Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj L ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
include htriv in

Lean source · statement

theorem invertibleTop : Module.Invertible Γ(X R, ⊤) Γ(L, ⊤)

theorem

invertibleR

L80 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.invertibleR

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]
variable (L : (X R).Modules)
  (htriv : ∀ x : X R, ∃ (V : (X R).Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj L ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
include htriv in

Lean source · statement

theorem invertibleR : @Module.Invertible R Γ(L, ⊤) _ _ (modR R L)

theorem

main

L85 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free.LFRAME.main

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct
namespace LFRAME
variable (R : Type u) [CommRing R]
variable (L : (X R).Modules)
  (htriv : ∀ x : X R, ∃ (V : (X R).Opens), x ∈ V ∧
    Nonempty ((Scheme.Modules.pullback V.ι).obj L ≅ SheafOfModules.unit V.toScheme.ringCatSheaf))
include htriv in

Lean source · statement

theorem main
    (hPic : ∀ (N : Type u) [AddCommGroup N] [Module R N], Module.Invertible R N → Module.Free R N) :
    Nonempty (L ≅ SheafOfModules.unit (X R).ringCatSheaf)

theorem

nonempty_iso_unit_of_forall_invertible_free

L104 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_unit_of_forall_invertible_free

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_unit_of_forall_invertible_free
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TensorProduct

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_unit_of_forall_invertible_free
  (R : Type u) [CommRing R]
    (hPic : ∀ (N : Type u) [AddCommGroup N] [Module R N], Module.Invertible R N → Module.Free R N)
    (L : (Spec (CommRingCat.of R)).Modules) (hL : Scheme.Modules.IsInvertible L) :
    Nonempty (L ≅ 𝟙_ (Spec (CommRingCat.of R)).Modules)

Module documentation

Scheme Modules Is Invertible nonempty iso unit of forall invertible free

Declarations