Module

Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_field.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_field

1 declaration indexed from sourceView source ↗

Module documentation

Invertible modules over the spectrum of a field

An invertible scheme module on the spectrum of a field is isomorphic to the tensor unit.

Imports2

Imported by18

theorem

nonempty_iso_tensorUnit_of_field

L34 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_tensorUnit_of_field

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_field
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_tensorUnit_of_field
    (k : Type u) [Field k] (L : (Spec (CommRingCat.of k)).Modules) (hL :
        Scheme.Modules.IsInvertible L) :
    Nonempty (L ≅ 𝟙_ (Spec (CommRingCat.of k)).Modules)

Module documentation

Invertible modules over the spectrum of a field

Declarations

nonempty_iso_tensorUnit_of_field