Module

Scheme_Modules_CechTrivialisation_comap_transition.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_comap_transition

37 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Cech Trivialisation comap transition

Imports7

Imported by2

def

uapp

L74 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules.uapp

Documentation

Evaluate a unit-module automorphism on a section over the whole restricted scheme.

Source context 15 commands

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

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

L80 ↗

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

L85 ↗

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

L92 ↗

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

L99 ↗

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

L104 ↗

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

L111 ↗

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

L115 ↗

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

L121 ↗

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

L127 ↗

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

L146 ↗

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

L151 ↗

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

L156 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.assoc_app

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.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,
    Category.id_comp, eqToHom_app] at this
  exact (Iso.inv_comp_eq ((pullbackComp f (g ≫ h)).app N)).1 this

lemma

assoc_app''

L167 ↗

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

Source context 13 commands

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

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

assoc_app'

L194 ↗

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.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) :
    (pullbackComp f g).inv.app ((Scheme.Modules.pullback h).obj N) ≫
      (Scheme.Modules.pullback f).map ((pullbackComp g h).hom.app N) =
    (pullbackComp (f ≫ g) h).hom.app N ≫ eqToHom
      (by rw [Category.assoc]) ≫ (pullbackComp f (g ≫ h)).inv.app N := by
  have h1 := assoc_app f g h N
  let α : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) :=
    (Scheme.Modules.pullback f).mapIso ((pullbackComp g h).app N)
  let β : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj
    ((Scheme.Modules.pullback h).obj N)) ≅
      (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) :=
    (pullbackComp f g).app ((Scheme.Modules.pullback h).obj N)
  let γ : (Scheme.Modules.pullback (f ≫ g)).obj ((Scheme.Modules.pullback h).obj N) ≅
      (Scheme.Modules.pullback ((f ≫ g) ≫ h)).obj N := (pullbackComp (f ≫ g) h).app N
  let δ : (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback (g ≫ h)).obj N) ≅
      (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N := (pullbackComp f (g ≫ h)).app N
  let η : (Scheme.Modules.pullback (f ≫ g ≫ h)).obj N ≅ (Scheme.Modules.pullback ((f ≫ g) ≫
    h)).obj N :=
    eqToIso (by rw [Category.assoc])
  have h2 : α.symm ≪≫ β ≪≫ γ = δ ≪≫ η := Iso.ext h1
  change β.inv ≫ α.hom = γ.hom ≫ η.inv ≫ δ.inv
  have h3 := congrArg (fun E => γ.hom ≫ E.inv) h2
  simpa only [Iso.trans_inv, Iso.symm_inv, Category.assoc, Iso.hom_inv_id_assoc] using h3

lemma

comp_congr_right

L220 ↗

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

L227 ↗

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

L235 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.congr_unit

Source context 13 commands

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

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

L241 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.congr_nat

Source context 13 commands

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

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

genRestrict

L262 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.genRestrict

Documentation

Restrict a local module trivialisation along a factorisation of its open immersion.

Source context 13 commands

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

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

theorem

genRestrict_comp

L268 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.genRestrict_comp

Source context 13 commands

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

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

pre_symm_trans_pre

L315 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.pre_symm_trans_pre

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
section isoAlgebra2
variable {C D : Type*} [Category C] [Category D] (F : C ⥤ D)

Lean source · statement

lemma pre_symm_trans_pre {M : C} {N U : D} {I : C} (P : N ≅ F.obj M) (ε : F.obj I ≅ U) (Ra Rb :
  M ≅ I) :
    (P ≪≫ F.mapIso Ra ≪≫ ε).symm ≪≫ (P ≪≫ F.mapIso Rb ≪≫ ε) =
      ε.symm ≪≫ F.mapIso (Ra.symm ≪≫ Rb) ≪≫ ε

theorem

genRestrict_pullback

L329 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.genRestrict_pullback

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
section GG
variable {Y Y' V B B' : Scheme.{u}} (𝓜 : Y.Modules)

Lean source · statement

theorem genRestrict_pullback (h : Y' ⟶ Y) (ι : V ⟶ Y) (j₁ : B ⟶ Y') (k : B ⟶ V) (e : k ≫ ι = j₁ ≫ h)
    (τ : (Scheme.Modules.pullback ι).obj 𝓜 ≅ SheafOfModules.unit V.ringCatSheaf)
    (k₂ : B' ⟶ B) (j₂ : B' ⟶ Y') (e₂ : k₂ ≫ j₁ = j₂) (e₃ : (k₂ ≫ k) ≫ ι = j₂ ≫ h) :
    genRestrict ((Scheme.Modules.pullback h).obj 𝓜) j₁ j₂ k₂ e₂
        ((pullbackComp j₁ h).app 𝓜 ≪≫ genRestrict 𝓜 ι (j₁ ≫ h) k e τ) =
      (pullbackComp j₂ h).app 𝓜 ≪≫ genRestrict 𝓜 ι (j₂ ≫ h) (k₂ ≫ k) e₃ τ

def

toU

L379 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.toU

Documentation

View a regular function 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.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
section conjGeneral
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

L382 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.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.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
section conjGeneral
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

L391 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.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.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
section conjGeneral
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

L409 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.uASm

Documentation

The function determined by a unit-module automorphism on an open subscheme.

Source context 12 commands

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

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

L414 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.uASm_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}

Lean source · statement

theorem uASm_eq (W : Y.Opens)
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) :
    uASm W E = W.topIso.hom.hom (uapp W E 1)

theorem

uASm_conj_general

L419 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.uASm_conj_general

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}

Lean source · statement

theorem uASm_conj_general {Y' : Scheme.{u}} {W : Y.Opens} {W'' : Y'.Opens}
    (q : (W'' : Scheme.{u}) ⟶ (W : Scheme.{u}))
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) :
    uASm W'' ((pullbackUnitIso q).symm ≪≫ (Scheme.Modules.pullback q).mapIso E ≪≫
      pullbackUnitIso q) =
      W''.topIso.hom.hom (q.appTop.hom (uapp W E 1))

theorem

uASm_conj_resLE

L451 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.uASm_conj_resLE

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}

Lean source · statement

theorem uASm_conj_resLE {Y' : Scheme.{u}} (h : Y' ⟶ Y) {W : Y.Opens} {W'' : Y'.Opens} (c : W'' ≤
  h ⁻¹ᵁ W)
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)) :
    uASm W'' ((pullbackUnitIso (h.resLE W W'' c)).symm ≪≫
        (Scheme.Modules.pullback (h.resLE W W'' c)).mapIso E ≪≫ pullbackUnitIso (h.resLE W W'' c)) =
      (Y'.presheaf.map (homOfLE c).op).hom ((h.app W).hom (uASm W E))

theorem

restrict_eq_genRestrict

L464 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.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.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)

Lean source · statement

theorem restrict_eq_genRestrict {a : 𝒱.ι} {W : Y.Opens} (hx : W ≤ 𝒱.U a) :
    τ.restrict hx = genRestrict 𝓜 (𝒱.U a).ι W.ι (Y.homOfLE hx) (Y.homOfLE_ι hx) (τ a)

theorem

comap_apply_eq

L469 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.comap_apply_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h]

Lean source · statement

theorem comap_apply_eq (a : 𝒱.ι) :
    τ.comap h a = (pullbackComp (h ⁻¹ᵁ 𝒱.U a).ι h).app 𝓜 ≪≫
      genRestrict 𝓜 (𝒱.U a).ι ((h ⁻¹ᵁ 𝒱.U a).ι ≫ h) (h ∣_ 𝒱.U a) (morphismRestrict_ι h (𝒱.U a))
        (τ a)

theorem

comap_restrict_eq_genRestrict

L475 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.comap_restrict_eq_genRestrict

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h]

Lean source · statement

theorem comap_restrict_eq_genRestrict (a : 𝒱.ι) {W'' : Y'.Opens} (hx' : W'' ≤ (𝒱.comap h).U a) :
    (τ.comap h).restrict hx' =
      genRestrict ((Scheme.Modules.pullback h).obj 𝓜) (h ⁻¹ᵁ 𝒱.U a).ι W''.ι (Y'.homOfLE hx')
        (Y'.homOfLE_ι hx')
        (τ.comap h a)

def

Piso

L482 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.Piso

Documentation

Compare restriction of a pullback module with pullback of its restriction along resLE.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h]

Lean source · statement

def Piso (𝓜 : Y.Modules) {W : Y.Opens} {W'' : Y'.Opens} (c : W'' ≤ h ⁻¹ᵁ W) :
    (Scheme.Modules.pullback W''.ι).obj ((Scheme.Modules.pullback h).obj 𝓜) ≅
      (Scheme.Modules.pullback (h.resLE W W'' c)).obj ((Scheme.Modules.pullback W.ι).obj 𝓜)

theorem

comap_restrict

L489 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.comap_restrict

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h]

Lean source · statement

theorem comap_restrict (a : 𝒱.ι) {W : Y.Opens} (hx : W ≤ 𝒱.U a) {W'' : Y'.Opens} (c : W'' ≤ h ⁻¹ᵁ W)
    (hx' : W'' ≤ (𝒱.comap h).U a) :
    (τ.comap h).restrict hx' =
      Piso h 𝓜 c ≪≫ (Scheme.Modules.pullback (h.resLE W W'' c)).mapIso (τ.restrict hx) ≪≫
        pullbackUnitIso (h.resLE W W'' c)

theorem

comap_transition

L516 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap.PV1TL.comap_transition

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
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 SchemeModulesCechTrivComap.AlgebraicGeometry.Scheme.Modules
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable {Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h]

Lean source · statement

theorem comap_transition (s : 𝒱.Idx 1) :
    (τ.comap h).transition s =
      (Y'.presheaf.map (homOfLE (𝒱.comap_inter_le h s)).op).hom ((h.app (𝒱.inter s)).hom
        (τ.transition s))

theorem

comap_transition

L550 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.comap_transition

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivComap
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.TopologicalSpace
universe u

Lean source · statement

theorem _root_.AlgebraicGeometry.Scheme.Modules.CechTrivialisation.comap_transition
    {Y Y' : Scheme.{u}} (h : Y' ⟶ Y) [IsAffineHom h] (𝒱 : Y.OrderedAffineCover) (𝓜 : Y.Modules)
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜) (s : 𝒱.Idx 1) :
    (τ.comap h).transition s =
      (Y'.presheaf.map (homOfLE (𝒱.comap_inter_le h s)).op).hom ((h.app (𝒱.inter s)).hom
        (τ.transition s))

Module documentation

Scheme Modules Cech Trivialisation comap transition

Declarations