Module

ProjSpaceCech_GradedModule_d_sq.lean

Nyll.SchemeTheory.Cohomology.Cech.ProjSpaceCech_GradedModule_d_sq

3 declarations indexed from sourceView source ↗

Module documentation

The square of the graded-module Cech differential is zero.

Imports2

Imported by4

theorem

d_sq'

L43 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_d_sq.ProjSpaceCech.GradedModule.d_sq'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_d_sq
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section GradAltdSq
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in

Lean source · statement

theorem GradedModule.d_sq' (i : ℕ) :
    GradedModule.d D (i + 1) ∘ₗ GradedModule.d D i = 0

theorem

range_d_le_ker

L114 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_d_sq.ProjSpaceCech.GradedModule.range_d_le_ker

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_d_sq
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section GradAltdSq
variable {R : Type u} [CommRing R] {n : ℕ}
variable (D : GradedModule R n)
open scoped _root_.ProjSpaceCech.GradedModule in

Lean source · statement

theorem GradedModule.range_d_le_ker (i : ℕ) :
    LinearMap.range (GradedModule.d D i)
      ≤ LinearMap.ker (GradedModule.d D (i + 1))

theorem

d_sq

L124 ↗

ProjSpaceCech.GradedModule.d_sq

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.ProjSpaceCech_GradedModule_d_sq
universe u
noncomputable section
open Finset Function MvPolynomial

Lean source · statement

theorem _root_.ProjSpaceCech.GradedModule.d_sq {R : Type u} [CommRing R] {n : ℕ} (D :
    ProjSpaceCech.GradedModule R n) (i : ℕ) :
    ProjSpaceCech.GradedModule.d D (i + 1) ∘ₗ ProjSpaceCech.GradedModule.d D i = 0

Module documentation

Declarations

d_sq'

range_d_le_ker

d_sq