Module

CechObstruction.lean

Nyll.AlgebraicCurves.Geometry.Picard.CechObstruction

8 declarations indexed from sourceView source ↗

Module documentation

Cech Obstruction

Imports6

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.LinearAlgebra.Dual.Defs
Mathlib.LinearAlgebra.Pi
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap
Nyll.AlgebraicCurves.Geometry.Picard.Functor

Imported by25

def

unitAutSection

L39 ↗

AlgebraicGeometry.Scheme.Modules.unitAutSection

Documentation

The section obtained by applying an automorphism of the unit sheaf on an open subscheme to its unit section and transporting it to the original open.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme.Modules
variable {Y : Scheme.{u}}

Lean source · statement

def unitAutSection (W : Y.Opens)
    (e : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    Γ(Y, W)

abbrev

CechTrivialisation

L46 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation

Documentation

A choice of a trivialisation of a sheaf of modules on each member of an ordered affine cover.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme.Modules
variable {Y : Scheme.{u}}

Lean source · statement

abbrev CechTrivialisation (𝒱 : Y.OrderedAffineCover) (𝓜 : Y.Modules) : Type u

def

restrict

L56 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.restrict

Documentation

Restrict a chosen cover trivialisation to a smaller open subscheme using the pullback composition and unit isomorphisms.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme.Modules
variable {Y : Scheme.{u}}
namespace CechTrivialisation
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

def restrict (τ : CechTrivialisation 𝒱 𝓜) {a : 𝒱.ι} {W : Y.Opens} (h : W ≤ 𝒱.U a) :
    (Scheme.Modules.pullback W.ι).obj 𝓜 ≅ SheafOfModules.unit ((W : Scheme.{u})).ringCatSheaf

def

transition

L65 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.transition

Documentation

The section representing the transition automorphism between the two restricted trivialisations on a cover overlap.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme.Modules
variable {Y : Scheme.{u}}
namespace CechTrivialisation
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

def transition (τ : CechTrivialisation 𝒱 𝓜) (s : 𝒱.Idx 1) : Γ(Y, 𝒱.inter s)

def

comap

L69 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.comap

Documentation

Pull back a cover trivialisation along an affine morphism to the inverse-image ordered cover.

Source context 8 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace Scheme.Modules
variable {Y : Scheme.{u}}
namespace CechTrivialisation
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}

Lean source · statement

def comap (τ : CechTrivialisation 𝒱 𝓜) {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h] :
    CechTrivialisation (𝒱.comap h) ((Scheme.Modules.pullback h).obj 𝓜)

def

IsFibreReading

L92 ↗

AlgebraicGeometry.SmallExtension.IsFibreReading

Documentation

Express a section using the small-extension ideal map and require its fibre readings against dual vectors to equal the corresponding restricted coefficient sums.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SmallExtension
open Scheme.TwoAffineOpenCover
variable {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
variable (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ιJ : V →ₗ[B₁] B₁)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
variable {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X)

Lean source · statement

def IsFibreReading (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ : Γ(X, U))
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W) : Prop

def

IsPicObstructionCocycle

L106 ↗

AlgebraicGeometry.SmallExtension.IsPicObstructionCocycle

Documentation

The assertion that a degree-two fibre cochain reads the failure of lifted invertible transition sections to satisfy the cocycle equation.

Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SmallExtension
open Scheme.TwoAffineOpenCover
variable {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
variable (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ιJ : V →ₗ[B₁] B₁)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
variable {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X)
variable {X₀ : Scheme.{u}} (g : X₀ ⟶ X) [IsAffineHom g] [IsAffineHom i]
variable (𝒰 : X.OrderedAffineCover)

Lean source · statement

def IsPicObstructionCocycle (𝓛₀ : X₀.Modules)
    (c : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).cochain (𝒰.comap i) 2) : Prop

def

IsPicDeformationCocycle

L125 ↗

AlgebraicGeometry.SmallExtension.IsPicDeformationCocycle

Documentation

The assertion that a degree-one fibre cochain reads the transition sections relative to chosen local units compatible with a pullback trivialisation.

Source context 12 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
namespace SmallExtension
open Scheme.TwoAffineOpenCover
variable {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
variable (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ιJ : V →ₗ[B₁] B₁)
variable {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
variable {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X)
variable {X₀ : Scheme.{u}} (g : X₀ ⟶ X) [IsAffineHom g] [IsAffineHom i]
variable (𝒰 : X.OrderedAffineCover)

Lean source · statement

def IsPicDeformationCocycle (M : X.Modules)
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ SheafOfModules.unit X₀.ringCatSheaf)
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).cochain (𝒰.comap i) 1) : Prop

Module documentation

Cech Obstruction

Declarations