NYLL
Module

SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.lean

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

Module documentation

Small Extension exists is Pic Deformation Cocycle pullback eq unit Pullback

Imports23
Imported by2

Declarations

theorem

unitPullback_add

L63 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.unitPullback_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem unitPullback_add (hk : Xk' ⟶ Xk) (𝒲 : Xk'.OrderedAffineCover) (𝒦 : Xk.OrderedAffineCover)
  (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ hk ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (z z' : (OModulePresheaf.unit fk).cochain 𝒦 n)
      :
    OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n (z + z') =
      OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n z +
        OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n z'
theorem

unitPullback_smul

L86 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.unitPullback_smul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem unitPullback_smul (hk : Xk' ⟶ Xk) (hfk : hk ≫ fk = fk') (𝒲 : Xk'.OrderedAffineCover) (𝒦 :
  Xk.OrderedAffineCover)
    (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ hk ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (c : k)
    (z : (OModulePresheaf.unit fk).cochain 𝒦 n) :
    OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n (c • z) =
      c • OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n z
def

unitPullbackLin

L120 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.unitPullbackLin
Documentation

The linear pullback map on the unit-module Čech cochains.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · full declaration
def unitPullbackLin (hk : Xk' ⟶ Xk) (hfk : hk ≫ fk = fk') (𝒲 : Xk'.OrderedAffineCover)
    (𝒦 : Xk.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ hk ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) :
    (OModulePresheaf.unit fk).cochain 𝒦 n →ₗ[k] (OModulePresheaf.unit fk').cochain 𝒲 n where
  toFun := OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam n
  map_add' := unitPullback_add hk 𝒲 𝒦 lam hlam n
  map_smul' := unitPullback_smul hk hfk 𝒲 𝒦 lam hlam n
theorem

sort_pair_eq_swap

L127 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.sort_pair_eq_swap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem sort_pair_eq_swap {ι : Type u} [LinearOrder ι] (f : Fin 2 → ι) (h : f 1 < f 0) : Tuple.sort
  f = Equiv.swap 0 1
theorem

injective_pair

L147 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.injective_pair
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem injective_pair {ι : Type u} (f : Fin 2 → ι) (h : f 0 ≠ f 1) : Function.Injective f
theorem

monotone_pair

L155 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.monotone_pair
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem monotone_pair {ι : Type u} [Preorder ι] (f : Fin 2 → ι) (h : f 0 ≤ f 1) : Monotone f
theorem

unitPullback_one_of_lt

L163 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.unitPullback_one_of_lt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem unitPullback_one_of_lt (hk : Xk' ⟶ Xk) (𝒲 : Xk'.OrderedAffineCover) (𝒦 :
  Xk.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ hk ⁻¹ᵁ 𝒦.U (lam w)) (z : (OModulePresheaf.unit fk).cochain 𝒦 1) (s : 𝒲.Idx
      1)
    (hinj : Function.Injective (lam ∘ s.1)) (hlt : lam (s.1 0) < lam (s.1 1)) :
    OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam 1 z s =
      (hk.appLE (𝒦.inter (𝒲.sortIdx 𝒦 lam s hinj)) (𝒲.inter s) (𝒲.inter_le_preimage_inter_sortIdx
        hk 𝒦 lam hlam s hinj)).hom
        (z (𝒲.sortIdx 𝒦 lam s hinj))
theorem

unitPullback_one_of_gt

L179 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.unitPullback_one_of_gt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem unitPullback_one_of_gt (hk : Xk' ⟶ Xk) (𝒲 : Xk'.OrderedAffineCover) (𝒦 :
  Xk.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ hk ⁻¹ᵁ 𝒦.U (lam w)) (z : (OModulePresheaf.unit fk).cochain 𝒦 1) (s : 𝒲.Idx
      1)
    (hinj : Function.Injective (lam ∘ s.1)) (hgt : lam (s.1 1) < lam (s.1 0)) :
    OModulePresheaf.unitPullback (πX := fk') hk 𝒲 𝒦 lam hlam 1 z s =
      -(hk.appLE (𝒦.inter (𝒲.sortIdx 𝒦 lam s hinj)) (𝒲.inter s) (𝒲.inter_le_preimage_inter_sortIdx
        hk 𝒦 lam hlam s hinj)).hom
        (z (𝒲.sortIdx 𝒦 lam s hinj))
theorem

mul_self_eq_zero_of_isFibreReading

L193 ↗
AlgebraicCurves.Geometry.Picard.Proofs.SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback.T3D4.mul_self_eq_zero_of_isFibreReading
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
namespace T3D4
variable {k : Type u} [Field k] {Xk Xk' : Scheme.{u}}
  {fk : Xk ⟶ Spec (CommRingCat.of k)} {fk' : Xk' ⟶ Spec (CommRingCat.of k)}
Lean source · statement
theorem mul_self_eq_zero_of_isFibreReading {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
    (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ι : V →ₗ[B₁] B₁) (hJ : ∀ v w : V, ι v
      * ι w = 0)
    {X Xk : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of B₁)) (fk : Xk ⟶ Spec (CommRingCat.of k)) (i :
      Xk ⟶ X)
    (U : X.Opens) (W : Xk.Opens) (hW : W ≤ i ⁻¹ᵁ U) (δ : Γ(X, U))
    (w : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk).obj W) (hw : IsFibreReading V ι f fk i U W
      hW δ w) :
    δ * δ = 0
theorem

exists_isPicDeformationCocycle_pullback_eq_unitPullback

L211 ↗
AlgebraicGeometry.SmallExtension.exists_isPicDeformationCocycle_pullback_eq_unitPullback
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Picard.Proofs
namespace SmallExtension_exists_isPicDeformationCocycle_pullback_eq_unitPullback
attribute [-simp] AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_neg
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_zero
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_sub
  AlgebraicGeometry.Scheme.Modules.pullbackLocalSection_add
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
universe u
open T3D4 in
Lean source · statement
theorem
  _root_.AlgebraicGeometry.SmallExtension.exists_isPicDeformationCocycle_pullback_eq_unitPullback
    {B₁ : Type u} [CommRing B₁] {k : Type u} [Field k]
    (V : Type u) [AddCommGroup V] [Module k V] [Module B₁ V] (ι : V →ₗ[B₁] B₁)
    (hJ : ∀ v w : V, ι v * ι w = 0)
    {X X' X₀ X₀' Xk Xk' : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of B₁)) (f' : X' ⟶ Spec (CommRingCat.of B₁))
    (g : X₀ ⟶ X) [IsAffineHom g] (g' : X₀' ⟶ X') [IsAffineHom g']
    (fk : Xk ⟶ Spec (CommRingCat.of k)) (fk' : Xk' ⟶ Spec (CommRingCat.of k))
    (i : Xk ⟶ X) [IsAffineHom i] (i' : Xk' ⟶ X') [IsAffineHom i']
    (h : X' ⟶ X) (hh : h ≫ f = f')
    (h₀ : X₀' ⟶ X₀) (hh₀ : h₀ ≫ g = g' ≫ h)
    (hk : Xk' ⟶ Xk) (hhk : hk ≫ i = i' ≫ h) (hfk : hk ≫ fk = fk')
    (𝒰 : X.OrderedAffineCover) (𝒲 : X'.OrderedAffineCover) (lam : 𝒲.ι → 𝒰.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒰.U (lam w))
    (hlamk : ∀ w, (𝒲.comap i').U w ≤ hk ⁻¹ᵁ (𝒰.comap i).U (lam w))
    (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)
    (hw : IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w) :
    ∃ w' : Module.Dual k V →ₗ[k] (OModulePresheaf.unit fk').cochain (𝒲.comap i') 1,
      (∀ ξ : Module.Dual k V,
        w' ξ = OModulePresheaf.unitPullback (πX := fk') hk (𝒲.comap i') (𝒰.comap i) lam hlamk 1 (w
          ξ)) ∧
      IsPicDeformationCocycle V ι f' fk' i' g' 𝒲 ((Scheme.Modules.pullback h).obj M)
        (((Scheme.Modules.pullbackComp g' h).app M) ≪≫
          ((Scheme.Modules.pullbackCongr hh₀.symm).app M) ≪≫
          ((Scheme.Modules.pullbackComp h₀ g).app M).symm ≪≫
          (Scheme.Modules.pullback h₀).mapIso φ₀ ≪≫
          Scheme.Modules.pullbackUnitIso h₀)
        w'

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