NYLL
Module

ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
39 declarations indexed from sourceView source ↗

Module documentation

Vanishing of positive Čech cohomology of projective twists in the stated degree range.

Imports5
Imported by2

Declarations

theorem

idx_canonical

L46 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.idx_canonical
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L51 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.idx_eq_of_img
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.img_face
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L75 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altOfFinset
Documentation

The increasing Cech index with a prescribed finite image.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L80 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.img_altOfFinset
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altPos
Documentation

The position of a coordinate in an increasing Cech index.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L93 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.idx_val_altPos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L100 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altPos_val
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L106 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altInsert
Documentation

Insert a new coordinate into an increasing Cech index.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L112 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.img_altInsert
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L120 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.insPos
Documentation

The position of the newly inserted coordinate.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L126 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altInsert_val_insPos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L132 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.face_altInsert_insPos
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L141 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.img_face_altInsert_ne
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L168 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff
Documentation

Extract a monomial coefficient, extending it by zero outside the chart.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L174 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_eq
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L181 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_of_not
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L188 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_add
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L198 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_smul
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L207 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.ext_coeff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L215 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_d
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L251 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_piSingle
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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
  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
        rw [Pi.single_eq_same]
        apply Finsupp.single_eq_of_ne' (α := Twist.Mon n d (Idx.img n s))
        intro heq
        exact hsa ⟨rfl, (Subtype.ext_iff.mp heq : b₀.1 = a).symm⟩
      · rw [Pi.single_eq_of_ne hs]
        exact Finsupp.zero_apply (a := (⟨a, hok⟩ : Twist.Mon n d (Idx.img n s)))
    · rfl
def

posMin

L273 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.posMin
Documentation

The smallest coordinate outside the negative support of a monomial.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L280 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.posMin_notMem_negSupp
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L296 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.altPos_eq_card
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L310 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.insPos_eq_card
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L323 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.img_subset_altInsert
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L330 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.hj
Documentation

The signed contraction obtained by inserting a fixed coordinate.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L342 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.hj_apply_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L350 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_hj_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L360 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_hj
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L381 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L396 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.dh_hd_coeff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L556 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeffL
Documentation

Monomial coefficient extraction as a linear map.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L564 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.homot
Documentation

The monomialwise contraction using the smallest coordinate outside negative support.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L575 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.homot_basis
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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

L592 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.coeff_homot
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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'

L623 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le.ProjSpaceCech.Twist.subsingleton_cohomology_succ_of_le'
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
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))
theorem

subsingleton_cohomology_succ_of_le

L657 ↗
ProjSpaceCech.Twist.subsingleton_cohomology_succ_of_le
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace ProjSpaceCech_Twist_subsingleton_cohomology_succ_of_le
universe u
noncomputable section
open Finset Function
Lean source · statement
theorem _root_.ProjSpaceCech.Twist.subsingleton_cohomology_succ_of_le (R : Type u) [CommRing R]
  (n : ℕ) (d : ℤ) {i : ℕ}
    (hi : i + 2 ≤ n) : Subsingleton (ProjSpaceCech.Twist.H R n d (i + 1))

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