Module

Scheme_Modules_CechTrivialisation_exists_forall_transition_eq_mul_mul.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_Modules_CechTrivialisation_exists_forall_transition_eq_mul_mul

16 declarations indexed from sourceView source ↗

Module documentation

Writing transition functions of a module trivialisation as products of local units.

Imports7

Imported by2

theorem

opHom_eq

L37 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.opHom_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem opHom_eq {A B : (Y.Opens)ᵒᵖ} (f g : A ⟶ B) : f = g

theorem

presheaf_map_eq

L40 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.presheaf_map_eq

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem presheaf_map_eq {A B : (Y.Opens)ᵒᵖ} (f g : A ⟶ B) : Y.presheaf.map f = Y.presheaf.map g

def

secOf

L45 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.secOf

Documentation

The section of the unit sheaf obtained by restricting a function on the open subscheme.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

def secOf (W : Y.Opens) (r : Γ(Y, W)) :
    (SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf).sections

theorem

secOf_val

L55 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.secOf_val

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem secOf_val (W : Y.Opens) (r : Γ(Y, W)) (V : ((W : Scheme.{u}).Opens)ᵒᵖ) :
    (secOf W r).val V = (W : Scheme.{u}).presheaf.map (homOfLE (le_top (a := V.unop))).op
      (W.topIso.inv r)

def

mulHom

L60 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.mulHom

Documentation

The endomorphism of the unit sheaf given by multiplication by a section.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

def mulHom (W : Y.Opens) (r : Γ(Y, W)) :
    SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ⟶ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf

theorem

mulHom_app

L65 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.mulHom_app

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem mulHom_app (W : Y.Opens) (r : Γ(Y, W)) (V : ((W : Scheme.{u}).Opens)ᵒᵖ)
    (x : (W : Scheme.{u}).presheaf.obj V) :
    ((mulHom W r).val.app V).hom x =
      x * (W : Scheme.{u}).presheaf.map (homOfLE (le_top (a := V.unop))).op (W.topIso.inv r)

theorem

secOf_val_mul

L70 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.secOf_val_mul

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem secOf_val_mul (W : Y.Opens) (r r' : Γ(Y, W)) (V : ((W : Scheme.{u}).Opens)ᵒᵖ) :
    (W : Scheme.{u}).presheaf.map (homOfLE (le_top (a := V.unop))).op (W.topIso.inv r) *
      (W : Scheme.{u}).presheaf.map (homOfLE (le_top (a := V.unop))).op (W.topIso.inv r') =
    (W : Scheme.{u}).presheaf.map (homOfLE (le_top (a := V.unop))).op (W.topIso.inv (r * r'))

theorem

mulHom_comp

L76 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.mulHom_comp

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem mulHom_comp (W : Y.Opens) (r r' : Γ(Y, W)) (h : r * r' = 1) :
    mulHom W r ≫ mulHom W r' = 𝟙 _

def

mulIso

L87 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.mulIso

Documentation

The isomorphism of the unit sheaf given by two mutually inverse sections.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · full declaration

def mulIso (W : Y.Opens) (r r' : Γ(Y, W)) (h : r * r' = 1) :
    SheafOfModules.unit (W : Scheme.{u}).ringCatSheaf ≅ SheafOfModules.unit (W :
      Scheme.{u}).ringCatSheaf where
  hom := mulHom W r
  inv := mulHom W r'
  hom_inv_id := mulHom_comp W r r' h
  inv_hom_id := mulHom_comp W r' r (by rw [mul_comm]; exact h)

abbrev

UMod

L96 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.UMod

Documentation

The unit module on the open subscheme.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

abbrev UMod (W : Y.Opens) : (W : Scheme.{u}).Modules

def

mulIsoM

L100 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.mulIsoM

Documentation

Multiplication by mutually inverse sections, viewed as an isomorphism of scheme modules.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · full declaration

def mulIsoM (W : Y.Opens) (r r' : Γ(Y, W)) (h : r * r' = 1) : UMod W ≅ UMod W where
  hom := (mulIso W r r' h).hom
  inv := (mulIso W r r' h).inv
  hom_inv_id := (mulIso W r r' h).hom_inv_id
  inv_hom_id := (mulIso W r r' h).inv_hom_id

theorem

unitAutSection_mulIso

L106 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.unitAutSection_mulIso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem unitAutSection_mulIso (W : Y.Opens) (r r' : Γ(Y, W)) (h : r * r' = 1) :
    Scheme.Modules.unitAutSection W (mulIsoM W r r' h) = r

theorem

map4

L118 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.map4

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem map4 {A B C D E : (Y.Opens)ᵒᵖ} (a : A ⟶ B) (b : B ⟶ C) (c' : C ⟶ D) (d : D ⟶ E) (e : A ⟶ E)
    (x : Y.presheaf.obj A) :
    (Y.presheaf.map d).hom ((Y.presheaf.map c').hom ((Y.presheaf.map b).hom ((Y.presheaf.map
      a).hom x))) =
      (Y.presheaf.map e).hom x

theorem

unitAutSection_conj_mulIso

L126 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.unitAutSection_conj_mulIso

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem unitAutSection_conj_mulIso {W W' : Y.Opens} (hle : W' ≤ W) (r r' : Γ(Y, W)) (h : r * r'
  = 1) :
    Scheme.Modules.unitAutSection W'
      ((Scheme.Modules.pullbackUnitIso (Y.homOfLE hle)).symm ≪≫
        (Scheme.Modules.pullback (Y.homOfLE hle)).mapIso (mulIsoM W r r' h) ≪≫
        Scheme.Modules.pullbackUnitIso (Y.homOfLE hle)) =
      (Y.presheaf.map (homOfLE hle).op).hom r

theorem

restrictIso_trans

L141 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll.L4Asm.restrictIso_trans

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
namespace L4Asm
variable {Y : Scheme.{u}}

Lean source · statement

theorem restrictIso_trans
    {C₀ : Type*} {C₁ : Type*} [Category C₀] [Category C₁] (F : C₀ ⥤ C₁)
    {M N : C₀} {A B T : C₁} (a : A ≅ B) (b : B ≅ F.obj M)
    (t : M ≅ N) (m : N ≅ N) (e : F.obj N ≅ T) :
    a ≪≫ b ≪≫ F.mapIso (t ≪≫ m) ≪≫ e =
      (a ≪≫ b ≪≫ F.mapIso t ≪≫ e) ≪≫ e.symm ≪≫ F.mapIso m ≪≫ e

theorem

exists_forall_transition_eq_mul_mul

L152 ↗

AlgebraicGeometry.Scheme.Modules.CechTrivialisation.exists_forall_transition_eq_mul_mul

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SchemeModulesCechTrivExistsAll
universe u
open CategoryTheory Opposite AlgebraicGeometry
open L4Asm in

Lean source · statement

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.CechTrivialisation.exists_forall_transition_eq_mul_mul
    {Y : Scheme.{u}} {𝒱 : Y.OrderedAffineCover} {𝓜 : Y.Modules}
    (τ : Scheme.Modules.CechTrivialisation 𝒱 𝓜)
    (c c' : ∀ a : 𝒱.ι, Γ(Y, 𝒱.U a)) (hc : ∀ a : 𝒱.ι, c a * c' a = 1) :
    ∃ τ' : Scheme.Modules.CechTrivialisation 𝒱 𝓜,
      (∀ a : 𝒱.ι, Scheme.Modules.unitAutSection (𝒱.U a) ((τ a).symm ≪≫ τ' a) = c a) ∧
      ∀ s : 𝒱.Idx 1,
        τ'.transition s = τ.transition s *
          (Y.presheaf.map (homOfLE (𝒱.inter_le s 0)).op).hom (c' (s.1 0)) *
          (Y.presheaf.map (homOfLE (𝒱.inter_le s 1)).op).hom (c (s.1 1))

Module documentation

Declarations