Module

Scheme_Modules_CechTrivialisation_isUnit_transition_and_transition_face_mul_eq.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_isUnit_transition_and_transition_face_mul_eq

43 declarations indexed from sourceView source ↗

Module documentation

Unit transition functions and the Čech cocycle identity

The transition functions of a module trivialisation are units and satisfy the cocycle identity.

Imports7

Imported by3

def

uapp

L122 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L128 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L133 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L140 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L147 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L152 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L159 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L163 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L169 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L175 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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

L194 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L199 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L204 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.assoc_app

Source context 13 commands

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

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

L216 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.assoc_app''

Source context 13 commands

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

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

L243 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L250 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L258 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.congr_unit

Source context 13 commands

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

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

L264 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.congr_nat

Source context 13 commands

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

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

L285 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.toU

Documentation

Regard a structure sheaf section 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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L288 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L298 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L310 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.uASm

Documentation

The structure sheaf section determined by 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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L320 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.uASm_trans

Source context 14 commands

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

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

L322 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.isUnit_uASm

Source context 14 commands

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

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

L324 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.uASm_eq

Source context 14 commands

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

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

L328 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L332 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L340 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.unitAutSection_conj

Source context 12 commands

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

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

L368 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.genRestrict

Documentation

Restrict a trivialisation along a factorisation of the scheme morphism.

Source context 13 commands

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

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

restrictIso_comp

L374 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.restrictIso_comp

Source context 13 commands

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

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

L392 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.genRestrict_comp

Source context 13 commands

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

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

L434 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L443 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L454 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.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.SchemeModulesCechTrivIsUnit
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 SchemeModulesCechTrivIsUnit.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

L458 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.κiso

Documentation

The canonical comparison between successive pullbacks along open inclusions.

Source context 13 commands

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

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

L463 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.restrict_trans

Source context 13 commands

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

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

θ

L474 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.θ

Documentation

The transition section comparing two trivialisations on a common open subscheme.

Source context 13 commands

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

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

L477 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.transition_eq_θ

Source context 13 commands

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

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

L480 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.θ_res

Source context 13 commands

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

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

L490 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.θ_mul

Source context 13 commands

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

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

L496 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.isUnit_transition

Source context 13 commands

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

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

L499 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit.PV1TL.cocycle

Source context 13 commands

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

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

isUnit_transition_and_transition_face_mul_eq

L523 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.isUnit_transition_and_transition_face_mul_eq

Source context 10 commands

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

section ProofImplementation
section PublicStatement
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsUnit
namespace AlgebraicGeometry.Scheme.Modules.CechTrivialisation

Lean source · statement

theorem isUnit_transition_and_transition_face_mul_eq
    {Y : Scheme.{u}} (𝒱 : Y.OrderedAffineCover) (𝓜 : Y.Modules)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) :
    (∀ s : 𝒱.Idx 1, IsUnit (τ.transition s)) ∧
    ∀ 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))

Module documentation

Unit transition functions and the Čech cocycle identity

Declarations