Module

Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_isLocalRing.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_isLocalRing

2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Is Invertible nonempty iso tensor Unit of is Local Ring

Imports7

Imported by8

theorem

nonempty_iso_unit_of_isFrameOn_top

L43 ↗

AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_IsInvertible_nonempty_iso_tensorUnit_of_isLocalRing.R2P.nonempty_iso_unit_of_isFrameOn_top

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_tensorUnit_of_isLocalRing
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.Opposite
open _root_.TopologicalSpace
open _root_.AlgebraicGeometry
open AlgebraicGeometry.Scheme.Modules
namespace R2P

Lean source · statement

theorem nonempty_iso_unit_of_isFrameOn_top {X : Scheme.{u}} {N : X.Modules} (s : Γ(N, ⊤))
    (hs : IsFrameOn s ⊤) : Nonempty (N ≅ 𝟙_ X.Modules)

theorem

nonempty_iso_tensorUnit_of_isLocalRing

L63 ↗

AlgebraicGeometry.Scheme.Modules.IsInvertible.nonempty_iso_tensorUnit_of_isLocalRing

Source context 10 commands