Module

OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le

8 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf subsingleton HSucc and euler Char eq sum range of card le

Imports1

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheafEulerChar

Imported by2

theorem

isEmpty_idx

L33 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.isEmpty_idx

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem isEmpty_idx {i : ℕ} (h : Fintype.card K.ι ≤ i) : IsEmpty (K.Idx i)

theorem

subsingleton_cochain

L39 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.subsingleton_cochain

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem subsingleton_cochain {i : ℕ} (h : Fintype.card K.ι ≤ i) : Subsingleton (F.cochain K i)

theorem

subsingleton_H0

L43 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.subsingleton_H0

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem subsingleton_H0 (h : Fintype.card K.ι = 0) : Subsingleton (F.H0 K)

theorem

subsingleton_HSucc

L47 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.subsingleton_HSucc

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem subsingleton_HSucc {i : ℕ} (h : Fintype.card K.ι ≤ i + 1) : Subsingleton (F.HSucc K i)

theorem

cechFinrank_eq_zero

L51 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.cechFinrank_eq_zero

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem cechFinrank_eq_zero [Nontrivial R] {i : ℕ} (h : Fintype.card K.ι ≤ i) : F.cechFinrank K i =
  0

theorem

eulerChar_eq_sum_range

L61 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.eulerChar_eq_sum_range

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem eulerChar_eq_sum_range [Nontrivial R] {N : ℕ} (h : Fintype.card K.ι ≤ N) :
    F.eulerChar K = ∑ i ∈ Finset.range N, (-1 : ℤ) ^ i * (F.cechFinrank K i : ℤ)

theorem

main

L68 ↗

AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le.P2mVan.main

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mVan
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
variable (F : OModulePresheaf π) (K : V.OrderedAffineCover)

Lean source · statement

theorem main :
    (∀ i : ℕ, Fintype.card K.ι ≤ i → IsEmpty (K.Idx i)) ∧
    (∀ i : ℕ, Fintype.card K.ι ≤ i → Subsingleton (F.cochain K i)) ∧
    (∀ i : ℕ, Fintype.card K.ι ≤ i + 1 → Subsingleton (F.HSucc K i)) ∧
    (Nontrivial R →
      (∀ i : ℕ, Fintype.card K.ι ≤ i → F.cechFinrank K i = 0) ∧
      (∀ N : ℕ, Fintype.card K.ι ≤ N →
        F.eulerChar K = ∑ i ∈ Finset.range N, (-1 : ℤ) ^ i * (F.cechFinrank K i : ℤ)))

theorem

subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le

L82 ↗

AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
universe u
open CategoryTheory AlgebraicGeometry

Lean source · statement

theorem
  _root_.AlgebraicGeometry.OModulePresheaf.subsingleton_HSucc_and_eulerChar_eq_sum_range_of_card_le
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)}
    (F : OModulePresheaf π) (K : V.OrderedAffineCover) :
    (∀ i : ℕ, Fintype.card K.ι ≤ i → IsEmpty (K.Idx i)) ∧
    (∀ i : ℕ, Fintype.card K.ι ≤ i → Subsingleton (F.cochain K i)) ∧
    (∀ i : ℕ, Fintype.card K.ι ≤ i + 1 → Subsingleton (F.HSucc K i)) ∧
    (Nontrivial R →
      (∀ i : ℕ, Fintype.card K.ι ≤ i → F.cechFinrank K i = 0) ∧
      (∀ N : ℕ, Fintype.card K.ι ≤ N →
        F.eulerChar K = ∑ i ∈ Finset.range N, (-1 : ℤ) ^ i * (F.cechFinrank K i : ℤ)))

Module documentation

OModule Presheaf subsingleton HSucc and euler Char eq sum range of card le

Declarations