NYLL
Module

SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.lean

Nyll.AlgebraicCurves.Geometry.Picard.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
10 declarations indexed from sourceView source ↗

Module documentation

Small Extension nonempty iso unit of is Pic Deformation Cocycle of forall mem range

Imports26
Imported by2

Declarations

def

sing

L73 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.sing
Documentation

The degree-zero ordered Čech index consisting of a single chart.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
Lean source · statement
def sing {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (a : 𝒰.ι) : 𝒰.Idx 0
theorem

inter_sing

L77 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.inter_sing
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
Lean source · statement
theorem inter_sing {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (a : 𝒰.ι) : 𝒰.inter (sing 𝒰 a) = 𝒰.U
  a
theorem

inter_idx0

L81 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.inter_idx0
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
Lean source · statement
theorem inter_idx0 {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (s₀ : 𝒰.Idx 0) : 𝒰.inter s₀ = 𝒰.U
  (s₀.1 0)
theorem

face_one_zero

L87 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.face_one_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
Lean source · statement
theorem face_one_zero {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (s : 𝒰.Idx 1) :
    𝒰.face s 0 = sing 𝒰 (s.1 1)
theorem

face_one_one

L93 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.face_one_one
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
Lean source · statement
theorem face_one_one {X : Scheme.{u}} (𝒰 : X.OrderedAffineCover) (s : 𝒰.Idx 1) :
    𝒰.face s 1 = sing 𝒰 (s.1 0)
theorem

rc_add

L105 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.rc_add
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
section RC
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
theorem rc_add (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ₁ δ₂ : Γ(X, U))
    (w₁ w₂ : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
    (h₁ : IsFibreReading V ιJ f fk i U W hW δ₁ w₁) (h₂ : IsFibreReading V ιJ f fk i U W hW δ₂ w₂) :
    IsFibreReading V ιJ f fk i U W hW (δ₁ + δ₂) (w₁ + w₂)
theorem

rc_neg

L117 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.rc_neg
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
section RC
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
theorem rc_neg (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ : Γ(X, U))
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
    (h : IsFibreReading V ιJ f fk i U W hW δ w) :
    IsFibreReading V ιJ f fk i U W hW (-δ) (-w)
theorem

rc_mul_eq_zero

L134 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.rc_mul_eq_zero
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
section RC
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
theorem rc_mul_eq_zero (hJ : ∀ v v' : V, ιJ v * ιJ v' = 0)
    (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ₁ δ₂ : Γ(X, U))
    (w₁ w₂ : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
    (h₁ : IsFibreReading V ιJ f fk i U W hW δ₁ w₁) (h₂ : IsFibreReading V ιJ f fk i U W hW δ₂ w₂) :
    δ₁ * δ₂ = 0
theorem

rc_res

L148 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range.D2Asm.rc_res
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
attribute [-instance] PresheafOfModules.ExteriorPower.instModulePresheafAb
attribute [-simp] AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
  PresheafOfModules.exteriorPower_map_ιMulti PresheafOfModules.ExteriorPower.appₗ_apply
  AlgebraicGeometry.Scheme.Modules.exteriorPower_obj
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
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 D2Asm
open Opposite
section RC
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
theorem rc_res (U U' : X.Opens) (hU : U' ≤ U) (W W' : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (hWW : W' ≤ W)
    (hW' : W' ≤ i ⁻¹ᵁ U') (δ : Γ(X, U))
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W)
    (h : IsFibreReading V ιJ f fk i U W hW δ w) :
    IsFibreReading V ιJ f fk i U' W' hW' ((X.presheaf.map (homOfLE hU).op).hom δ)
      (((OModulePresheaf.unit fk).res hWW).comp w)
theorem

nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range

L210 ↗
AlgebraicGeometry.SmallExtension.nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicGeometry.SmallExtension
universe u
open _root_.AlgebraicCurves.Geometry.Picard.Proofs in
open SmallExtension_nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range in
open _root_.CategoryTheory in
open _root_.CategoryTheory.Limits in
open _root_.AlgebraicGeometry in
open _root_.IsLocalRing in
open _root_.AlgebraicGeometry.SmallExtension in
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover in
open D2Asm in
Lean source · statement
theorem nonempty_iso_unit_of_isPicDeformationCocycle_of_forall_mem_range
    {B₁ B₀ : Type u} [CommRing B₁] [IsLocalRing B₁] [CommRing B₀]
    (π : B₁ →+* B₀)
    (hsmall : RingHom.ker π * maximalIdeal B₁ = ⊥) (hI : RingHom.ker π ≤ maximalIdeal B₁)
    (V : Type u) [AddCommGroup V] [Module (ResidueField B₁) V] [Module.Finite (ResidueField B₁) V]
    [Module B₁ V] [IsScalarTower B₁ (ResidueField B₁) V]
    (ι : V →ₗ[B₁] B₁)
    (hιI : LinearMap.range ι = Submodule.restrictScalars B₁ (RingHom.ker π))
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁)) [IsSeparated f] [Flat f]
    {X₀ : Scheme.{u}} (g : X₀ ⟶ X) [IsAffineHom g]
    {Xk : Scheme.{u}} (fk : Xk ⟶ Spec (CommRingCat.of (ResidueField B₁))) (i : Xk ⟶ X) [IsAffineHom
      i]
    (hi : IsPullback i fk f (Spec.map (CommRingCat.ofHom (residue B₁))))
    (𝒰 : X.OrderedAffineCover)
    (M : X.Modules) (φ₀ : (Scheme.Modules.pullback g).obj M ≅ SheafOfModules.unit X₀.ringCatSheaf)
    (w : Module.Dual (ResidueField B₁) V →ₗ[ResidueField B₁] (OModulePresheaf.unit fk).cochain
      (𝒰.comap i) 1)
    (hw : IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w)
    (hcob : ∀ ξ : Module.Dual (ResidueField B₁) V,
      w ξ ∈ LinearMap.range ((OModulePresheaf.unit fk).d (𝒰.comap i) 0)) :
    Nonempty (M ≅ SheafOfModules.unit X.ringCatSheaf)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.