Module

Scheme_Modules_exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible

4 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists ordered Affine Cover nonempty cech Trivialisation comap of is

Invertible

Imports11

Mathlib.Topology.Sheaves.SheafCondition.Sites
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.Topology.Compactness.Compact
Mathlib.Data.Fintype.EquivFin
Mathlib.Order.Basic
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap
Nyll.AlgebraicCurves.Cohomology.Sheaves.OrderedAffineCoverCochainPullback
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Picard.CechObstruction

Imported by2

def

restrictTriv

L49 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation.TrivCoverPen.restrictTriv

Documentation

Restrict a trivialisation from an open subscheme to a smaller open.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace TrivCoverPen
open TopologicalSpace Opposite

Lean source · statement

def restrictTriv {Y : Scheme.{u}} {M : Y.Modules} {V W : Y.Opens} (h : W ≤ V)
    (τ : (Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit ((V :
      Scheme.{u})).ringCatSheaf) :
    (Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit ((W : Scheme.{u})).ringCatSheaf

theorem

isZero_of_isEmpty

L58 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation.TrivCoverPen.isZero_of_isEmpty

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace TrivCoverPen
open TopologicalSpace Opposite

Lean source · statement

theorem isZero_of_isEmpty {Y : Scheme.{u}} [IsEmpty Y] (M : SheafOfModules.{u} Y.ringCatSheaf) :
    Limits.IsZero M

theorem

nonempty_iso_of_isEmpty

L71 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation.TrivCoverPen.nonempty_iso_of_isEmpty

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace TrivCoverPen
open TopologicalSpace Opposite

Lean source · statement

theorem nonempty_iso_of_isEmpty {Y : Scheme.{u}} [IsEmpty Y] (M N : Y.Modules) : Nonempty (M ≅
  N)

theorem

exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible

L94 ↗

AlgebraicGeometry.Scheme.Modules.exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible

Source context 11 commands

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

section ProofImplementation
section PublicStatement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.InvertibleAffineTrivialisation
namespace AlgebraicGeometry.Scheme.Modules

Lean source · statement

theorem exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible
    {X X₀ : Scheme.{u}} [CompactSpace X] (g : X₀ ⟶ X) [IsClosedImmersion g]
    (𝓛₀ : X₀.Modules) (h𝓛₀ : Scheme.Modules.IsInvertible 𝓛₀) :
    ∃ 𝒰 : X.OrderedAffineCover, Nonempty (Scheme.Modules.CechTrivialisation (𝒰.comap g) 𝓛₀)

Module documentation

Scheme Modules exists ordered Affine Cover nonempty cech Trivialisation comap of is

Declarations

restrictTriv

isZero_of_isEmpty

nonempty_iso_of_isEmpty

exists_orderedAffineCover_nonempty_cechTrivialisation_comap_of_isInvertible