Module

ProjSpaceCech_Twist_finite_cohomology.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_Twist_finite_cohomology

58 declarations indexed from sourceView source ↗

Module documentation

Finiteness of twist cohomology on projective space through the monomial Cech complex.

Imports7

Mathlib.Data.Finset.Sort
Mathlib.LinearAlgebra.Finsupp.LSum
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.Algebra.BigOperators.Fin
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Finsupp
Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCechTwist

Imported by2

theorem

subsingleton_cohomology_of_lt

L47 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.subsingleton_cohomology_of_lt

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Cohomology
variable (R : Type u) [CommRing R] (n : ℕ) (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

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

theorem

idx_canonical

L63 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.idx_canonical

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.idx_canonical {i : ℕ} (s : Idx n i) :
    s.1 = (Idx.img n s).orderEmbOfFin (Idx.card_img n s)

theorem

idx_eq_of_img

L68 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.idx_eq_of_img

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.idx_eq_of_img {i : ℕ} {s t : Idx n i}
    (h : Idx.img n s = Idx.img n t) : s = t

theorem

img_face

L76 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_face

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_face {i : ℕ} (s : Idx n (i + 1))
    (j : Fin (i + 2)) :
    Idx.img n (Idx.face n s j)
      = (Idx.img n s).erase (s.1 j)

def

altOfFinset

L94 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altOfFinset

Documentation

The increasing Cech index enumerating a finite coordinate subset of the specified cardinality.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.altOfFinset {i : ℕ} (T : Finset (Fin (n + 1))) (hT : T.card = i + 1) :
    Idx n i

theorem

img_altOfFinset

L99 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_altOfFinset

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_altOfFinset {i : ℕ} (T : Finset (Fin (n + 1)))
    (hT : T.card = i + 1) :
    Idx.img n (Twist.altOfFinset T hT) = T

def

altPos

L107 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altPos

Documentation

The position of a coordinate in the increasing enumeration of the Cech index.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.altPos {i : ℕ} (s : Idx n i) (j : Fin (n + 1))
    (hj : j ∈ Idx.img n s) : Fin (i + 1)

theorem

idx_val_altPos

L112 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.idx_val_altPos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.idx_val_altPos {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∈ Idx.img n s) :
    s.1 (Twist.altPos s j hj) = j

theorem

altPos_val

L119 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altPos_val

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.altPos_val {i : ℕ} (s : Idx n i) (p : Fin (i + 1)) :
    Twist.altPos s (s.1 p) (Finset.mem_image_of_mem _ (Finset.mem_univ p)) = p

def

altInsert

L125 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altInsert

Documentation

The increasing Cech index obtained by inserting a new coordinate.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.altInsert {i : ℕ} (s : Idx n i) (j : Fin (n + 1))
    (hj : j ∉ Idx.img n s) : Idx n (i + 1)

theorem

img_altInsert

L131 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_altInsert

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_altInsert {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∉ Idx.img n s) :
    Idx.img n (Twist.altInsert s j hj)
      = insert j (Idx.img n s)

def

insPos

L139 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.insPos

Documentation

The position occupied by the inserted coordinate in the enlarged Cech index.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.insPos {i : ℕ} (s : Idx n i) (j : Fin (n + 1))
    (hj : j ∉ Idx.img n s) : Fin (i + 2)

theorem

altInsert_val_insPos

L145 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altInsert_val_insPos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.altInsert_val_insPos {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∉ Idx.img n s) :
    (Twist.altInsert s j hj).1 (Twist.insPos s j hj) = j

theorem

face_altInsert_insPos

L151 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.face_altInsert_insPos

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.face_altInsert_insPos {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∉ Idx.img n s) :
    Idx.face n (Twist.altInsert s j hj)
      (Twist.insPos s j hj) = s

theorem

img_face_altInsert_ne

L160 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_face_altInsert_ne

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_face_altInsert_ne {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∉ Idx.img n s)
    (k : Fin (i + 2)) (hk : k ≠ Twist.insPos s j hj) :
    ∃ (m : Fin (n + 1)), m ∈ Idx.img n s ∧ m ≠ j ∧
      Idx.img n (Idx.face n (Twist.altInsert s j hj) k)
        = insert j ((Idx.img n s).erase m)

def

coeff

L190 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff

Documentation

The coefficient of a Laurent monomial on the specified Cech chart, extended by zero outside its admissible support.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.coeff {i : ℕ} (f : Twist.cochain R n d i)
    (s : Idx n i) (a : Twist.MonExp n) : R

theorem

coeff_eq

L196 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_eq {i : ℕ} (f : Twist.cochain R n d i)
    (s : Idx n i) (a : Twist.Mon n d (Idx.img n s)) :
    Twist.coeff R d f s a.1 = f s a

theorem

coeff_of_not

L203 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_of_not

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_of_not {i : ℕ} (f : Twist.cochain R n d i)
    (s : Idx n i) (a : Twist.MonExp n)
    (h : ¬ Twist.negSupp n a ⊆ Idx.img n s) :
    Twist.coeff R d f s a = 0

theorem

coeff_add

L210 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_add

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_add {i : ℕ} (f g : Twist.cochain R n d i)
    (s : Idx n i) (a : Twist.MonExp n) :
    Twist.coeff R d (f + g) s a
      = Twist.coeff R d f s a + Twist.coeff R d g s a

theorem

coeff_smul

L221 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_smul

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_smul {i : ℕ} (r : R) (f : Twist.cochain R n d i)
    (s : Idx n i) (a : Twist.MonExp n) :
    Twist.coeff R d (r • f) s a = r • Twist.coeff R d f s a

theorem

ext_coeff

L231 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.ext_coeff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.ext_coeff {i : ℕ} {f g : Twist.cochain R n d i}
    (h : ∀ s a, Twist.coeff R d f s a = Twist.coeff R d g s a) :
    f = g

theorem

coeff_d

L239 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_d

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_d {i : ℕ} (f : Twist.cochain R n d i)
    (s : Idx n (i + 1)) (a : Twist.MonExp n) :
    Twist.coeff R d (Twist.d R n d i f) s a
      = ∑ j : Fin (i + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          Twist.coeff R d f (Idx.face n s j) a

theorem

coeff_piSingle

L267 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_piSingle

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · full declaration

theorem Twist.coeff_piSingle {i : ℕ} (s₀ : Idx n i)
    (b₀ : Twist.Mon n d (Idx.img n s₀)) (r : R)
    (s : Idx n i) (a : Twist.MonExp n) :
    Twist.coeff R d (Pi.single s₀ (Finsupp.single b₀ r)) s a
      = if s = s₀ ∧ a = b₀.1 then r else 0 := by
  classical
  by_cases hsa : s = s₀ ∧ a = b₀.1
  · obtain ⟨rfl, rfl⟩ := hsa
    rw [ite_eq_left ⟨rfl, rfl⟩, Twist.coeff_eq, Pi.single_eq_same, Finsupp.single_eq_same]
  · rw [ite_eq_right hsa, Twist.coeff]
    split_ifs with hok
    · by_cases hs : s = s₀
      · subst hs
        erw [Pi.single_eq_same, Finsupp.single_apply, ite_eq_right]
        intro heq
        exact hsa ⟨rfl, (Subtype.ext_iff.mp heq : b₀.1 = a).symm⟩
      · erw [Pi.single_eq_of_ne hs, Finsupp.zero_apply]
    · rfl

def

posMin

L288 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.posMin

Documentation

The least coordinate outside the negative support of a Laurent monomial.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.posMin (a : Twist.MonExp n)
    (ha : Twist.negSupp n a ≠ univ) : Fin (n + 1)

theorem

posMin_notMem_negSupp

L295 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.posMin_notMem_negSupp

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homotopy
variable {n : ℕ}
variable (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.posMin_notMem_negSupp (a : Twist.MonExp n)
    (ha : Twist.negSupp n a ≠ univ) :
    Twist.posMin a ha ∉ Twist.negSupp n a

theorem

altPos_eq_card

L311 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.altPos_eq_card

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Rank
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.altPos_eq_card {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∈ Idx.img n s) :
    (Twist.altPos s j hj : ℕ) = #((Idx.img n s).filter (· < j))

theorem

insPos_eq_card

L325 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.insPos_eq_card

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Rank
variable {n : ℕ}
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.insPos_eq_card {i : ℕ} (s : Idx n i)
    (j : Fin (n + 1)) (hj : j ∉ Idx.img n s) :
    (Twist.insPos s j hj : ℕ) = #((Idx.img n s).filter (· < j))

theorem

img_subset_altInsert

L338 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_subset_altInsert

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_subset_altInsert {i : ℕ} (s : Idx n i)
    (j₁ : Fin (n + 1)) (hj : j₁ ∉ Idx.img n s) :
    Idx.img n s ⊆ Idx.img n (Twist.altInsert s j₁ hj)

def

hj

L345 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.hj

Documentation

The signed contraction inserting the specified coordinate in the twist Cech complex.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.hj (j₁ : Fin (n + 1)) (i : ℕ) :
    Twist.cochain R n d (i + 1) →ₗ[R] Twist.cochain R n d i

theorem

hj_apply_of_mem

L357 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.hj_apply_of_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.hj_apply_of_mem (j₁ : Fin (n + 1)) {i : ℕ}
    (f : Twist.cochain R n d (i + 1)) (s : Idx n i)
    (hmem : j₁ ∈ Idx.img n s) :
    Twist.hj R d j₁ i f s = 0

theorem

coeff_hj_of_mem

L365 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_hj_of_mem

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_hj_of_mem (j₁ : Fin (n + 1)) {i : ℕ}
    (f : Twist.cochain R n d (i + 1)) (s : Idx n i)
    (a : Twist.MonExp n) (hmem : j₁ ∈ Idx.img n s) :
    Twist.coeff R d (Twist.hj R d j₁ i f) s a = 0

theorem

coeff_hj

L374 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_hj

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_hj (j₁ : Fin (n + 1)) {i : ℕ}
    (f : Twist.cochain R n d (i + 1)) (s : Idx n i)
    (a : Twist.MonExp n) (hjs : j₁ ∉ Idx.img n s)
    (ha : Twist.negSupp n a ⊆ Idx.img n s) :
    Twist.coeff R d (Twist.hj R d j₁ i f) s a
      = ((-1 : ℤ) ^ (Twist.insPos s j₁ hjs : ℕ)) •
          Twist.coeff R d f (Twist.altInsert s j₁ hjs) a

theorem

coeff_zero

L398 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Hj
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_zero {i : ℕ} (s : Idx n i)
    (a : Twist.MonExp n) :
    Twist.coeff R d (0 : Twist.cochain R n d i) s a = 0

theorem

dh_hd_coeff

L411 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.dh_hd_coeff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section DhHd
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.dh_hd_coeff (j₁ : Fin (n + 1)) (i : ℕ)
    (s : Idx n (i + 1)) (a : Twist.MonExp n)
    (hsub : Twist.negSupp n a ⊆ Idx.img n s)
    (haj : j₁ ∉ Twist.negSupp n a)
    (f : Twist.cochain R n d (i + 1)) :
    Twist.coeff R d
        (Twist.d R n d i (Twist.hj R d j₁ i f)) s a
      + Twist.coeff R d
          (Twist.hj R d j₁ (i + 1) (Twist.d R n d (i + 1) f)) s a
      = Twist.coeff R d f s a

def

coeffL

L571 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeffL

Documentation

The linear functional extracting one Laurent monomial coefficient from a Cech cochain.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homot
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · full declaration

def Twist.coeffL {i : ℕ} (s : Idx n i)
    (a : Twist.MonExp n) : Twist.cochain R n d i →ₗ[R] R where
  toFun f := Twist.coeff R d f s a
  map_add' f g := Twist.coeff_add R d f g s a
  map_smul' r f := Twist.coeff_smul R d r f s a

def

homot

L579 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.homot

Documentation

The monomialwise sum of coordinate contractions used to contract the twist Cech complex.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homot
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.homot (i : ℕ) :
    Twist.cochain R n d (i + 1) →ₗ[R] Twist.cochain R n d i

theorem

homot_basis

L590 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.homot_basis

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homot
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · full declaration

theorem Twist.homot_basis {i : ℕ} (s₀ : Idx n (i + 1))
    (b₀ : Twist.Mon n d (Idx.img n s₀)) (r : R) :
    Twist.homot R d i (Pi.single s₀ (Finsupp.single b₀ r))
      = if hb : Twist.negSupp n b₀.1 ≠ Finset.univ then
          Twist.hj R d (Twist.posMin b₀.1 hb) i
            (Pi.single s₀ (Finsupp.single b₀ r)) else 0 := by
  unfold Twist.homot
  rw [LinearMap.sum_apply,
    Finset.sum_eq_single s₀ (fun s' _ hne => by
      rw [LinearMap.comp_apply, LinearMap.proj_apply, Pi.single_eq_of_ne hne, map_zero])
      (fun h => absurd (Finset.mem_univ s₀) h)]
  simp only [LinearMap.comp_apply, LinearMap.proj_apply, Pi.single_eq_same, Finsupp.lsum_single]
  split_ifs with hb
  · simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, LinearMap.single_apply]
  · rfl

theorem

coeff_homot

L607 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_homot

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homot
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.coeff_homot {i : ℕ} (t : Idx n i)
    (a : Twist.MonExp n) (hsub : Twist.negSupp n a ⊆ Idx.img n t)
    (hne : Twist.negSupp n a ≠ Finset.univ)
    (f : Twist.cochain R n d (i + 1)) :
    Twist.coeff R d (Twist.homot R d i f) t a
      = Twist.coeff R d
          (Twist.hj R d (Twist.posMin a hne) i f) t a

theorem

subsingleton_cohomology_succ_of_le

L638 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.subsingleton_cohomology_succ_of_le

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Homot
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.subsingleton_cohomology_succ_of_le {i : ℕ} (hi : i + 2 ≤ n) :
    Subsingleton (Twist.H R n d (i + 1))

def

vtx

L676 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.vtx

Documentation

The Cech vertex indexed by the specified coordinate.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.vtx (j : Fin (n + 1)) : Idx n 0

theorem

img_vtx

L680 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_vtx

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_vtx (j : Fin (n + 1)) :
    Idx.img n (Twist.vtx j) = {j}

theorem

eq_vtx

L687 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.eq_vtx

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.eq_vtx (t : Idx n 0) :
    t = Twist.vtx (t.1 0)

instance

mon_empty_finite

L692 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.mon_empty_finite

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

instance Twist.mon_empty_finite :
    Finite (Twist.Mon n d ∅)

def

constSec

L717 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.constSec

Documentation

The constant Cech zero cochain associated to a monomial section with empty negative support.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.constSec :
    (Twist.Mon n d ∅ →₀ R) →ₗ[R] Twist.cochain R n d 0

theorem

coeff_constSec

L723 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.coeff_constSec

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · full declaration

theorem Twist.coeff_constSec (g : Twist.Mon n d ∅ →₀ R)
    (t : Idx n 0) (a : Twist.MonExp n) :
    Twist.coeff R d (Twist.constSec R d g) t a
      = if h : (∑ j, a j = d ∧ Twist.negSupp n a = ∅) then g ⟨a, h.1, h.2.le⟩
        else 0 := by
  rw [Twist.coeff, Twist.constSec, LinearMap.pi_apply, Finsupp.lmapDomain_apply]
  split_ifs with h1 h2 h3
  · have key : (⟨a, h1⟩ : Twist.Mon n d (Idx.img n t))
        = Twist.Mon.incl n d (Finset.empty_subset _) ⟨a, h2.1, h2.2.le⟩ := rfl
    erw [key, Finsupp.mapDomain_apply_of_injective (Twist.Mon.incl_injective n d _)]
  · erw [Finsupp.mapDomain_of_notMem_range]
    rintro ⟨b, hb⟩
    refine h2 ⟨h1.1, ?_⟩
    have : b.1 = a := congrArg Subtype.val hb
    exact this ▸ Finset.subset_empty.mp b.2.2
  · exact absurd ⟨h3.1, h3.2.le.trans (Finset.empty_subset _)⟩ h1
  · rfl

theorem

constSec_mem_ker

L742 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.constSec_mem_ker

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.constSec_mem_ker (g : Twist.Mon n d ∅ →₀ R) :
    Twist.constSec R d g ∈ LinearMap.ker (Twist.d R n d 0)

theorem

ker_edge

L751 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.ker_edge

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.ker_edge {f : Twist.cochain R n d 0}
    (hf : f ∈ LinearMap.ker (Twist.d R n d 0))
    (j k : Fin (n + 1)) (a : Twist.MonExp n) :
    Twist.coeff R d f (Twist.vtx j) a
      = Twist.coeff R d f (Twist.vtx k) a

theorem

H_zero_finite

L778 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.H_zero_finite

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HZero
variable {n : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.H_zero_finite (hn : 1 ≤ n) :
    Module.Finite R (Twist.H R n d 0)

def

sfull

L825 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.sfull

Documentation

The full increasing Cech index containing every projective coordinate.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

def Twist.sfull : Idx (m + 1) (m + 1)

theorem

img_sfull

L828 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.img_sfull

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.img_sfull :
    Idx.img (m + 1) (Twist.sfull (m := m)) = Finset.univ

theorem

eq_sfull

L833 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.eq_sfull

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.eq_sfull (s : Idx (m + 1) (m + 1)) :
    s = Twist.sfull

instance

mon_allNeg_finite

L840 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.mon_allNeg_finite

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

instance Twist.mon_allNeg_finite :
    Finite {b : Twist.Mon (m + 1) d
      (Idx.img (m + 1) (Twist.sfull (m := m))) //
      Twist.negSupp (m + 1) b.1 = Finset.univ}

theorem

basis_mem_range

L864 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.basis_mem_range

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.basis_mem_range
    (b : Twist.Mon (m + 1) d
      (Idx.img (m + 1) (Twist.sfull (m := m))))
    (hb : Twist.negSupp (m + 1) b.1 ≠ Finset.univ) (r : R) :
    Pi.single (Twist.sfull (m := m)) (Finsupp.single b r)
      ∈ LinearMap.range (Twist.d R (m + 1) d m)

theorem

H_top_finite

L894 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.H_top_finite

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section HN
variable {m : ℕ} (R : Type u) [CommRing R] (d : ℤ)
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.H_top_finite :
    Module.Finite R (Twist.H R (m + 1) d (m + 1))

instance

mon_zero_finite

L971 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.mon_zero_finite

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Headline
variable (R : Type u) [CommRing R]
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

instance Twist.mon_zero_finite (d : ℤ) (I : Finset (Fin 1)) :
    Finite (Twist.Mon 0 d I)

theorem

finite_of_subsingleton

L980 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.finite_of_subsingleton

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Headline
variable (R : Type u) [CommRing R]
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.finite_of_subsingleton (n : ℕ) (d : ℤ) (i : ℕ)
    (h : Subsingleton (Twist.H R n d i)) :
    Module.Finite R (Twist.H R n d i)

theorem

finite_cohomology

L986 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology.ProjSpaceCech.Twist.finite_cohomology

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section Headline
variable (R : Type u) [CommRing R]
open scoped _root_.ProjSpaceCech.Twist in

Lean source · statement

theorem Twist.finite_cohomology (n : ℕ) (d : ℤ) (i : ℕ) :
    Module.Finite R (Twist.H R n d i)

theorem

finite_cohomology

L1015 ↗

ProjSpaceCech.Twist.finite_cohomology

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_finite_cohomology
universe u
noncomputable section
open Finset Function
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in

Lean source · statement

theorem _root_.ProjSpaceCech.Twist.finite_cohomology (R : Type u) [CommRing R] (n : ℕ) (d : ℤ) (i
    : ℕ) :
    Module.Finite R (ProjSpaceCech.Twist.H R n d i)

Module documentation

Declarations