Module

ProjSpaceCechTwist.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCechTwist

28 declarations indexed from sourceView source ↗

Module documentation

Monomial sections and Cech cohomology of twists on projective space.

Imports10

Mathlib.Data.Fintype.Card
Mathlib.Data.Fintype.Sets
Mathlib.Data.Fintype.Pi
Mathlib.LinearAlgebra.Finsupp.Defs
Mathlib.LinearAlgebra.Pi
Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.Order.Fin.Basic
Mathlib.Tactic.Ext
Mathlib.Tactic.SplitIfs
Lean.Elab.Tactic.Omega

Imported by25

theorem

succAbove_comp_succAbove

L36 ↗

ProjSpaceCech.Idx.succAbove_comp_succAbove

Source context 4 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech

Lean source · statement

theorem Idx.succAbove_comp_succAbove {n : ℕ} {i j : Fin (n + 2)} (H : i ≤ j) :
    Fin.succAbove j.succ ∘ Fin.succAbove i
      = Fin.succAbove i.castSucc ∘ Fin.succAbove j

abbrev

MonExp

L51 ↗

ProjSpaceCech.Twist.MonExp

Documentation

Integer exponent vectors for Laurent monomials in the projective coordinates.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

abbrev Twist.MonExp

def

negSupp

L54 ↗

ProjSpaceCech.Twist.negSupp

Documentation

The coordinate indices at which a monomial exponent is negative.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

def Twist.negSupp (a : Twist.MonExp n) : Finset (Fin (n + 1))

theorem

mem_negSupp

L57 ↗

ProjSpaceCech.Twist.mem_negSupp

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

theorem Twist.mem_negSupp {a : Twist.MonExp n} {j : Fin (n + 1)} :
    j ∈ Twist.negSupp n a ↔ a j < 0

def

Mon

L62 ↗

ProjSpaceCech.Twist.Mon

Documentation

Degree-d exponent vectors whose negative support lies in the specified coordinate set.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

def Twist.Mon (d : ℤ) (I : Finset (Fin (n + 1))) : Type

instance

instDecidableEq

L65 ↗

ProjSpaceCech.Twist.Mon.instDecidableEq

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

instance Twist.Mon.instDecidableEq (d : ℤ) (I : Finset (Fin (n + 1))) :
    DecidableEq (Twist.Mon n d I)

def

incl

L69 ↗

ProjSpaceCech.Twist.Mon.incl

Documentation

Include the monomials permitted by a coordinate set into those permitted by a larger set.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

def Twist.Mon.incl (d : ℤ) {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J) :
    Twist.Mon n d I → Twist.Mon n d J

theorem

incl_injective

L73 ↗

ProjSpaceCech.Twist.Mon.incl_injective

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

theorem Twist.Mon.incl_injective (d : ℤ) {I J : Finset (Fin (n + 1))}
    (hIJ : I ⊆ J) : Function.Injective (Twist.Mon.incl n d hIJ)

theorem

incl_val

L78 ↗

ProjSpaceCech.Twist.Mon.incl_val

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

theorem Twist.Mon.incl_val (d : ℤ) {I J : Finset (Fin (n + 1))} (hIJ : I ⊆ J)
    (a : Twist.Mon n d I) :
    (Twist.Mon.incl n d hIJ a).1 = a.1

abbrev

Sec

L83 ↗

ProjSpaceCech.Twist.Sec

Documentation

Finite coefficient sums of the degree-d monomials permitted by the specified coordinate set.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Setup
variable (n : ℕ)

Lean source · statement

abbrev Twist.Sec (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)
    (I : Finset (Fin (n + 1))) : Type u

def

Idx

L94 ↗

ProjSpaceCech.Idx

Documentation

Strictly increasing coordinate tuples indexing intersections in the given Cech degree.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

def Idx (i : ℕ) : Type

instance

instFintype

L96 ↗

ProjSpaceCech.Idx.instFintype

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Idx.instFintype (i : ℕ) : Fintype (Idx n i)

instance

instDecidableEq

L98 ↗

ProjSpaceCech.Idx.instDecidableEq

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Idx.instDecidableEq (i : ℕ) : DecidableEq (Idx n i)

def

img

L101 ↗

ProjSpaceCech.Idx.img

Documentation

The finite set of coordinates occurring in an increasing tuple.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

def Idx.img {i : ℕ} (s : Idx n i) : Finset (Fin (n + 1))

theorem

card_img

L104 ↗

ProjSpaceCech.Idx.card_img

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

theorem Idx.card_img {i : ℕ} (s : Idx n i) :
    (Idx.img n s).card = i + 1

def

face

L110 ↗

ProjSpaceCech.Idx.face

Documentation

Delete one coordinate from an increasing tuple to obtain a Cech face.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

def Idx.face {i : ℕ} (s : Idx n (i + 1)) (j : Fin (i + 2)) :
    Idx n i

theorem

img_face_subset

L114 ↗

ProjSpaceCech.Idx.img_face_subset

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

theorem Idx.img_face_subset {i : ℕ} (s : Idx n (i + 1))
    (j : Fin (i + 2)) :
    Idx.img n (Idx.face n s j) ⊆ Idx.img n s

def

faceRes

L123 ↗

ProjSpaceCech.Twist.faceRes

Documentation

The linear face restriction induced by including the permitted monomial exponent vectors.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

def Twist.faceRes {i : ℕ} (s : Idx n (i + 1)) (j : Fin (i + 2)) :
    Twist.Sec R n d (Idx.img n (Idx.face n s j))
      →ₗ[R] Twist.Sec R n d (Idx.img n s)

abbrev

cochain

L131 ↗

ProjSpaceCech.Twist.cochain

Documentation

Cech cochains with coefficients in the degree-d monomial sections on each coordinate intersection.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

abbrev Twist.cochain (i : ℕ) : Type u

instance

instAddCommGroup

L134 ↗

ProjSpaceCech.Twist.cochain.instAddCommGroup

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Twist.cochain.instAddCommGroup (i : ℕ) : AddCommGroup (Twist.cochain R n d i)

instance

instModule

L137 ↗

ProjSpaceCech.Twist.cochain.instModule

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Twist.cochain.instModule (i : ℕ) : Module R (Twist.cochain R n d i)

def

d

L143 ↗

ProjSpaceCech.Twist.d

Documentation

The alternating sum of face restrictions defining the differential for twisted Cech cochains.

Source context 4 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech

Lean source · statement

def Twist.d (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) (i : ℕ) :
    Twist.cochain R n d i →ₗ[R] Twist.cochain R n d (i + 1)

theorem

d_apply

L152 ↗

ProjSpaceCech.Twist.d_apply

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

theorem Twist.d_apply (i : ℕ) (f : Twist.cochain R n d i)
    (s : Idx n (i + 1)) :
    Twist.d R n d i f s =
      ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) •
        Twist.faceRes R n d s j (f (Idx.face n s j))

theorem

isEmpty_of_lt

L160 ↗

ProjSpaceCech.Idx.isEmpty_of_lt

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

theorem Idx.isEmpty_of_lt {i : ℕ} (hi : n < i) :
    IsEmpty (Idx n i)

theorem

cochain_subsingleton_of_lt

L167 ↗

ProjSpaceCech.Twist.cochain_subsingleton_of_lt

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section AltCech
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

theorem Twist.cochain_subsingleton_of_lt {i : ℕ} (hi : n < i) :
    Subsingleton (Twist.cochain R n d i)

def

H

L182 ↗

ProjSpaceCech.Twist.H

Documentation

Twisted Cech cohomology, using a kernel in degree zero and cocycles modulo boundaries in positive degrees.

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Cohomology
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · full declaration

def Twist.H : ℕ → Type u
  | 0 => LinearMap.ker (Twist.d R n d 0)
  | (i + 1) =>
      LinearMap.ker (Twist.d R n d (i + 1)) ⧸
        (LinearMap.range (Twist.d R n d i)).comap
          (LinearMap.ker (Twist.d R n d (i + 1))).subtype

instance

addCommGroup

L189 ↗

ProjSpaceCech.Twist.H.addCommGroup

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Cohomology
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Twist.H.addCommGroup (i : ℕ) : AddCommGroup (Twist.H R n d i)

instance

module

L196 ↗

ProjSpaceCech.Twist.H.module

Source context 6 commands

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

noncomputable section
universe u
open Finset Function
namespace ProjSpaceCech
section Cohomology
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)

Lean source · statement

instance Twist.H.module (i : ℕ) : Module R (Twist.H R n d i)

Module documentation

Declarations