Module

SmallExtension_isPicDeformationCocycle_of_iso.lean

Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_of_iso

6 declarations indexed from sourceView source ↗

Module documentation

Small Extension is Pic Deformation Cocycle of iso

Imports11

Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.Category.Basic
Mathlib.CategoryTheory.Functor.Basic
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.NatTrans
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Picard.CechObstruction

Imported by2

def

transport

L42 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso.PicDefIso.transport

Documentation

The Čech trivialization transported along an isomorphism of modules.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace PicDefIso
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 𝓜' : Y.Modules}

Lean source · statement

def transport (e : 𝓜' ≅ 𝓜) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) :
    Scheme.Modules.CechTrivialisation 𝒱 𝓜'

theorem

transport_restrict

L46 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso.PicDefIso.transport_restrict

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace PicDefIso
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 𝓜' : Y.Modules}

Lean source · statement

theorem transport_restrict (e : 𝓜' ≅ 𝓜) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜)
    {a : 𝒱.ι} {W : Y.Opens} (h : W ≤ 𝒱.U a) :
    (transport e τ).restrict h = (Scheme.Modules.pullback W.ι).mapIso e ≪≫ τ.restrict h

theorem

transport_transition

L77 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso.PicDefIso.transport_transition

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace PicDefIso
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 𝓜' : Y.Modules}

Lean source · statement

theorem transport_transition (e : 𝓜' ≅ 𝓜) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) (s : 𝒱.Idx 1)
  :
    (transport e τ).transition s = τ.transition s

theorem

transport_comap_hom

L97 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso.PicDefIso.transport_comap_hom

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace PicDefIso
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 𝓜' : Y.Modules}

Lean source · statement

theorem transport_comap_hom (e : 𝓜' ≅ 𝓜) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜)
    {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h] (a : 𝒱.ι) :
    ((transport e τ).comap h a).hom =
      (Scheme.Modules.pullback h ⋙ Scheme.Modules.pullback (h ⁻¹ᵁ 𝒱.U a).ι).map e.hom ≫ (τ.comap h
        a).hom

theorem

transport_comap

L137 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso.PicDefIso.transport_comap

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
namespace PicDefIso
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 𝓜' : Y.Modules}

Lean source · statement

theorem transport_comap (e : 𝓜' ≅ 𝓜) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜)
    {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h] (a : 𝒱.ι) :
    (transport e τ).comap h a =
      (Scheme.Modules.pullback ((𝒱.comap h).U a).ι).mapIso ((Scheme.Modules.pullback h).mapIso e)
        ≪≫ τ.comap h a

theorem

isPicDeformationCocycle_of_iso

L147 ↗

AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_of_iso

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_iso
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe u
open PicDefIso in

Lean source · statement

theorem _root_.AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_of_iso
    {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
    (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ι : V →ₗ[B₁] B₁)
    {X X₀ Xk : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁))
    (fk : Xk ⟶ Spec (CommRingCat.of k)) (i : Xk ⟶ X) [IsAffineHom i]
    (g : X₀ ⟶ X) [IsAffineHom g]
    (𝒰 : X.OrderedAffineCover)
    {M M' : X.Modules} (e : M ≅ M')
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ SheafOfModules.unit X₀.ringCatSheaf)
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).cochain (𝒰.comap i) 1)
    (hw : SmallExtension.IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w) :
    SmallExtension.IsPicDeformationCocycle V ι f fk i g 𝒰 M'
      ((Scheme.Modules.pullback g).mapIso e.symm ≪≫ φ₀) w

Module documentation

Small Extension is Pic Deformation Cocycle of iso

Declarations

transport

transport_restrict

transport_transition

transport_comap_hom

transport_comap

isPicDeformationCocycle_of_iso