Module

ProjSpaceCech_Twist_subsingleton_cohomology_of_lt.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_Twist_subsingleton_cohomology_of_lt

2 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Twist subsingleton cohomology of lt

Imports1

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCechTwist

Imported by2

theorem

subsingleton_cohomology_of_lt

L42 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjectiveTwistSubsingleton.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.ProjectiveTwistSubsingleton
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

subsingleton_cohomology_of_lt

L56 ↗

ProjSpaceCech.Twist.subsingleton_cohomology_of_lt

Source context 6 commands

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

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

Lean source · statement

theorem _root_.ProjSpaceCech.Twist.subsingleton_cohomology_of_lt (R : Type u) [CommRing R] (n :
  ℕ) (d : ℤ) {i : ℕ}
    (hi : n < i) : Subsingleton (ProjSpaceCech.Twist.H R n d i)

Module documentation

Proj Space Cech Twist subsingleton cohomology of lt

Declarations

subsingleton_cohomology_of_lt

subsingleton_cohomology_of_lt