NYLL
Module

Scheme_Modules_CechTrivialisation_exists_refinement_transition_eq.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_exists_refinement_transition_eq
65 declarations indexed from sourceView source ↗

Module documentation

Refine a Cech trivialisation along a morphism and compare its transition functions with the pullbacks of the original transitions, including coincident and reversed chart indices.

Imports9
Imported by2

Declarations

def

uapp

L143 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules.uapp
Documentation

Evaluate an automorphism of the unit module on a section over an open subscheme.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (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.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e = W.topIso.hom.hom (uapp W e 1)
theorem

uapp_mul

L154 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (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

L161 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (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

L168 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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

L173 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W (e ≪≫ e') = unitAutSection W e * unitAutSection W e'
theorem

unitAutSection_refl

L180 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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

L184 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e.symm * unitAutSection W e = 1
theorem

unitAutSection_mul_symm

L190 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    unitAutSection W e * unitAutSection W e.symm = 1
theorem

isUnit_unitAutSection

L196 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf) :
    IsUnit (unitAutSection W e)
lemma

pullbackCongr_hom_app_eq

L215 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L220 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

pullbackCongr_symm_app_eq

L225 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.pullbackCongr_symm_app_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
variable {T' T A' : Scheme.{u}}
Lean source · statement
lemma pullbackCongr_symm_app_eq {q q' : T ⟶ A'} (H : q = q')
    (N : A'.Modules) :
    ((pullbackCongr H).app N).symm = (pullbackCongr H.symm).app N
lemma

assoc_app

L231 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.assoc_app
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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''

L243 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.assoc_app''
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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
  let A : T'.Modules :=
    (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N)
  let B : T'.Modules :=
    (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj ((Scheme.Modules.pullback
      h).obj N))
  let C : T'.Modules :=
    (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N)
  let D : T'.Modules := (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj N
  let E : T'.Modules := (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N
  let a : A ⟶ B := (Scheme.Modules.pullback f).map ((pullbackComp g h).inv.app N)
  let b : B ≅ C := (pullbackComp f g).app ((Scheme.Modules.pullback h).obj N)
  let c : C ≅ D := (pullbackComp (f ≫ g) h).app N
  let d : A ⟶ E := (pullbackComp f (g ≫ h)).hom.app N
  let e : E ⟶ D := eqToHom (by dsimp only [E, D]; rw [Category.assoc])
  have h1 : a ≫ b.hom ≫ c.hom = d ≫ e := assoc_app f g h N
  have h2 : (a ≫ b.hom) ≫ c.hom = d ≫ e :=
    (Category.assoc a b.hom c.hom).trans h1
  have h3 : a ≫ b.hom = (d ≫ e) ≫ c.inv := (Iso.eq_comp_inv c).2 h2
  have h4 : a = ((d ≫ e) ≫ c.inv) ≫ b.inv := (Iso.eq_comp_inv b).2 h3
  exact h4.trans ((Category.assoc (d ≫ e) c.inv b.inv).trans
    (Category.assoc d e (c.inv ≫ b.inv)))
lemma

comp_congr_right

L270 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L277 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 only [eqToHom_refl, Category.comp_id, Category.id_comp]
lemma

congr_unit

L285 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.congr_unit
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 T.ringCatSheaf) ≫ (pullbackUnitIso f').hom =
      (pullbackUnitIso f).hom
lemma

congr_nat

L291 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.congr_nat
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L312 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.toU
Documentation

View a section of the structure sheaf 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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 Z.ringCatSheaf : Z.Modules), U)
theorem

pullbackUnitIso_hom_app_pls

L315 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L325 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L337 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.uASm
Documentation

The section of the structure sheaf associated to an automorphism of the unit module.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
Lean source · statement
def uASm (W : Y.Opens)
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) : Γ(Y, W)
theorem

uASm_trans

L347 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.uASm_trans
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
    (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf))
Lean source · statement
theorem uASm_trans : uASm W (E ≪≫ E') = uASm W E * uASm W E'
theorem

isUnit_uASm

L349 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.isUnit_uASm
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
    (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf))
Lean source · statement
theorem isUnit_uASm : IsUnit (uASm W E)
theorem

uASm_eq

L351 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.uASm_eq
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
section uasMod
variable (W : Y.Opens)
  (E E' : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
    (SheafOfModules.unit (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

L355 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L359 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L367 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.unitAutSection_conj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (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

L395 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.genRestrict
Documentation

Restrict a trivialisation along a morphism compatible with the structural maps.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 V.ringCatSheaf : V.Modules)) :
    (Scheme.Modules.pullback j).obj 𝓜 ≅ (SheafOfModules.unit B.ringCatSheaf : B.Modules)
theorem

pullbackComp_genRestrict_eq

L402 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.pullbackComp_genRestrict_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
theorem pullbackComp_genRestrict_eq {A : Scheme.{u}}
    (i : B ⟶ A) (h : A ⟶ Y) (ι : V ⟶ Y) (k : B ⟶ V) (e : k ≫ ι = i ≫ h)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅
      (SheafOfModules.unit V.ringCatSheaf : V.Modules)) :
    @Eq ((Scheme.Modules.pullback i).obj ((Scheme.Modules.pullback h).obj 𝓜) ≅
      (SheafOfModules.unit B.ringCatSheaf : B.Modules))
      ((pullbackComp i h).app 𝓜 ≪≫ genRestrict 𝓜 ι (i ≫ h) k e τ)
      ((pullbackComp i h).app 𝓜 ≪≫ (pullbackCongr e.symm).app 𝓜 ≪≫
        ((pullbackComp k ι).app 𝓜).symm ≪≫
          (Scheme.Modules.pullback k).mapIso τ ≪≫ pullbackUnitIso k)
theorem

restrictIso_comp

L419 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.restrictIso_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
section G
variable {Y V B : Scheme.{u}} (𝓜 : Y.Modules)
Lean source · statement
theorem restrictIso_comp
    {C₀ C₁ C₂ : Type*} [Category C₀] [Category C₁] [Category C₂]
    (F : C₀ ⥤ C₁) (G : C₁ ⥤ C₂) (H : C₀ ⥤ C₂) (α : F ⋙ G ≅ H)
    {M I : C₀} {B₀ B₁ J : C₁} {A₀ A₁ U : C₂}
    (a₀ : A₀ ≅ A₁) (a₁ : A₁ ≅ H.obj M) (c : A₀ ≅ G.obj B₀)
    (b₀ : B₀ ≅ B₁) (b₁ : B₁ ≅ F.obj M) (τ : M ≅ I)
    (ε : F.obj I ≅ J) (δ : G.obj J ≅ U) (η : H.obj I ≅ U)
    (hc : c.hom ≫ G.map b₀.hom ≫ G.map b₁.hom =
      a₀.hom ≫ a₁.hom ≫ α.inv.app M)
    (hu : α.hom.app I ≫ η.hom = G.map ε.hom ≫ δ.hom) :
    a₀ ≪≫ a₁ ≪≫ H.mapIso τ ≪≫ η =
      c ≪≫ G.mapIso (b₀ ≪≫ b₁ ≪≫ F.mapIso τ ≪≫ ε) ≪≫ δ
theorem

genRestrict_comp

L437 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.genRestrict_comp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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 V.ringCatSheaf : V.Modules))
    {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

L479 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L488 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L499 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L503 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.κiso
Documentation

Identify iterated restriction to an open subscheme with direct pullback.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L508 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.restrict_trans
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

θ

L519 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.θ
Documentation

The transition section between two trivialisations restricted to a common open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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_θ

L522 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.transition_eq_θ
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L525 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.θ_res
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L535 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.θ_mul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L541 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.isUnit_transition
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L544 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL.cocycle
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.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

L564 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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 V.ringCatSheaf : V.Modules)) :
    genRestrict 𝓜 ι j k e τc = genRestrict 𝓜 ι j k' e' τc
theorem

restrictIso_precomp

L570 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4.restrictIso_precomp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
section generic
variable {Y Y' : Scheme.{u}} (𝓜 : Y.Modules) (h : Y' ⟶ Y)
Lean source · statement
theorem restrictIso_precomp
    {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
    {M N I : C} {A₀ A₁ B U : D}
    (a₀ : A₀ ≅ A₁) (a₁ : A₁ ≅ F.obj M) (c : A₀ ≅ B) (b : B ≅ F.obj N)
    (t : M ≅ N) (τ : N ≅ I) (ε : F.obj I ≅ U)
    (hc : a₀.hom ≫ a₁.hom ≫ F.map t.hom = c.hom ≫ b.hom) :
    a₀ ≪≫ a₁ ≪≫ F.mapIso (t ≪≫ τ) ≪≫ ε =
      c ≪≫ b ≪≫ F.mapIso τ ≪≫ ε
theorem

genRestrict_precomp

L582 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4.genRestrict_precomp
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
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 SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.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 V.ringCatSheaf : V.Modules))
    (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

trans_symm_trans_trans

L638 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.trans_symm_trans_trans
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
section isoAlgebra
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
Lean source · statement
lemma trans_symm_trans_trans {A B U U' : C} (c : A ≅ B) (G₀ : B ≅ U) (G₁ : B ≅ U') :
    (c ≪≫ G₀).symm ≪≫ (c ≪≫ G₁) = G₀.symm ≪≫ G₁
lemma

conj_trans_conj_eq_refl

L643 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.conj_trans_conj_eq_refl
Source context 15 commands

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

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

uASm_eq_one_of_eq_refl

L653 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.uASm_eq_one_of_eq_refl
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
Lean source · statement
theorem uASm_eq_one_of_eq_refl (W : X.Opens)
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) (hE : E = Iso.refl _) :
    uASm W E = 1
theorem

uASm_symm_self

L659 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.uASm_symm_self
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
Lean source · statement
theorem uASm_symm_self (W : X.Opens) {A : (W : Scheme.{u}).Modules}
    (G : A ≅ SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf) : uASm W (G.symm ≪≫ G) = 1
lemma

topIso_hom_inv_apply

L663 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.topIso_hom_inv_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
Lean source · statement
lemma topIso_hom_inv_apply (U : X.Opens) (x : Γ(X, U)) : U.topIso.hom.hom (U.topIso.inv.hom x) = x
theorem

uASm_resLE

L668 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.uASm_resLE
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
Lean source · statement
theorem uASm_resLE (h : X ⟶ Y) {W : Y.Opens} {W' : X.Opens} (hle : W' ≤ h ⁻¹ᵁ W)
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) :
    (X.presheaf.map (homOfLE hle).op).hom ((h.app W).hom (uASm W E)) =
      uASm W' ((pullbackUnitIso (h.resLE W W' hle)).symm ≪≫
        (Scheme.Modules.pullback (h.resLE W W' hle)).mapIso E ≪≫ pullbackUnitIso (h.resLE W W'
          hle))
theorem

sortIdx_fin_two

L699 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.sortIdx_fin_two
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
Lean source · statement
theorem sortIdx_fin_two (_h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam :
  𝒲.ι → 𝒱.ι)
    (s : 𝒲.Idx 1) (hinj : Function.Injective (lam ∘ s.1)) :
    (lam (s.1 0) < lam (s.1 1) →
      (𝒲.sortIdx 𝒱 lam s hinj).1 0 = lam (s.1 0) ∧ (𝒲.sortIdx 𝒱 lam s hinj).1 1 = lam (s.1 1)) ∧
    (lam (s.1 1) < lam (s.1 0) →
      (𝒲.sortIdx 𝒱 lam s hinj).1 0 = lam (s.1 1) ∧ (𝒲.sortIdx 𝒱 lam s hinj).1 1 = lam (s.1 0))
def

jw

L729 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.jw
Documentation

The morphism from a refined chart to its assigned chart in the original cover.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def jw (w : 𝒲.ι) : (𝒲.U w : Scheme.{u}) ⟶ (𝒱.U (lam w) : Scheme.{u})
theorem

jw_ι

L732 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.jw_ι
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem jw_ι (w : 𝒲.ι) : jw h 𝒱 𝒲 lam hlam w ≫ (𝒱.U (lam w)).ι = (𝒲.U w).ι ≫ h
def

tauP

L736 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.tauP
Documentation

The trivialisation obtained by pulling each chart trivialisation to the refined cover.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def tauP : CechTrivialisation 𝒲 ((Scheme.Modules.pullback h).obj 𝓜)
theorem

genRestrict_chart_congr

L741 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.genRestrict_chart_congr
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem genRestrict_chart_congr {B : Scheme.{u}} {a b : 𝒱.ι} (hab : a = b) (j : B ⟶ Y)
    (k : B ⟶ (𝒱.U a : Scheme.{u})) (k' : B ⟶ (𝒱.U b : Scheme.{u}))
    (e : k ≫ (𝒱.U a).ι = j) (e' : k' ≫ (𝒱.U b).ι = j) :
    genRestrict 𝓜 (𝒱.U a).ι j k e (τ a) = genRestrict 𝓜 (𝒱.U b).ι j k' e' (τ b)
theorem

tauP_restrict

L749 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.tauP_restrict
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · full declaration
theorem tauP_restrict (w : 𝒲.ι) {W' : X.Opens} (hle : W' ≤ 𝒲.U w) :
    (tauP h 𝒱 𝒲 lam hlam 𝓜 τ).restrict hle =
      (pullbackComp W'.ι h).app 𝓜 ≪≫
        genRestrict 𝓜 (𝒱.U (lam w)).ι (W'.ι ≫ h) (X.homOfLE hle ≫ jw h 𝒱 𝒲 lam hlam w)
          (by rw [Category.assoc, jw_ι, ← Category.assoc, Scheme.homOfLE_ι]) (τ (lam w)) := by
  rw [restrict_eq_genRestrict]
  exact genRestrict_precomp 𝓜 h (𝒱.U (lam w)).ι (𝒲.U w).ι (jw h 𝒱 𝒲 lam hlam w) (jw_ι h 𝒱 𝒲 lam
    hlam w)
    (τ (lam w)) W'.ι (X.homOfLE hle) (X.homOfLE_ι hle) _
theorem

tauP_transition

L759 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.tauP_transition
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · full declaration
theorem tauP_transition (s : 𝒲.Idx 1) :
    (tauP h 𝒱 𝒲 lam hlam 𝓜 τ).transition s =
      uASm (𝒲.inter s)
        ((genRestrict 𝓜 (𝒱.U (lam (s.1 0))).ι ((𝒲.inter s).ι ≫ h)
            (X.homOfLE (𝒲.inter_le s 0) ≫ jw h 𝒱 𝒲 lam hlam (s.1 0))
            (by rw [Category.assoc, jw_ι, ← Category.assoc, Scheme.homOfLE_ι]) (τ (lam (s.1
              0)))).symm ≪≫
          genRestrict 𝓜 (𝒱.U (lam (s.1 1))).ι ((𝒲.inter s).ι ≫ h)
            (X.homOfLE (𝒲.inter_le s 1) ≫ jw h 𝒱 𝒲 lam hlam (s.1 1))
            (by rw [Category.assoc, jw_ι, ← Category.assoc, Scheme.homOfLE_ι]) (τ (lam (s.1 1))))
              := by
  rw [transition_eq_θ, θ, tauP_restrict, tauP_restrict]
  refine congrArg (uASm (𝒲.inter s)) ?_
  apply Iso.ext
  dsimp only [Iso.trans, Iso.symm, Iso.app]
  erw [Category.assoc, Iso.inv_hom_id_app_assoc]
  try rfl
theorem

clause_T0

L777 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.clause_T0
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem clause_T0 (s : 𝒲.Idx 1) (hs : lam (s.1 0) = lam (s.1 1)) :
    (tauP h 𝒱 𝒲 lam hlam 𝓜 τ).transition s = 1
theorem

symm_trans_eq_conj

L785 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.symm_trans_eq_conj
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · full declaration
theorem symm_trans_eq_conj (s : 𝒲.Idx 1) (t : 𝒱.Idx 1) (hWt : 𝒲.inter s ≤ h ⁻¹ᵁ 𝒱.inter t)
    (i₀ i₁ : Fin 2) (h₀ : t.1 i₀ = lam (s.1 0)) (h₁ : t.1 i₁ = lam (s.1 1)) :
    (genRestrict 𝓜 (𝒱.U (lam (s.1 0))).ι ((𝒲.inter s).ι ≫ h)
            (X.homOfLE (𝒲.inter_le s 0) ≫ jw h 𝒱 𝒲 lam hlam (s.1 0))
            (by rw [Category.assoc, jw_ι, ← Category.assoc, Scheme.homOfLE_ι]) (τ (lam (s.1
              0)))).symm ≪≫
          genRestrict 𝓜 (𝒱.U (lam (s.1 1))).ι ((𝒲.inter s).ι ≫ h)
            (X.homOfLE (𝒲.inter_le s 1) ≫ jw h 𝒱 𝒲 lam hlam (s.1 1))
            (by rw [Category.assoc, jw_ι, ← Category.assoc, Scheme.homOfLE_ι]) (τ (lam (s.1 1))) =
      (pullbackUnitIso (h.resLE (𝒱.inter t) (𝒲.inter s) hWt)).symm ≪≫
        (Scheme.Modules.pullback (h.resLE (𝒱.inter t) (𝒲.inter s) hWt)).mapIso
          ((τ.restrict (𝒱.inter_le t i₀)).symm ≪≫ τ.restrict (𝒱.inter_le t i₁)) ≪≫
        pullbackUnitIso (h.resLE (𝒱.inter t) (𝒲.inter s) hWt) := by
  have hm : h.resLE (𝒱.inter t) (𝒲.inter s) hWt ≫ (𝒱.inter t).ι = (𝒲.inter s).ι ≫ h :=
    Scheme.Hom.resLE_comp_ι _ _
  have ek : ∀ i, (h.resLE (𝒱.inter t) (𝒲.inter s) hWt ≫ Y.homOfLE (𝒱.inter_le t i)) ≫ (𝒱.U (t.1
    i)).ι =
      (𝒲.inter s).ι ≫ h := fun i => by
    rw [Category.assoc, Scheme.homOfLE_ι, hm]
  rw [← genRestrict_chart_congr 𝒱 𝓜 τ h₀ ((𝒲.inter s).ι ≫ h)
      (h.resLE (𝒱.inter t) (𝒲.inter s) hWt ≫ Y.homOfLE (𝒱.inter_le t i₀)) _ (ek i₀),
    ← genRestrict_chart_congr 𝒱 𝓜 τ h₁ ((𝒲.inter s).ι ≫ h)
      (h.resLE (𝒱.inter t) (𝒲.inter s) hWt ≫ Y.homOfLE (𝒱.inter_le t i₁)) _ (ek i₁)]
  rw [genRestrict_comp 𝓜 (𝒱.U (t.1 i₀)).ι (𝒱.inter t).ι (Y.homOfLE (𝒱.inter_le t i₀)) (Y.homOfLE_ι
    _)
      (τ (t.1 i₀)) (h.resLE (𝒱.inter t) (𝒲.inter s) hWt) ((𝒲.inter s).ι ≫ h) hm _ rfl (ek i₀),
    genRestrict_comp 𝓜 (𝒱.U (t.1 i₁)).ι (𝒱.inter t).ι (Y.homOfLE (𝒱.inter_le t i₁)) (Y.homOfLE_ι _)
      (τ (t.1 i₁)) (h.resLE (𝒱.inter t) (𝒲.inter s) hWt) ((𝒲.inter s).ι ≫ h) hm _ rfl (ek i₁),
    ← restrict_eq_genRestrict, ← restrict_eq_genRestrict]
  exact conj_symm_trans_conj
    (Scheme.Modules.pullback (h.resLE (𝒱.inter t) (𝒲.inter s) hWt))
    ((pullbackComp (h.resLE (𝒱.inter t) (𝒲.inter s) hWt) (𝒱.inter t).ι).app 𝓜 ≪≫
      (pullbackCongr hm).app 𝓜)
    (pullbackUnitIso (h.resLE (𝒱.inter t) (𝒲.inter s) hWt))
    (τ.restrict (𝒱.inter_le t i₀)) (τ.restrict (𝒱.inter_le t i₁))
theorem

clause_Tplus

L821 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.clause_Tplus
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem clause_Tplus (s : 𝒲.Idx 1) (hinj : Function.Injective (lam ∘ s.1)) (hlt : lam (s.1 0) <
  lam (s.1 1)) :
    (tauP h 𝒱 𝒲 lam hlam 𝓜 τ).transition s =
      (X.presheaf.map (homOfLE (𝒲.inter_le_preimage_inter_sortIdx h 𝒱 lam hlam s hinj)).op).hom
        ((h.app (𝒱.inter (𝒲.sortIdx 𝒱 lam s hinj))).hom (τ.transition (𝒲.sortIdx 𝒱 lam s hinj)))
theorem

clause_Tminus

L832 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLT1.clause_Tminus
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
namespace PV1TLT1
open _root_.AlgebraicGeometry.Scheme.Modules
open SchemeModulesCechTrivExists.AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TL
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists.PV1TLC4
variable {X Y : Scheme.{u}}
section main
variable (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam : 𝒲.ι → 𝒱.ι)
  (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w)) (𝓜 : Y.Modules) (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem clause_Tminus (s : 𝒲.Idx 1) (hinj : Function.Injective (lam ∘ s.1)) (hlt : lam (s.1 1) <
  lam (s.1 0)) :
    (tauP h 𝒱 𝒲 lam hlam 𝓜 τ).transition s *
      (X.presheaf.map (homOfLE (𝒲.inter_le_preimage_inter_sortIdx h 𝒱 lam hlam s hinj)).op).hom
        ((h.app (𝒱.inter (𝒲.sortIdx 𝒱 lam s hinj))).hom (τ.transition (𝒲.sortIdx 𝒱 lam s hinj))) =
          1
theorem

exists_refinement_transition_eq

L850 ↗
AlgebraicGeometry.Scheme.Modules.CechTrivialisation.exists_refinement_transition_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExists
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
open PV1TL PV1TLT1 in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.CechTrivialisation.exists_refinement_transition_eq
    {X Y : Scheme.{u}} (h : X ⟶ Y) (𝒱 : Y.OrderedAffineCover) (𝒲 : X.OrderedAffineCover) (lam :
      𝒲.ι → 𝒱.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒱.U (lam w))
    (𝓜 : Y.Modules) (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) :
    ∃ τ' : Scheme.Modules.CechTrivialisation 𝒲 ((Scheme.Modules.pullback h).obj 𝓜),
      (∀ w : 𝒲.ι, τ' w =
        ((Scheme.Modules.pullbackComp (𝒲.U w).ι h).app 𝓜) ≪≫
          ((Scheme.Modules.pullbackCongr
              (show (𝒲.U w).ι ≫ h = (X.homOfLE (hlam w) ≫ (h ∣_ 𝒱.U (lam w))) ≫ (𝒱.U (lam w)).ι by
                rw [Category.assoc, morphismRestrict_ι, ← Category.assoc, Scheme.homOfLE_ι])).app
                  𝓜) ≪≫
          ((Scheme.Modules.pullbackComp (X.homOfLE (hlam w) ≫ (h ∣_ 𝒱.U (lam w))) (𝒱.U (lam
            w)).ι).app 𝓜).symm ≪≫
          (Scheme.Modules.pullback (X.homOfLE (hlam w) ≫ (h ∣_ 𝒱.U (lam w)))).mapIso (τ (lam w)) ≪≫
          Scheme.Modules.pullbackUnitIso (X.homOfLE (hlam w) ≫ (h ∣_ 𝒱.U (lam w)))) ∧
      (∀ s : 𝒲.Idx 1, lam (s.1 0) = lam (s.1 1) → τ'.transition s = 1) ∧
      (∀ (s : 𝒲.Idx 1) (hinj : Function.Injective (lam ∘ s.1)), lam (s.1 0) < lam (s.1 1) →
        τ'.transition s =
          (X.presheaf.map (homOfLE (𝒲.inter_le_preimage_inter_sortIdx h 𝒱 lam hlam s hinj)).op).hom
            ((h.app (𝒱.inter (𝒲.sortIdx 𝒱 lam s hinj))).hom (τ.transition (𝒲.sortIdx 𝒱 lam s
              hinj)))) ∧
      (∀ (s : 𝒲.Idx 1) (hinj : Function.Injective (lam ∘ s.1)), lam (s.1 1) < lam (s.1 0) →
        τ'.transition s *
          (X.presheaf.map (homOfLE (𝒲.inter_le_preimage_inter_sortIdx h 𝒱 lam hlam s hinj)).op).hom
            ((h.app (𝒱.inter (𝒲.sortIdx 𝒱 lam s hinj))).hom (τ.transition (𝒲.sortIdx 𝒱 lam s
              hinj))) = 1) := by
  refine ⟨tauP h 𝒱 𝒲 lam hlam 𝓜 τ, fun w => ?_, clause_T0 h 𝒱 𝒲 lam hlam 𝓜 τ,
    clause_Tplus h 𝒱 𝒲 lam hlam 𝓜 τ, clause_Tminus h 𝒱 𝒲 lam hlam 𝓜 τ⟩
  exact pullbackComp_genRestrict_eq 𝓜 (𝒲.U w).ι h (𝒱.U (lam w)).ι
    (jw h 𝒱 𝒲 lam hlam w) (jw_ι h 𝒱 𝒲 lam hlam w) (τ (lam w))

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