NYLL
Module

SmallExtension_exists_isPicDeformationCocycle_of_cechTrivialisation.lean

Nyll.AlgebraicCurves.Cohomology.Cech.SmallExtension_exists_isPicDeformationCocycle_of_cechTrivialisation
63 declarations indexed from sourceView source ↗

Module documentation

Small Extension exists is Pic Deformation Cocycle of cech Trivialisation

Imports36
Imported by2

Declarations

lemma

comp_square_right

L66 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.comp_square_right
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_square_right {C : Type*} [Category C]
    {A B D E F G : C} {f : A ⟶ B} {g : B ⟶ D} {k : A ⟶ E} {l : E ⟶ D}
    (hfg : f ≫ g = k ≫ l) (h : D ⟶ F) (i : F ⟶ G) :
    f ≫ (g ≫ h) ≫ i = k ≫ l ≫ h ≫ i
lemma

comp_unit_cancel

L73 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.comp_unit_cancel
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_unit_cancel {C : Type*} [Category C]
    {A B D E F G H : C} (e : A ≅ B) (b : B ⟶ D) (f : D ⟶ E)
    (z : F ≅ E) (c : F ⟶ G) (d : G ⟶ H) (v : E ⟶ H)
    (hu : z.hom ≫ v = c ≫ d) :
    b ≫ f ≫ v = e.inv ≫ (e.hom ≫ b ≫ f ≫ z.inv ≫ c) ≫ d
lemma

comp_discrepancy_square

L81 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.comp_discrepancy_square
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
Lean source · statement
lemma comp_discrepancy_square {C : Type*} [Category C]
    {A B D E F G H I : C} (a : A ⟶ B) (b : B ⟶ D) (c : D ⟶ E)
    (d : E ⟶ B) (u : B ⟶ A) (e : D ⟶ F) (f : F ⟶ G) (g : G ⟶ H)
    (v : H ⟶ A) (k : E ⟶ I) (l : I ⟶ A) (m : F ⟶ I) (n : I ⟶ H)
    (hu : k ≫ l = d ≫ u) (hn : c ≫ k = e ≫ m)
    (hc : f ≫ g = m ≫ n) (hv : n ≫ v = l) :
    (a ≫ (b ≫ c ≫ d)) ≫ u = (((a ≫ b) ≫ e) ≫ f) ≫ g ≫ v
def

uapp

L141 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.uapp
Documentation

The map on top sections induced by an automorphism of the unit module.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
def uapp (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf))
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : (W : Scheme.{u}).presheaf.obj (op ⊤)
theorem

unitAutSection_eq

L149 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.unitAutSection_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_eq (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e = W.topIso.hom.hom (uapp W e 1)
theorem

uapp_mul

L156 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.uapp_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_mul (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf))
    (x y : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W e (x * y) = x * uapp W e y
theorem

uapp_trans

L165 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.uapp_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_trans (W : Y.Opens)
    (e e' : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W :
      Scheme.{u}) : TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf))
    (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (e ≪≫ e') x = uapp W e' (uapp W e x)
theorem

uapp_refl

L174 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.uapp_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem uapp_refl (W : Y.Opens) (x : (W : Scheme.{u}).presheaf.obj (op ⊤)) : uapp W (Iso.refl _) x
  = x
theorem

unitAutSection_trans

L179 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.unitAutSection_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_trans (W : Y.Opens)
    (e e' : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W :
      Scheme.{u}) : TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf)) :
    unitAutSection W (e ≪≫ e') = unitAutSection W e * unitAutSection W e'
theorem

unitAutSection_refl

L188 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.unitAutSection_refl
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_refl (W : Y.Opens) :
    unitAutSection W (Iso.refl _) = 1
theorem

unitAutSection_symm_mul

L192 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.unitAutSection_symm_mul
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_symm_mul (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e.symm * unitAutSection W e = 1
theorem

unitAutSection_mul_symm

L200 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.unitAutSection_mul_symm
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_mul_symm (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf)) :
    unitAutSection W e * unitAutSection W e.symm = 1
theorem

isUnit_unitAutSection

L208 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.AlgebraicGeometry.Scheme.Modules.isUnit_unitAutSection
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace AlgebraicGeometry
namespace Scheme
namespace Modules
open _root_.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
variable {Y : Scheme.{u}}
Lean source · statement
theorem isUnit_unitAutSection (W : Y.Opens)
    (e : (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf) ≅ (SheafOfModules.unit (J :=
        _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
        Scheme.{u}).ringCatSheaf)) :
    IsUnit (unitAutSection W e)
lemma

pullbackCongr_hom_app_eq

L229 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.pullbackCongr_hom_app_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_hom_app_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    (pullbackCongr H).hom.app N = eqToHom (by rw [H]) := by
  subst H
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_hom, NatTrans.id_app, eqToHom_refl]
lemma

pullbackCongr_inv_app_eq

L234 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.pullbackCongr_inv_app_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma pullbackCongr_inv_app_eq {q q' : T ⟶ A'} (H : q = q') (N : A'.Modules) :
    (pullbackCongr H).inv.app N = eqToHom (by rw [H]) := by
  subst H
  simp only [pullbackCongr, eqToIso_refl, Iso.refl_inv, NatTrans.id_app, eqToHom_refl]
lemma

assoc_app

L239 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.assoc_app
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma assoc_app {W : Scheme.{u}} (f : T' ⟶ T) (g : T ⟶ W) (h : W ⟶ A') (N : A'.Modules) :
    (Scheme.Modules.pullback f).map ((pullbackComp g h).inv.app N) ≫
      (pullbackComp f g).hom.app ((Scheme.Modules.pullback h).obj N) ≫ (pullbackComp (f ≫ g)
        h).hom.app N =
    (pullbackComp f (g ≫ h)).hom.app N ≫ eqToHom (by rw [Category.assoc]) := by
  have := NatTrans.congr_app (pseudofunctor_associativity f g h) N
  simp only [NatTrans.comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app,
    Functor.associator_hom_app,
    eqToHom_app] at this
  erw [Category.id_comp] at this
  exact (Iso.inv_comp_eq ((pullbackComp f (g ≫ h)).app N)).1 this
lemma

assoc_app''

L251 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.assoc_app''
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma assoc_app'' {W : Scheme.{u}} (f : T' ⟶ T) (g : T ⟶ W) (h : W ⟶ A') (N : A'.Modules) :
    (Scheme.Modules.pullback f).map ((pullbackComp g h).inv.app N) =
      (pullbackComp f (g ≫ h)).hom.app N ≫ eqToHom
        (by rw [Category.assoc]) ≫ (pullbackComp (f ≫ g) h).inv.app N ≫
        (pullbackComp f g).inv.app ((Scheme.Modules.pullback h).obj N) := by
  have h1 := assoc_app f g h N
  let α : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) :=
    (Scheme.Modules.pullback f).mapIso ((pullbackComp g h).app N)
  let β : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) :=
    (pullbackComp f g).app ((Scheme.Modules.pullback h).obj N)
  let γ : (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) ≅
      (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj N := (pullbackComp (f ≫ g) h).app N
  let δ : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) ≅
      (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N := (pullbackComp f (g ≫ h)).app N
  let η : (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N ≅ (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj
    N :=
    eqToIso (by rw [Category.assoc])
  have h2 : α.symm ≪≫ β ≪≫ γ = δ ≪≫ η := Iso.ext h1
  have h3 : α.symm = δ ≪≫ η ≪≫ γ.symm ≪≫ β.symm := by
    calc α.symm = (α.symm ≪≫ β ≪≫ γ) ≪≫ (γ.symm ≪≫ β.symm) := by simp
      _ = (δ ≪≫ η) ≪≫ (γ.symm ≪≫ β.symm) := by rw [h2]
      _ = δ ≪≫ η ≪≫ γ.symm ≪≫ β.symm := by simp
  have h4 := congrArg Iso.hom h3
  simpa [α, β, γ, δ, η, eqToIso] using h4
lemma

comp_congr_right

L280 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.comp_congr_right
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma comp_congr_right (f : T' ⟶ T) {g g' : T ⟶ A'} (H : g = g') (N : A'.Modules) :
    (pullbackComp f g).inv.app N ≫ eqToHom (by rw [H]) ≫ (pullbackComp f g').hom.app N =
      eqToHom (by rw [H]) := by
  subst H
  simpa only [eqToHom_refl, Category.id_comp, Category.comp_id] using
    (pullbackComp f g).inv_hom_id_app N
lemma

comp_congr_left

L287 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.comp_congr_left
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · full declaration
lemma comp_congr_left {f f' : T' ⟶ T} (H : f = f') (g : T ⟶ A') (N : A'.Modules) :
    (pullbackComp f g).inv.app N ≫
        eqToHom (show (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj N) =
          (Scheme.Modules.pullback f').obj ((Scheme.Modules.pullback g).obj N) by rw [H]) =
      eqToHom (by rw [H]) ≫ (pullbackComp f' g).inv.app N := by
  subst H; simp
lemma

congr_unit

L294 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.congr_unit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · statement
lemma congr_unit {f f' : T' ⟶ T} (H : f = f') :
    (pullbackCongr H).hom.app ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (T : TopCat)) T.ringCatSheaf)) ≫ (pullbackUnitIso
      f').hom =
      (pullbackUnitIso f).hom
lemma

congr_nat

L303 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.congr_nat
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
section coh
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · statement
lemma congr_nat {f f' : T' ⟶ T} (H : f = f') {M N : T.Modules} (φ : M ⟶ N) :
    (pullbackCongr H).hom.app M ≫ (Scheme.Modules.pullback f').map φ =
      (Scheme.Modules.pullback f).map φ ≫ (pullbackCongr H).hom.app N
def

toU

L324 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.toU
Documentation

A structure sheaf section viewed as a section of the unit module.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
def toU (U : Z.Opens) (g : Z.presheaf.obj (op U)) :
    Γ(((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Z : TopCat))
      Z.ringCatSheaf) : Z.Modules), U)
theorem

pullbackUnitIso_hom_app_pls

L328 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.pullbackUnitIso_hom_app_pls
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
theorem pullbackUnitIso_hom_app_pls (U : Z.Opens) (g : Z.presheaf.obj (op U)) :
    (pullbackUnitIso φ).hom.app (φ ⁻¹ᵁ U) (pullbackLocalSection φ (toU U g)) =
      toU (φ ⁻¹ᵁ U) ((φ.app U).hom g)
theorem

pullbackUnitIso_inv_app_one

L338 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.pullbackUnitIso_inv_app_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section conj
variable {X Z : Scheme.{u}} (φ : X ⟶ Z)
Lean source · statement
theorem pullbackUnitIso_inv_app_one (U : Z.Opens) :
    (pullbackUnitIso φ).inv.app (φ ⁻¹ᵁ U) (toU (φ ⁻¹ᵁ U) 1) = pullbackLocalSection φ (toU U 1)
def

uASm

L351 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.uASm
Documentation

The structure sheaf section corresponding to a unit-module automorphism.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
def uASm (W : Y.Opens)
    (E : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
      ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
        TopCat)) (W : Scheme.{u}).ringCatSheaf))) : Γ(Y, W)
theorem

uASm_trans

L367 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.uASm_trans
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem uASm_trans : uASm W (E ≪≫ E') = uASm W E * uASm W E'
theorem

isUnit_uASm

L369 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.isUnit_uASm
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem isUnit_uASm : IsUnit (uASm W E)
theorem

uASm_eq

L371 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.uASm_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
    _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
    Scheme.{u}).ringCatSheaf))
    ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
      TopCat)) (W : Scheme.{u}).ringCatSheaf)))
Lean source · statement
theorem uASm_eq : uASm W E = W.topIso.hom.hom (uapp W E 1)
lemma

presheaf_map_op_apply_eq

L375 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.presheaf_map_op_apply_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
lemma presheaf_map_op_apply_eq {U V : Y.Opens} (f g : U ⟶ V) (x : Y.presheaf.obj (op V)) :
    (Y.presheaf.map f.op).hom x = (Y.presheaf.map g.op).hom x
lemma

presheaf_comp_apply_eq

L379 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.presheaf_comp_apply_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
lemma presheaf_comp_apply_eq {U V V' W : Y.Opens} (f : V ⟶ U) (g : W ⟶ V) (f' : V' ⟶ U) (g' : W ⟶
  V')
    (x : Y.presheaf.obj (op U)) :
    (Y.presheaf.map f.op ≫ Y.presheaf.map g.op).hom x = (Y.presheaf.map f'.op ≫ Y.presheaf.map
      g'.op).hom x
theorem

unitAutSection_conj

L387 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.unitAutSection_conj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
theorem unitAutSection_conj {W W' : Y.Opens} (h' : W' ≤ W)
    (E : @Iso ((W : Scheme.{u}).Modules) _ ((SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf))
      ((SheafOfModules.unit (J := _root_.Opens.grothendieckTopology ((W : Scheme.{u}) :
        TopCat)) (W : Scheme.{u}).ringCatSheaf))) :
    uASm W' ((pullbackUnitIso (Y.homOfLE h')).symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE h')).mapIso E ≪≫ pullbackUnitIso (Y.homOfLE h')) =
      (Y.presheaf.map (homOfLE h').op).hom (uASm W E)
def

genRestrict

L417 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.genRestrict
Documentation

The trivialisation pulled back along a factorisation of a chart inclusion.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
def genRestrict (ι : V ⟶ Y) (j : B ⟶ Y) (k : B ⟶ V) (e : k ≫ ι = j)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf)) :
    (Scheme.Modules.pullback j).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (B : TopCat)) B.ringCatSheaf)
theorem

genRestrict_comp

L425 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.genRestrict_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
theorem genRestrict_comp (ι : V ⟶ Y) (j : B ⟶ Y) (k : B ⟶ V) (e : k ≫ ι = j)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf))
    {B' : Scheme.{u}} (q : B' ⟶ B) (j' : B' ⟶ Y) (e' : q ≫ j = j') (k' : B' ⟶ V) (Hk : q ≫ k = k')
    (e'' : k' ≫ ι = j') :
    genRestrict 𝓜 ι j' k' e'' τ =
      ((pullbackComp q j).app 𝓜 ≪≫ (pullbackCongr e').app 𝓜).symm ≪≫
        (Scheme.Modules.pullback q).mapIso (genRestrict 𝓜 ι j k e τ) ≪≫ pullbackUnitIso q
lemma

conj_symm_trans_conj

L468 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.conj_symm_trans_conj
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section isoAlgebra
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
Lean source · statement
lemma conj_symm_trans_conj {M : C} {N U : D} {I : C} (κ : F.obj M ≅ N) (ε : F.obj I ≅ U) (Ra Rb : M
  ≅ I) :
    (κ.symm ≪≫ F.mapIso Ra ≪≫ ε).symm ≪≫ (κ.symm ≪≫ F.mapIso Rb ≪≫ ε) =
      ε.symm ≪≫ F.mapIso (Ra.symm ≪≫ Rb) ≪≫ ε
lemma

symm_trans_trans_symm_trans

L477 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.symm_trans_trans_symm_trans
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
section isoAlgebra
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
Lean source · statement
lemma symm_trans_trans_symm_trans {M I : C} (Ra Rb Rc : M ≅ I) :
    (Ra.symm ≪≫ Rb) ≪≫ (Rb.symm ≪≫ Rc) = Ra.symm ≪≫ Rc
theorem

restrict_eq_genRestrict

L487 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.restrict_eq_genRestrict
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_eq_genRestrict {a : 𝒱.ι} {W : Y.Opens} (h : W ≤ 𝒱.U a) :
    τ.restrict h = genRestrict 𝓜 (𝒱.U a).ι W.ι (Y.homOfLE h) (Y.homOfLE_ι h) (τ a)
def

κiso

L491 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.κiso
Documentation

The canonical comparison between iterated restriction and direct restriction.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def κiso (𝓜 : Y.Modules) {W W' : Y.Opens} (h' : W' ≤ W) :
    (Scheme.Modules.pullback (Y.homOfLE h')).obj ((Scheme.Modules.pullback W.ι).obj 𝓜) ≅
      (Scheme.Modules.pullback W'.ι).obj 𝓜
theorem

restrict_trans

L496 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.restrict_trans
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_trans {a : 𝒱.ι} {W W' : Y.Opens} (h : W ≤ 𝒱.U a) (h' : W' ≤ W) :
    τ.restrict (h'.trans h) =
      (κiso 𝓜 h').symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE h')).mapIso (τ.restrict h) ≪≫ pullbackUnitIso
          (Y.homOfLE h')
def

θ

L507 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.θ
Documentation

The transition section between two restricted chart trivialisations.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def θ (W : Y.Opens) (a b : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) : Γ(Y, W)
theorem

transition_eq_θ

L510 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.transition_eq_θ
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem transition_eq_θ (s : 𝒱.Idx 1) :
    τ.transition s = θ τ (𝒱.inter s) (s.1 0) (s.1 1) (𝒱.inter_le s 0) (𝒱.inter_le s 1)
theorem

θ_res

L513 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.θ_res
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem θ_res {W W' : Y.Opens} (h' : W' ≤ W) (a b : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) :
    (Y.presheaf.map (homOfLE h').op).hom (θ τ W a b ha hb) = θ τ W' a b (h'.trans ha) (h'.trans hb)
theorem

θ_mul

L522 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.θ_mul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem θ_mul (W : Y.Opens) (a b c : 𝒱.ι) (ha : W ≤ 𝒱.U a) (hb hb' : W ≤ 𝒱.U b) (hc : W ≤ 𝒱.U c) :
    θ τ W a b ha hb * θ τ W b c hb' hc = θ τ W a c ha hc
theorem

isUnit_transition

L528 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.isUnit_transition
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem isUnit_transition (s : 𝒱.Idx 1) : IsUnit (τ.transition s)
theorem

cocycle

L531 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL.cocycle
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TL
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem cocycle (r : 𝒱.Idx 2) :
    (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 2)).op).hom (τ.transition (𝒱.face r 2)) *
        (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 0)).op).hom (τ.transition (𝒱.face r 0)) =
      (Y.presheaf.map (homOfLE (𝒱.inter_le_inter_face r 1)).op).hom (τ.transition (𝒱.face r 1))
theorem

genRestrict_congr_k

L551 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TLC4.genRestrict_congr_k
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLC4
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section generic
variable {Y Y' : Scheme.{u}} (𝓜 : Y.Modules) (h : Y' ⟶ Y)
Lean source · statement
theorem genRestrict_congr_k {V B : Scheme.{u}} (ι : V ⟶ Y) (j : B ⟶ Y) {k k' : B ⟶ V} (H : k = k')
    (e : k ≫ ι = j) (e' : k' ≫ ι = j)
    (τc : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf)) :
    genRestrict 𝓜 ι j k e τc = genRestrict 𝓜 ι j k' e' τc
theorem

genRestrict_precomp

L559 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TLC4.genRestrict_precomp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLC4
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section generic
variable {Y Y' : Scheme.{u}} (𝓜 : Y.Modules) (h : Y' ⟶ Y)
Lean source · statement
theorem genRestrict_precomp {V V' B : Scheme.{u}} (ι : V ⟶ Y) (ι' : V' ⟶ Y') (k₁ : V' ⟶ V)
    (e₁ : k₁ ≫ ι = ι' ≫ h)
    (τc : (Scheme.Modules.pullback ι).obj 𝓜 ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (V : TopCat)) V.ringCatSheaf))
    (j : B ⟶ Y') (k₂ : B ⟶ V') (e₂ : k₂ ≫ ι' = j) (e₃ : (k₂ ≫ k₁) ≫ ι = j ≫ h) :
    genRestrict ((Scheme.Modules.pullback h).obj 𝓜) ι' j k₂ e₂
        ((pullbackComp ι' h).app 𝓜 ≪≫ genRestrict 𝓜 ι (ι' ≫ h) k₁ e₁ τc) =
      (pullbackComp j h).app 𝓜 ≪≫ genRestrict 𝓜 ι (j ≫ h) (k₂ ≫ k₁) e₃ τc
lemma

presheaf_map_op_apply_eq

L602 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.presheaf_map_op_apply_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma presheaf_map_op_apply_eq {Y : Scheme.{u}} {U V : Y.Opens} (f g : U ⟶ V) (x : Y.presheaf.obj
  (op V)) :
    (Y.presheaf.map f.op).hom x = (Y.presheaf.map g.op).hom x
lemma

presheaf_map_map

L607 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.presheaf_map_map
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma presheaf_map_map {Y : Scheme.{u}} {U V W : Y.Opens} (h₁ : W ≤ V) (h₂ : V ≤ U) (x :
  Y.presheaf.obj (op U)) :
    (Y.presheaf.map (homOfLE h₁).op).hom ((Y.presheaf.map (homOfLE h₂).op).hom x) =
      (Y.presheaf.map (homOfLE (h₁.trans h₂)).op).hom x
lemma

presheaf_map_map'

L614 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.presheaf_map_map'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma presheaf_map_map' {Y : Scheme.{u}} {U V W : Y.Opens} (h₁ : W ≤ V) (h₂ : V ≤ U) (h₃ : W ≤ U)
    (x : Y.presheaf.obj (op U)) :
    (Y.presheaf.map (homOfLE h₁).op).hom ((Y.presheaf.map (homOfLE h₂).op).hom x) =
      (Y.presheaf.map (homOfLE h₃).op).hom x
lemma

presheaf_map_map_self

L620 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.presheaf_map_map_self
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma presheaf_map_map_self {Y : Scheme.{u}} {U V : Y.Opens} (h₁ : U ≤ V) (h₂ : V ≤ U) (x :
  Y.presheaf.obj (op U)) :
    (Y.presheaf.map (homOfLE h₁).op).hom ((Y.presheaf.map (homOfLE h₂).op).hom x) = x
lemma

app_res

L628 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.app_res
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma app_res {X Y : Scheme.{u}} (g : X ⟶ Y) {U V : Y.Opens} (h : V ≤ U) (x : Y.presheaf.obj (op
  U)) :
    (g.app V).hom ((Y.presheaf.map (homOfLE h).op).hom x) =
      (X.presheaf.map (homOfLE (g.preimage_mono h : g ⁻¹ᵁ V ≤ g ⁻¹ᵁ U)).op).hom ((g.app U).hom x)
lemma

res_congr

L637 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.res_congr
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
lemma res_congr {X : Scheme.{u}} {I : Type*} (O : I → X.Opens) (u : ∀ s, X.presheaf.obj (op (O s)))
  {s s' : I}
    (e : s = s') {W : X.Opens} (h : W ≤ O s) (h' : W ≤ O s') :
    (X.presheaf.map (homOfLE h).op).hom (u s) = (X.presheaf.map (homOfLE h').op).hom (u s')
lemma

res_algebraMap

L643 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.res_algebraMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · full declaration
lemma res_algebraMap {R : Type u} [CommRing R] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R))
    {U U' : X.Opens} (h : U' ≤ U) (b : R) :
    letI := algebraOfHom f U
    letI := algebraOfHom f U'
    (X.presheaf.map (homOfLE h).op).hom (algebraMap R Γ(X, U) b) = algebraMap R Γ(X, U') b := by
  change ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appLE ⊤ U le_top ≫ X.presheaf.map (homOfLE
    h).op).hom b =
    ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ f.appLE ⊤ U' le_top).hom b
  exact congrArg (fun e => ((Scheme.ΓSpecIso (CommRingCat.of R)).inv ≫ e).hom b)
    (Scheme.Hom.appLE_map f (U := ⊤) (V := U) (V' := U') le_top (homOfLE h).op)
def

ΨW

L668 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.ΨW
Documentation

The restriction of a global trivialisation to an open subset.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
def ΨW (W : Y.Opens) :
    (Scheme.Modules.pullback W.ι).obj N ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology ((W : Scheme.{u}) : TopCat)) (W :
      Scheme.{u}).ringCatSheaf)
def

disc

L675 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.disc
Documentation

The discrepancy section between a chart trivialisation and a global one.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
def disc (a : 𝒱.ι) : Γ(Y, 𝒱.U a)
theorem

isUnit_disc

L677 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.isUnit_disc
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
theorem isUnit_disc (a : 𝒱.ι) : IsUnit (disc σ ψ a)
theorem

disc_res_iso

L679 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.disc_res_iso
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
theorem disc_res_iso {a : 𝒱.ι} {W : Y.Opens} (hW : W ≤ 𝒱.U a) :
    (pullbackUnitIso (Y.homOfLE hW)).symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE hW)).mapIso ((σ a).symm ≪≫ ΨW ψ (𝒱.U a)) ≪≫
          pullbackUnitIso (Y.homOfLE hW) =
      (σ.restrict hW).symm ≪≫ ΨW ψ W
theorem

disc_res

L710 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.disc_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
theorem disc_res {a : 𝒱.ι} {W : Y.Opens} (hW : W ≤ 𝒱.U a) :
    (Y.presheaf.map (homOfLE hW).op).hom (disc σ ψ a) = uASm W ((σ.restrict hW).symm ≪≫ ΨW ψ W)
theorem

transition_mul_disc_res

L716 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.transition_mul_disc_res
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
section disc
variable {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {N : Y.Modules} (σ : CechTrivialisation 𝒱 N)
  (ψ : N ≅ (SheafOfModules.unit (J := _root_.Opens.grothendieckTopology (Y : TopCat))
    Y.ringCatSheaf))
Lean source · statement
theorem transition_mul_disc_res (s : 𝒱.Idx 1) :
    σ.transition s * (Y.presheaf.map (homOfLE (𝒱.inter_le s 1)).op).hom (disc σ ψ (s.1 1)) =
      (Y.presheaf.map (homOfLE (𝒱.inter_le s 0)).op).hom (disc σ ψ (s.1 0))
lemma

tri

L725 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.tri
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
Lean source · statement
lemma tri {R : Type*} [CommRing R] (Uab Ubc Uac Ea' Eb Eb' Ec : R)
    (hcoc : Uab * Ubc = Uac) (hb : Eb * Eb' = 1)
    (h02 : (Uab * Ea' * Eb - 1) * (Ubc * Eb' * Ec - 1) = 0) :
    (Ubc * Eb' * Ec - 1) - (Uac * Ea' * Ec - 1) + (Uab * Ea' * Eb - 1) = 0
lemma

exists_lift_unit

L731 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.exists_lift_unit
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
Lean source · statement
lemma exists_lift_unit {A B : Type*} [CommRing A] [CommRing B] (φ : A →+* B) (hφ :
  Function.Surjective φ)
    (hker : ∀ x y : A, φ x = 0 → φ y = 0 → x * y = 0) (t : B) (ht : IsUnit t) :
    ∃ ab : A × A, φ ab.1 = t ∧ ab.1 * ab.2 = 1
theorem

main

L755 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1D1.main
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1D1
open _root_.AlgebraicGeometry.Scheme.Modules
open AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle.PV1TL
open _root_.IsLocalRing
open _root_.AlgebraicGeometry.SmallExtension
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem main
    {B₁ B₀ : Type u} [CommRing B₁] [IsLocalRing B₁] [CommRing B₀]
    (π : B₁ →+* B₀) (hπ : Function.Surjective π)
    (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ι : Function.Injective ι)
    (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}} (f₀ : X₀ ⟶ Spec (CommRingCat.of B₀)) (g : X₀ ⟶ X) [IsAffineHom g]
    (hg : IsPullback g f₀ f (Spec.map (CommRingCat.ofHom π)))
    {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.CechTrivialisation 𝒰 M)
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (X₀ : TopCat)) X₀.ringCatSheaf)) :
    ∃ w : Module.Dual (ResidueField B₁) V →ₗ[ResidueField B₁] (OModulePresheaf.unit fk).cochain
      (𝒰.comap i) 1,
      IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w ∧
      ∀ ξ : Module.Dual (ResidueField B₁) V, (OModulePresheaf.unit fk).d (𝒰.comap i) 1 (w ξ) = 0
theorem

exists_isPicDeformationCocycle_of_cechTrivialisation

L969 ↗
AlgebraicGeometry.SmallExtension.exists_isPicDeformationCocycle_of_cechTrivialisation
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SmallExtensionPicCocycle
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
open IsLocalRing AlgebraicGeometry.SmallExtension
  _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover in
Lean source · statement
theorem _root_.AlgebraicGeometry.SmallExtension.exists_isPicDeformationCocycle_of_cechTrivialisation
    {B₁ B₀ : Type u} [CommRing B₁] [IsLocalRing B₁] [CommRing B₀]
    (π : B₁ →+* B₀) (hπ : Function.Surjective π)
    (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ι : Function.Injective ι)
    (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}} (f₀ : X₀ ⟶ Spec (CommRingCat.of B₀)) (g : X₀ ⟶ X) [IsAffineHom g]
    (hg : IsPullback g f₀ f (Spec.map (CommRingCat.ofHom π)))
    {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.CechTrivialisation 𝒰 M)
    (φ₀ : (Scheme.Modules.pullback g).obj M ≅ (SheafOfModules.unit (J :=
      _root_.Opens.grothendieckTopology (X₀ : TopCat)) X₀.ringCatSheaf)) :
    ∃ w : Module.Dual (ResidueField B₁) V →ₗ[ResidueField B₁] (OModulePresheaf.unit fk).cochain
      (𝒰.comap i) 1,
      IsPicDeformationCocycle V ι f fk i g 𝒰 M φ₀ w ∧
      ∀ ξ : Module.Dual (ResidueField B₁) V, (OModulePresheaf.unit fk).d (𝒰.comap i) 1 (w ξ) = 0

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