Module

ModulesGlueOfCocycle.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.ModulesGlueOfCocycle

46 declarations indexed from sourceView source ↗

Module documentation

Modules Glue Of Cocycle

Imports6

Mathlib.Algebra.Category.ModuleCat.Presheaf
Mathlib.AlgebraicGeometry.Modules.Sheaf
Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Mathlib.Tactic.Choose
Mathlib.Tactic.Ring
Nyll.SchemeTheory.Modules.TensorSections

Imported by12

abbrev

rO

L35 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO

Documentation

The ring homomorphism restricting regular functions along an inclusion of opens.

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

abbrev rO {A B : X.Opens} (h : B ≤ A) : Γ(X, A) →+* Γ(X, B)

theorem

rO_rO

L38 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO_rO

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

theorem rO_rO {A B C : X.Opens} (hBA : B ≤ A) (hCB : C ≤ B) (g : Γ(X, A)) :
    rO hCB (rO hBA g) = rO (hCB.trans hBA) g

theorem

rO_irrel

L43 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO_irrel

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

theorem rO_irrel {A B : X.Opens} (h h' : B ≤ A) (g : Γ(X, A)) : rO h g = rO h' g

theorem

rO_refl

L45 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO_refl

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

theorem rO_refl {A : X.Opens} (g : Γ(X, A)) : rO (le_refl A) g = g

theorem

rO_rO_self

L49 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO_rO_self

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

theorem rO_rO_self {A B : X.Opens} (h : B ≤ A) (h' : A ≤ B) (g : Γ(X, B)) : rO h (rO h' g) = g

theorem

rO_bijective_of_le_le

L52 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.rO_bijective_of_le_le

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
namespace GlueOfCocycle

Lean source · statement

theorem rO_bijective_of_le_le {A B : X.Opens} (h : B ≤ A) (h' : A ≤ B) : Function.Bijective (rO h)

structure

UnitCocycle

L62 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle

Documentation

Transition functions satisfying the identity and cocycle equations on the open cover.

Source context 5 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle

Lean source · full declaration

structure UnitCocycle (U : ι → X.Opens) where
  /-- The transition function on each pairwise intersection. -/
  u : ∀ i j, Γ(X, U i ⊓ U j)
  /-- The transition function from a chart to itself is one. -/
  refl : ∀ i, u i i = 1
  /-- The transition functions compose multiplicatively on triple intersections. -/
  cocycle : ∀ i j k,
    rO (le_inf (inf_le_left.trans inf_le_left) (inf_le_left.trans inf_le_right) : U i ⊓ U j ⊓ U k
      ≤ U i ⊓ U j) (u i j) *
      rO (le_inf (inf_le_left.trans inf_le_right) inf_le_right : U i ⊓ U j ⊓ U k ≤ U j ⊓ U k) (u j
        k) =
    rO (le_inf (inf_le_left.trans inf_le_left) inf_le_right : U i ⊓ U j ⊓ U k ≤ U i ⊓ U k) (u i k)

theorem

cocycle_le

L79 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.cocycle_le

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)

Lean source · statement

theorem cocycle_le (i j k : ι) {W : X.Opens} (hij : W ≤ U i ⊓ U j) (hjk : W ≤ U j ⊓ U k) (hik : W
  ≤ U i ⊓ U k) :
    rO hij (c.u i j) * rO hjk (c.u j k) = rO hik (c.u i k)

theorem

mul_symm

L87 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.mul_symm

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)

Lean source · statement

theorem mul_symm (i j : ι) :
    c.u i j * rO (le_of_eq (inf_comm (U i) (U j)) : U i ⊓ U j ≤ U j ⊓ U i) (c.u j i) = 1

theorem

isUnit

L94 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.isUnit

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)

Lean source · statement

theorem isUnit (i j : ι) : IsUnit (c.u i j)

def

trivial

L99 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.trivial

Documentation

The cocycle whose transition functions are all one.

Source context 8 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)
variable (U) in

Lean source · full declaration

def trivial : UnitCocycle U where
  u _ _ := 1
  refl _ := rfl
  cocycle _ _ _ := by simp only [map_one, mul_one]

def

mul

L105 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.mul

Documentation

The pointwise product of two transition cocycles.

Source context 8 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)
variable (U) in

Lean source · full declaration

def mul (c' : UnitCocycle U) : UnitCocycle U where
  u i j := c.u i j * c'.u i j
  refl i := by rw [c.refl, c'.refl, mul_one]
  cocycle i j k := by
    simp only [map_mul]
    rw [mul_mul_mul_comm, c.cocycle, c'.cocycle]

def

twist

L113 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.twist

Documentation

The cocycle obtained by changing each local frame by the specified unit.

Source context 8 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)
variable (U) in

Lean source · full declaration

def twist (h : ∀ i, Γ(X, U i)ˣ) : UnitCocycle U where
  u i j := rO inf_le_left (h i : Γ(X, U i)) * c.u i j * rO inf_le_right (↑(h j)⁻¹ : Γ(X, U j))
  refl i := by
    rw [c.refl, mul_one, rO_irrel inf_le_left inf_le_right, ← map_mul, Units.mul_inv, map_one]
  cocycle i j k := by
    simp only [map_mul, rO_rO]
    have hc := c.cocycle i j k
    have hj : rO ((le_inf (inf_le_left.trans inf_le_left) (inf_le_left.trans inf_le_right) : U i ⊓
      U j ⊓ U k ≤ U i ⊓ U j).trans
          inf_le_right) (↑(h j)⁻¹ : Γ(X, U j)) *
        rO ((le_inf (inf_le_left.trans inf_le_right) inf_le_right : U i ⊓ U j ⊓ U k ≤ U j ⊓ U
          k).trans inf_le_left)
          (h j : Γ(X, U j)) = 1 := by
      rw [rO_irrel _ ((le_inf (inf_le_left.trans inf_le_right) inf_le_right : U i ⊓ U j ⊓ U k ≤ U
        j ⊓ U k).trans inf_le_left),
        ← map_mul, Units.inv_mul, map_one]
    calc _ = rO _ (h i : Γ(X, U i)) * (rO _ (c.u i j) * rO _ (c.u j k)) *
          (rO _ (↑(h j)⁻¹ : Γ(X, U j)) * rO _ (h j : Γ(X, U j))) * rO _ (↑(h k)⁻¹ : Γ(X, U k))
            := by ring
      _ = _ := by rw [hj, mul_one, hc]

def

comap

L135 ↗

AlgebraicGeometry.Scheme.Modules.UnitCocycle.comap

Documentation

The transition cocycle pulled back along a morphism of schemes.

Source context 8 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace UnitCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U)
variable (U) in

Lean source · full declaration

def comap {X' : Scheme.{u}} (g : X' ⟶ X) : UnitCocycle (fun i => g ⁻¹ᵁ U i) where
  u i j := (g.app (U i ⊓ U j)).hom (c.u i j)
  refl i := by rw [c.refl, map_one]; rfl
  cocycle i j k := by
    have nat : ∀ {A B : X.Opens} (hBA : B ≤ A) (s : Γ(X, A)),
        GlueOfCocycle.rO (X := X') (show g ⁻¹ᵁ B ≤ g ⁻¹ᵁ A from fun _ hx => hBA hx) ((g.app A).hom
          s) =
          (g.app B).hom (rO hBA s) := by
      intro A B hBA s
      have h := CategoryTheory.ConcreteCategory.congr_hom (g.naturality (homOfLE hBA).op) s
      rw [CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ConcreteCategory.comp_apply]
        at h
      exact h.symm
    have := congrArg (g.app (U i ⊓ U j ⊓ U k)).hom (c.cocycle i j k)
    rw [map_mul, ← nat, ← nat, ← nat] at this
    exact this

theorem

leTi

L158 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.leTi

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)

Lean source · statement

theorem leTi (i j : ι) : T ⊓ (U i ⊓ U j) ≤ T ⊓ U i

theorem

leTj

L159 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.leTj

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)

Lean source · statement

theorem leTj (i j : ι) : T ⊓ (U i ⊓ U j) ≤ T ⊓ U j

theorem

leij

L160 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.leij

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)

Lean source · statement

theorem leij (i j : ι) : T ⊓ (U i ⊓ U j) ≤ U i ⊓ U j

def

families

L163 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.families

Documentation

Local section families satisfying the transition equations for the cocycle.

Source context 7 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)

Lean source · full declaration

def families : AddSubgroup (∀ i, Γ(X, T ⊓ U i)) where
  carrier := {x | ∀ i j, rO (leTi T i j) (x i) = rO (leij T i j) (c.u i j) * rO (leTj T i j) (x j)}
  zero_mem' := by intro i j; simp
  add_mem' := by
    intro x y hx hy i j
    simp only [Pi.add_apply, map_add]
    rw [hx, hy, mul_add]
  neg_mem' := by
    intro x hx i j
    simp only [Pi.neg_apply, map_neg]
    rw [hx, mul_neg]

theorem

mem_families

L177 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.mem_families

Source context 8 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}

Lean source · statement

theorem mem_families {x : ∀ i, Γ(X, T ⊓ U i)} :
    x ∈ families c T ↔ ∀ i j, rO (leTi T i j) (x i) = rO (leij T i j) (c.u i j) * rO (leTj T i j)
      (x j)

instance

instSMulFamilies

L183 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instSMulFamilies

Source context 9 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)

Lean source · full declaration

instance instSMulFamilies : SMul Γ(X, T) (families c T) where
  smul g x := ⟨fun i => rO inf_le_left g * x.1 i, by
    have hx := x.2
    rw [mem_families] at hx ⊢
    intro i j
    simp only [map_mul, rO_rO]
    rw [hx i j, rO_irrel ((leTi T i j).trans inf_le_left) ((leTj T i j).trans inf_le_left)]
    ring⟩

theorem

smul_val

L192 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.smul_val

Source context 9 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)

Lean source · statement

theorem smul_val (g : Γ(X, T)) (x : families c T) (i : ι) : (g • x).1 i = rO inf_le_left g * x.1 i

instance

instModuleFamilies

L195 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instModuleFamilies

Source context 9 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)

Lean source · full declaration

instance instModuleFamilies : Module Γ(X, T) (families c T) where
  one_smul x := by apply Subtype.ext; funext i; rw [smul_val]; simp
  mul_smul a b x := by apply Subtype.ext; funext i; simp only [smul_val, map_mul, mul_assoc]
  smul_zero a := by apply Subtype.ext; funext i; rw [smul_val]; simp
  smul_add a x y := by
    apply Subtype.ext
    funext i
    simp only [smul_val, AddSubgroup.coe_add, Pi.add_apply, mul_add]
  add_smul a b x := by
    apply Subtype.ext
    funext i
    simp only [smul_val, map_add, add_mul, AddSubgroup.coe_add, Pi.add_apply]
  zero_smul x := by apply Subtype.ext; funext i; rw [smul_val]; simp

def

resFam

L212 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.resFam

Documentation

The additive restriction map on compatible local section families.

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · full declaration

def resFam {T T' : X.Opens} (h : T' ≤ T) : families c T →+ families c T' where
  toFun x := ⟨fun i => rO (inf_le_inf_right (U i) h) (x.1 i), by
    have hx := x.2
    rw [mem_families] at hx ⊢
    intro i j
    rw [rO_rO, rO_rO]
    have e1 : rO ((leTi T' i j).trans (inf_le_inf_right (U i) h)) (x.1 i) =
        rO (inf_le_inf_right (U i ⊓ U j) h) (rO (leTi T i j) (x.1 i)) := by rw [rO_rO]
    have e2 : rO ((leTj T' i j).trans (inf_le_inf_right (U j) h)) (x.1 j) =
        rO (inf_le_inf_right (U i ⊓ U j) h) (rO (leTj T i j) (x.1 j)) := by rw [rO_rO]
    rw [e1, e2, hx i j, map_mul, rO_rO]⟩
  map_zero' := by apply Subtype.ext; funext i; simp
  map_add' x y := by apply Subtype.ext; funext i; simp

theorem

resFam_val

L226 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.resFam_val

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · statement

theorem resFam_val {T T' : X.Opens} (h : T' ≤ T) (x : families c T) (i : ι) :
    (resFam c h x).1 i = rO (inf_le_inf_right (U i) h) (x.1 i)

def

preGlue

L230 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.preGlue

Documentation

The presheaf of compatible local section families.

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · full declaration

def preGlue : (Opens X)ᵒᵖ ⥤ Ab where
  obj T := AddCommGrpCat.of (families c T.unop)
  map {T T'} f := AddCommGrpCat.ofHom (resFam c f.unop.le)
  map_id T := by
    ext
    exact rO_refl _
  map_comp {T₁ T₂ T₃} f g := by
    ext
    exact (rO_rO _ _ _).symm

instance

instModulePreGlue

L240 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.instModulePreGlue

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · statement

instance instModulePreGlue (T : (Opens X)ᵒᵖ) :
    Module (X.ringCatSheaf.obj.obj T) ((preGlue c).obj T)

theorem

preGlue_map_smul

L244 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.preGlue_map_smul

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · statement

theorem preGlue_map_smul ⦃T T' : (Opens X)ᵒᵖ⦄ (f : T ⟶ T') (r : X.ringCatSheaf.obj.obj T) (m :
  (preGlue c).obj T) :
    (preGlue c).map f (r • m) = X.ringCatSheaf.obj.map f r • (preGlue c).map f m

def

preGlueMod

L254 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.preGlueMod

Documentation

The compatible-family presheaf with its module structure over regular functions.

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · statement

def preGlueMod : _root_.PresheafOfModules X.ringCatSheaf.obj

theorem

preGlue_isSheaf

L257 ↗

AlgebraicGeometry.Scheme.Modules.GlueOfCocycle.preGlue_isSheaf

Source context 10 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
namespace GlueOfCocycle
variable {U : ι → X.Opens} (c : UnitCocycle U) (T : X.Opens)
variable {c T}
variable (c T)
variable {T}

Lean source · statement

theorem preGlue_isSheaf : TopCat.Presheaf.IsSheaf (preGlue c)

def

glueOfCocycle

L309 ↗

AlgebraicGeometry.Scheme.Modules.glueOfCocycle

Documentation

The sheaf of modules obtained by gluing with the transition cocycle.

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

def glueOfCocycle (c : UnitCocycle U) : X.Modules

theorem

glueOfCocycle_sections_eq

L312 ↗

AlgebraicGeometry.Scheme.Modules.glueOfCocycle_sections_eq

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueOfCocycle_sections_eq (c : UnitCocycle U) (T : X.Opens) :
    (Γ(glueOfCocycle c, T) : Type u) = GlueOfCocycle.families c T

theorem

glue_map_val

L315 ↗

AlgebraicGeometry.Scheme.Modules.glue_map_val

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glue_map_val (c : UnitCocycle U) {T T' : X.Opens} (h : T' ≤ T) (p : Γ(glueOfCocycle c, T))
  (i : ι) :
    (((glueOfCocycle c).presheaf.map (homOfLE h).op p : Γ(glueOfCocycle c, T')) :
      GlueOfCocycle.families c T').1 i =
      rO (inf_le_inf_right (U i) h) ((p : GlueOfCocycle.families c T).1 i)

theorem

glue_smul_val

L321 ↗

AlgebraicGeometry.Scheme.Modules.glue_smul_val

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glue_smul_val (c : UnitCocycle U) {T : X.Opens} (g : Γ(X, T)) (p : Γ(glueOfCocycle c, T))
  (i : ι) :
    ((g • p : Γ(glueOfCocycle c, T)) : GlueOfCocycle.families c T).1 i =
      rO inf_le_left g * (p : GlueOfCocycle.families c T).1 i

def

glueComponent

L327 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent

Documentation

The local component of a section of the glued sheaf.

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · full declaration

def glueComponent (c : UnitCocycle U) (T : X.Opens) (i : ι) : Γ(glueOfCocycle c, T)
  →+ Γ(X, T ⊓ U i) where
  toFun p := (p : GlueOfCocycle.families c T).1 i
  map_zero' := rfl
  map_add' _ _ := rfl

theorem

glueComponent_apply

L333 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_apply

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_apply (c : UnitCocycle U) (T : X.Opens) (i : ι) (p : Γ(glueOfCocycle c, T)) :
    glueComponent c T i p = (p : GlueOfCocycle.families c T).1 i

theorem

glue_ext

L336 ↗

AlgebraicGeometry.Scheme.Modules.glue_ext

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glue_ext (c : UnitCocycle U) {T : X.Opens} {p q : Γ(glueOfCocycle c, T)}
    (h : ∀ i, glueComponent c T i p = glueComponent c T i q) : p = q

theorem

glueComponent_transition

L340 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_transition

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_transition (c : UnitCocycle U) (T : X.Opens) (i j : ι) (p : Γ(glueOfCocycle
  c, T)) :
    rO (GlueOfCocycle.leTi T i j) (glueComponent c T i p) =
      rO (GlueOfCocycle.leij T i j) (c.u i j) * rO (GlueOfCocycle.leTj T i j) (glueComponent c T j
        p)

theorem

glueComponent_map

L347 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_map

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_map (c : UnitCocycle U) {T T' : X.Opens} (h : T' ≤ T) (i : ι) (p :
  Γ(glueOfCocycle c, T)) :
    glueComponent c T' i ((glueOfCocycle c).presheaf.map (homOfLE h).op p) =
      rO (inf_le_inf_right (U i) h) (glueComponent c T i p)

theorem

glueComponent_smul

L352 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_smul

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_smul (c : UnitCocycle U) {T : X.Opens} (g : Γ(X, T)) (i : ι) (p :
  Γ(glueOfCocycle c, T)) :
    glueComponent c T i (g • p) = rO inf_le_left g * glueComponent c T i p

def

glueMk

L357 ↗

AlgebraicGeometry.Scheme.Modules.glueMk

Documentation

The section of the glued sheaf determined by a compatible local family.

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

def glueMk (c : UnitCocycle U) (T : X.Opens) (x : ∀ i, Γ(X, T ⊓ U i))
    (hx : ∀ i j, rO (GlueOfCocycle.leTi T i j) (x i) =
      rO (GlueOfCocycle.leij T i j) (c.u i j) * rO (GlueOfCocycle.leTj T i j) (x j)) :
        Γ(glueOfCocycle c, T)

theorem

glueComponent_glueMk

L363 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_glueMk

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_glueMk (c : UnitCocycle U) (T : X.Opens) (x : ∀ i, Γ(X, T ⊓ U i))
    (hx : ∀ i j, rO (GlueOfCocycle.leTi T i j) (x i) =
      rO (GlueOfCocycle.leij T i j) (c.u i j) * rO (GlueOfCocycle.leTj T i j) (x j)) (i : ι) :
    glueComponent c T i (glueMk c T x hx) = x i

def

glueFrame

L369 ↗

AlgebraicGeometry.Scheme.Modules.glueFrame

Documentation

The local frame of the glued sheaf associated to a cover member.

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

def glueFrame (c : UnitCocycle U) (i : ι) : Γ(glueOfCocycle c, U i)

theorem

glueComponent_glueFrame

L374 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_glueFrame

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_glueFrame (c : UnitCocycle U) (i k : ι) :
    glueComponent c (U i) k (glueFrame c i) = rO (le_of_eq (inf_comm (U i) (U k))) (c.u k i)

theorem

glueComponent_glueFrame_self

L377 ↗

AlgebraicGeometry.Scheme.Modules.glueComponent_glueFrame_self

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem glueComponent_glueFrame_self (c : UnitCocycle U) (i : ι) :
    glueComponent c (U i) i (glueFrame c i) = 1

theorem

isFrameOn_glueFrame

L381 ↗

AlgebraicGeometry.Scheme.Modules.isFrameOn_glueFrame

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem isFrameOn_glueFrame (c : UnitCocycle U) (i : ι) : IsFrameOn (glueFrame c i) (U i)

theorem

map_glueFrame_eq_smul

L406 ↗

AlgebraicGeometry.Scheme.Modules.map_glueFrame_eq_smul

Source context 6 commands

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

universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.Modules
variable {X : Scheme.{u}} {ι : Type u}
open GlueOfCocycle
variable {U : ι → X.Opens}

Lean source · statement

theorem map_glueFrame_eq_smul (c : UnitCocycle U) (i j : ι) :
    (glueOfCocycle c).presheaf.map (homOfLE (inf_le_right : U i ⊓ U j ≤ U j)).op (glueFrame c j) =
      c.u i j • (glueOfCocycle c).presheaf.map (homOfLE (inf_le_left : U i ⊓ U j ≤ U i)).op
        (glueFrame c i)

Module documentation

Modules Glue Of Cocycle

Declarations