NYLL
Module

Scheme_Modules_CechTrivialisation_nonempty_iso_unit_of_forall_transition_eq_one.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_nonempty_iso_unit_of_forall_transition_eq_one
59 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules Cech Trivialisation nonempty iso unit of forall transition eq one

Imports8
Imported by2

Declarations

def

uapp

L41 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.uapp
Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.unitAutSection_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.uapp_mul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.uapp_trans
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L66 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.uapp_refl
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L71 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.unitAutSection_trans
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L78 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.unitAutSection_refl
Source context 8 commands

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

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

unitAutSection_symm_mul

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.unitAutSection_symm_mul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.unitAutSection_mul_symm
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L94 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA.isUnit_unitAutSection
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
namespace L5G
namespace UA
open AlgebraicGeometry.Scheme.Modules
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

L114 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pullbackCongr_hom_app_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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

L119 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pullbackCongr_inv_app_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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

L124 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.assoc_app
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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''

L136 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.assoc_app''
Source context 9 commands

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

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

comp_congr_right

L165 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.comp_congr_right
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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

L172 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.comp_congr_left
Source context 9 commands

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

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

congr_unit

L179 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.congr_unit
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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

L185 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.congr_nat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
section coh
open _root_.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

L205 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.toU
Documentation

View a regular function as a section of the unit module.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L208 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pullbackUnitIso_hom_app_pls
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L217 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pullbackUnitIso_inv_app_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L235 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.uASm
Documentation

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

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L245 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.uASm_trans
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L247 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.isUnit_uASm
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L249 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.uASm_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L253 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.presheaf_map_op_apply_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L257 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.presheaf_comp_apply_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L265 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.unitAutSection_conj
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L311 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.genRestrict
Documentation

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

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L317 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.genRestrict_comp
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

conj_symm_trans_conj

L363 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.conj_symm_trans_conj
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L372 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.symm_trans_trans_symm_trans
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L382 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.restrict_eq_genRestrict
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L386 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.κiso
Documentation

Compare iterated pullback along an open inclusion with pullback to the smaller open.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L391 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.restrict_trans
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

θ

L402 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.θ
Documentation

The function comparing two local trivialisations on a common open subset.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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_θ

L405 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.transition_eq_θ
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L408 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.θ_res
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L431 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.θ_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L441 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.isUnit_transition
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

L444 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.cocycle
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.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

eq_refl_of_uASm_eq_one

L465 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.eq_refl_of_uASm_eq_one
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
section localAgree
variable (W : Y.Opens)
Lean source · statement
theorem eq_refl_of_uASm_eq_one
    (E : @Iso ((W : Scheme.{u}).Modules) _ (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf)
      (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf))
    (h : uASm W E = 1) : E = Iso.refl _
theorem

restrict_congr_idx

L490 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.restrict_congr_idx
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_congr_idx {a a' : 𝒱.ι} (e : a = a') {W : Y.Opens} (ha : W ≤ 𝒱.U a) (ha' : W ≤
  𝒱.U a') :
    τ.restrict ha = τ.restrict ha'
def

pair

L496 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pair
Documentation

The increasing one-simplex associated to two strictly ordered cover indices.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
def pair {a b : 𝒱.ι} (hab : a < b) : 𝒱.Idx 1
theorem

pair_zero

L501 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pair_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem pair_zero {a b : 𝒱.ι} (hab : a < b) : (pair (𝒱 := 𝒱) hab).1 0 = a
theorem

pair_one

L502 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.pair_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem pair_one {a b : 𝒱.ι} (hab : a < b) : (pair (𝒱 := 𝒱) hab).1 1 = b
theorem

le_inter_pair

L504 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.le_inter_pair
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem le_inter_pair {a b : 𝒱.ι} (hab : a < b) {W : Y.Opens} (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) :
    W ≤ 𝒱.inter (pair hab)
theorem

restrict_eq_of_lt

L511 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.restrict_eq_of_lt
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_eq_of_lt (h1 : ∀ s : 𝒱.Idx 1, τ.transition s = 1)
    {a b : 𝒱.ι} (hab : a < b) {W : Y.Opens} (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) :
    τ.restrict ha = τ.restrict hb
theorem

restrict_indep

L529 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.restrict_indep
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem restrict_indep (h1 : ∀ s : 𝒱.Idx 1, τ.transition s = 1)
    {a b : 𝒱.ι} {W : Y.Opens} (ha : W ≤ 𝒱.U a) (hb : W ≤ 𝒱.U b) :
    τ.restrict ha = τ.restrict hb
theorem

mapIso_pullbackUnitIso_trans

L537 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.mapIso_pullbackUnitIso_trans
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
Lean source · statement
theorem mapIso_pullbackUnitIso_trans {W W' : Y.Opens} (h' : W' ≤ W) :
    (Scheme.Modules.pullback (Y.homOfLE h')).mapIso (pullbackUnitIso W.ι) ≪≫ pullbackUnitIso
      (Y.homOfLE h') =
      κiso (SheafOfModules.unit Y.ringCatSheaf) h' ≪≫ pullbackUnitIso W'.ι
def

Sub

L562 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.Sub
Documentation

Open subsets contained in at least one member of the ordered affine cover.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
def Sub : Type u
def

ch

L565 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.ch
Documentation

Choose a cover member containing an open subset subordinate to the cover.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
def ch (i : Sub 𝒱) : 𝒱.ι
theorem

le_ch

L567 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.le_ch
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
theorem le_ch (i : Sub 𝒱) : i.1 ≤ 𝒱.U (ch i)
theorem

iSup_sub_eq_top

L569 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.iSup_sub_eq_top
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
theorem iSup_sub_eq_top : ⨆ i : Sub 𝒱, i.1 = ⊤
theorem

sub_basisLike

L573 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.sub_basisLike
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
theorem sub_basisLike (i j : Sub 𝒱) :
    i.1 ⊓ j.1 ≤ ⨆ (k : {k : Sub 𝒱 // k.1 ≤ i.1 ⊓ j.1}), k.1.1
def

eSub

L580 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.eSub
Documentation

Compare the module with the unit module after pullback to a subordinate open subset.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
def eSub (i : Sub 𝒱) :
    (Scheme.Modules.pullback i.1.ι).obj 𝓜 ≅
      (Scheme.Modules.pullback i.1.ι).obj (SheafOfModules.unit Y.ringCatSheaf)
theorem

eSub_compat

L585 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.eSub_compat
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
theorem eSub_compat (h1 : ∀ s : 𝒱.Idx 1, τ.transition s = 1) (i j : Sub 𝒱) (h : j.1 ≤ i.1) :
    (Scheme.Modules.pullback (Y.homOfLE h)).mapIso (eSub τ i) =
      ((Scheme.Modules.pullbackComp (Y.homOfLE h) i.1.ι).app 𝓜 ≪≫
          (Scheme.Modules.pullbackCongr (Y.homOfLE_ι h)).app 𝓜) ≪≫
        eSub τ j ≪≫
        ((Scheme.Modules.pullbackComp (Y.homOfLE h) i.1.ι).app (SheafOfModules.unit
          Y.ringCatSheaf) ≪≫
          (Scheme.Modules.pullbackCongr (Y.homOfLE_ι h)).app (SheafOfModules.unit
            Y.ringCatSheaf)).symm
theorem

main

L637 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.main
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry Opposite TopologicalSpace
universe u
open L5G.UA
namespace L5G
open _root_.AlgebraicGeometry.Scheme.Modules
open UA
variable {Y : Scheme.{u}}
variable {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules} (τ : CechTrivialisation 𝒱 𝓜)
variable (𝒱) in
Lean source · statement
theorem main (h1 : ∀ s : 𝒱.Idx 1, τ.transition s = 1) :
    Nonempty (𝓜 ≅ SheafOfModules.unit Y.ringCatSheaf)
theorem

nonempty_iso_unit_of_forall_transition_eq_one

L663 ↗
AlgebraicGeometry.Scheme.Modules.CechTrivialisation.nonempty_iso_unit_of_forall_transition_eq_one
Source context 7 commands

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

section ProofImplementation
section PublicStatement
open
  _root_.CategoryTheory
  _root_.CategoryTheory.Limits
  _root_.AlgebraicGeometry
  _root_.Opposite
  _root_.TopologicalSpace
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll.L5G.UA
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivIsoUnitAll
namespace AlgebraicGeometry.Scheme.Modules.CechTrivialisation
Lean source · statement
theorem nonempty_iso_unit_of_forall_transition_eq_one
    {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜)
    (h : ∀ s : 𝒱.Idx 1, τ.transition s = 1) :
    Nonempty (𝓜 ≅ SheafOfModules.unit Y.ringCatSheaf)

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