Module

SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection.lean

Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection

5 declarations indexed from sourceView source ↗

Module documentation

Small Extension is Pic Deformation Cocycle of app Top eq unit Aut Section

Imports7

Imported by2

theorem

uAS_trans

L36 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection.PicDefRescale.uAS_trans

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace PicDefRescale

Lean source · statement

theorem uAS_trans {Y : Scheme.{u}} (W : Y.Opens)
    (e₁ e₂ : SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    Scheme.Modules.unitAutSection W (e₁ ≪≫ e₂) =
      Scheme.Modules.unitAutSection W e₁ * Scheme.Modules.unitAutSection W e₂

theorem

unit_app_one_res

L43 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection.PicDefRescale.unit_app_one_res

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace PicDefRescale

Lean source · statement

theorem unit_app_one_res {Y : Scheme.{u}} (ψ : SheafOfModules.unit Y.ringCatSheaf ≅
  SheafOfModules.unit Y.ringCatSheaf)
    {U V : Y.Opens} (i : V ⟶ U) :
    (Y.presheaf.map i.op).hom ((ψ.hom.val.app (op U)).hom (1 : Y.presheaf.obj (op U))) =
      (ψ.hom.val.app (op V)).hom (1 : Y.presheaf.obj (op V))

theorem

uAS_conj_res

L52 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection.PicDefRescale.uAS_conj_res

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace PicDefRescale

Lean source · statement

theorem uAS_conj_res {Y : Scheme.{u}} (W : Y.Opens)
    (ψ : SheafOfModules.unit Y.ringCatSheaf ≅ SheafOfModules.unit Y.ringCatSheaf) :
    Scheme.Modules.unitAutSection W
        ((Scheme.Modules.pullbackUnitIso W.ι).symm ≪≫ (Scheme.Modules.pullback W.ι).mapIso ψ ≪≫
          Scheme.Modules.pullbackUnitIso W.ι) =
      (Y.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
        (Scheme.Modules.unitAutSection ⊤
          ((Scheme.Modules.pullbackUnitIso (⊤ : Y.Opens).ι).symm ≪≫
            (Scheme.Modules.pullback (⊤ : Y.Opens).ι).mapIso ψ ≪≫
            Scheme.Modules.pullbackUnitIso (⊤ : Y.Opens).ι))

theorem

res_res

L67 ↗

AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection.PicDefRescale.res_res

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace PicDefRescale
variable {X : Scheme.{u}}

Lean source · statement

theorem res_res {U V : X.Opens} (h : V ≤ U) (x : Γ(X, ⊤)) :
    (X.presheaf.map (homOfLE h).op).hom ((X.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op).hom x) =
      (X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op).hom x

theorem

isPicDeformationCocycle_of_appTop_eq_unitAutSection

L78 ↗

AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_of_appTop_eq_unitAutSection

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_isPicDeformationCocycle_of_appTop_eq_unitAutSection
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open PicDefRescale in

Lean source · statement

theorem _root_.AlgebraicGeometry.SmallExtension.isPicDeformationCocycle_of_appTop_eq_unitAutSection
    {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 : X.Modules)
    (φ₀ φ₀' : (Scheme.Modules.pullback g).obj M ≅ SheafOfModules.unit X₀.ringCatSheaf)
    (u u' : Γ(X, ⊤)) (huu' : u * u' = 1)
    (hu : g.appTop.hom u =
      Scheme.Modules.unitAutSection ⊤
        ((Scheme.Modules.pullbackUnitIso (⊤ : X₀.Opens).ι).symm ≪≫
          (Scheme.Modules.pullback (⊤ : X₀.Opens).ι).mapIso (φ₀.symm ≪≫ φ₀') ≪≫
          Scheme.Modules.pullbackUnitIso (⊤ : X₀.Opens).ι))
    (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 φ₀' w

Module documentation

Small Extension is Pic Deformation Cocycle of app Top eq unit Aut Section

Declarations

uAS_trans

unit_app_one_res

uAS_conj_res

res_res

isPicDeformationCocycle_of_appTop_eq_unitAutSection