NYLL
Module

BoundedCochainTensor.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.BoundedCochainTensor
19 declarations indexed from sourceView source ↗

Module documentation

Bounded Cochain Tensor

Imports4
Imported by2

Declarations

def

preimageFamily

L29 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily
Documentation

The family of opens obtained by taking inverse images of the ordered affine cover.

Source context 3 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
Lean source · statement
def AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily {P Y : Scheme.{u}} (K
  : Y.OrderedAffineCover)
    (q : P ⟶ Y) : P.OrderedOpenFamily
theorem

preimageFamily_ι

L34 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily_ι
Source context 3 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
Lean source · statement
theorem AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily_ι {P Y : Scheme.{u}} (K :
  Y.OrderedAffineCover)
    (q : P ⟶ Y) : (K.preimageFamily q).ι = K.ι
theorem

preimageFamily_U

L38 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily_U
Source context 3 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
Lean source · statement
theorem AlgebraicGeometry.Scheme.OrderedAffineCover.preimageFamily_U {P Y : Scheme.{u}} (K :
  Y.OrderedAffineCover)
    (q : P ⟶ Y) (i : K.ι) : (K.preimageFamily q).U i = q ⁻¹ᵁ K.U i
structure

Bounded

L45 ↗
CochainCx.Bounded
Documentation

A cochain complex of modules that is zero in sufficiently large degree.

Source context 4 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
Lean source · full declaration
structure Bounded (R : Type u) [CommRing R] where
  /-- The module in each degree. -/
  X : ℕ → Type u
  /-- The additive commutative group structure in each degree. -/
  [abGrp : ∀ n, AddCommGroup (X n)]
  /-- The scalar module structure in each degree. -/
  [modR : ∀ n, Module R (X n)]
  /-- The differential from each degree to the next. -/
  d : ∀ n, X n →ₗ[R] X (n + 1)
  /-- The composite of successive differentials is zero. -/
  d_sq : ∀ n, d (n + 1) ∘ₗ d n = 0
  /-- The degree above which all terms vanish. -/
  N : ℕ
  /-- Each term at or above the bound is a subsingleton. -/
  hBound : ∀ n, N ≤ n → Subsingleton (X n)
def

B

L68 ↗
CochainCx.Bounded.B
Documentation

The submodule of coboundaries inside the cocycles.

Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · full declaration
def B : (n : ℕ) → Submodule R (LinearMap.ker (C.d n))
  | 0 => ⊥
  | n + 1 => (LinearMap.range (C.d n)).comap (LinearMap.ker (C.d (n + 1))).subtype
abbrev

H

L73 ↗
CochainCx.Bounded.H
Documentation

The cohomology module in the specified degree.

Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
abbrev H (n : ℕ) : Type u
abbrev

hfinrank

L76 ↗
CochainCx.Bounded.hfinrank
Documentation

The rank of the cohomology module in the specified degree.

Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
abbrev hfinrank (n : ℕ) : ℕ
theorem

B_zero

L78 ↗
CochainCx.Bounded.B_zero
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem B_zero : C.B 0 = ⊥
theorem

B_succ

L80 ↗
CochainCx.Bounded.B_succ
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem B_succ (n : ℕ) :
    C.B (n + 1) = (LinearMap.range (C.d n)).comap (LinearMap.ker (C.d (n + 1))).subtype
def

tensor

L84 ↗
CochainCx.Bounded.tensor
Documentation

The bounded double complex obtained by tensoring two bounded cochain complexes.

Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · full declaration
def tensor : DoubleComplex.Bounded R where
  C p q := C.X p ⊗[R] D.X q
  dH p q := (C.d p).rTensor (D.X q)
  dV p q := (D.d q).lTensor (C.X p)
  dH_sq p q := by
    rw [← LinearMap.rTensor_comp, C.d_sq, LinearMap.rTensor_zero]
  dV_sq p q := by
    rw [← LinearMap.lTensor_comp, D.d_sq, LinearMap.lTensor_zero]
  dHV_comm p q := by
    ext x y
    simp
  N := max C.N D.N
  hBound p q h := by
    rcases h with h | h
    · have := C.hBound p (le_of_max_le_left h)
      infer_instance
    · have := D.hBound q (le_of_max_le_right h)
      infer_instance
theorem

tensor_C

L103 ↗
CochainCx.Bounded.tensor_C
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem tensor_C (p q : ℕ) : (C.tensor D).C p q = (C.X p ⊗[R] D.X q)
theorem

tensor_dH

L104 ↗
CochainCx.Bounded.tensor_dH
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem tensor_dH (p q : ℕ) : (C.tensor D).dH p q = (C.d p).rTensor (D.X q)
theorem

tensor_dV

L105 ↗
CochainCx.Bounded.tensor_dV
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem tensor_dV (p q : ℕ) : (C.tensor D).dV p q = (D.d q).lTensor (C.X p)
theorem

tensor_N

L106 ↗
CochainCx.Bounded.tensor_N
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem tensor_N : (C.tensor D).N = max C.N D.N
def

ofCech

L109 ↗
CochainCx.Bounded.ofCech
Documentation

The bounded cochain complex associated to the given finite Čech cover.

Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · full declaration
def ofCech {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} (F : OModulePresheaf π) (K :
  V.OrderedAffineCover)
    (hdd : ∀ i, F.d K (i + 1) ∘ₗ F.d K i = 0) : Bounded R where
  X i := F.cochain K i
  d i := F.d K i
  d_sq := hdd
  N := Fintype.card K.ι
  hBound n hn := by
    have : IsEmpty (K.Idx n) := by
      refine ⟨fun s => ?_⟩
      have := Fintype.card_le_of_injective s.1 s.2.injective
      simp only [Fintype.card_fin] at this
      omega
    infer_instance
theorem

ofCech_X

L124 ↗
CochainCx.Bounded.ofCech_X
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem ofCech_X {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} (F : OModulePresheaf π) (K :
  V.OrderedAffineCover)
    (hdd : ∀ i, F.d K (i + 1) ∘ₗ F.d K i = 0) (i : ℕ) : (ofCech F K hdd).X i = F.cochain K i
theorem

ofCech_d

L128 ↗
CochainCx.Bounded.ofCech_d
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem ofCech_d {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} (F : OModulePresheaf π) (K :
  V.OrderedAffineCover)
    (hdd : ∀ i, F.d K (i + 1) ∘ₗ F.d K i = 0) (i : ℕ) : (ofCech F K hdd).d i = F.d K i
theorem

ofCech_H_succ

L132 ↗
CochainCx.Bounded.ofCech_H_succ
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem ofCech_H_succ {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} (F : OModulePresheaf π)
  (K : V.OrderedAffineCover)
    (hdd : ∀ i, F.d K (i + 1) ∘ₗ F.d K i = 0) (i : ℕ) : (ofCech F K hdd).H (i + 1) = F.HSucc K i
theorem

ofCech_H_zero

L137 ↗
CochainCx.Bounded.ofCech_H_zero
Source context 7 commands

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

noncomputable section
universe u
open TensorProduct AlgebraicGeometry
namespace CochainCx
attribute [instance] Bounded.abGrp Bounded.modR
namespace Bounded
variable {R : Type u} [CommRing R] (C D : Bounded R)
Lean source · statement
theorem ofCech_H_zero {V : Scheme.{u}} {π : V ⟶ Spec (CommRingCat.of R)} (F : OModulePresheaf π)
  (K : V.OrderedAffineCover)
    (hdd : ∀ i, F.d K (i + 1) ∘ₗ F.d K i = 0) :
    (ofCech F K hdd).H 0 = ((F.H0 K) ⧸ (⊥ : Submodule R (F.H0 K)))

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