NYLL
Module

ProjSpaceCech_GradedModule_Presentation_subsingleton_H_of_ses.lean

Nyll.AlgebraicCurves.Cohomology.Cech.ProjSpaceCech_GradedModule_Presentation_subsingleton_H_of_ses
9 declarations indexed from sourceView source ↗

Module documentation

Proj Space Cech Graded Module Presentation subsingleton H of ses

Imports3
Imported by2

Declarations

theorem

piC_surjective

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.piC_surjective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.piC_surjective (i : ℕ) : Function.Surjective (πC i)
theorem

iotaC_injective

L57 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.iotaC_injective
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.iotaC_injective (i : ℕ) : Function.Injective (ιC i)
theorem

altC_exact

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.altC_exact
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.altC_exact (i : ℕ) :
    LinearMap.ker (πC i) = LinearMap.range (ιC i)
theorem

snake_data

L111 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.snake_data
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.snake_data (i : ℕ)
    (z : ↥(LinearMap.ker (GradedModule.d D i))) :
    ∃ (k₀ : ↥(LinearMap.ker (GradedModule.d σ.ker (i + 1))))
      (f₀ : GradedModule.cochain σ.F i),
        πC i f₀ = z.1 ∧ ιC (i + 1) k₀.1 = GradedModule.d σ.F i f₀ ∧
        ∀ f, πC i f = z.1 → ∃ h, ιC (i + 1) k₀.1
          = GradedModule.d σ.F i f + ιC (i + 1) (GradedModule.d σ.ker i h)
def

delta0

L142 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.delta0
Documentation

The connecting class constructed from a lifted graded Čech cocycle.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
def GradedModule.delta0 (i : ℕ) :
    ↥(LinearMap.ker (GradedModule.d D i)) →ₗ[R] GradedModule.H σ.ker (i + 1)
theorem

ker_delta0_le

L160 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.ker_delta0_le
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.ker_delta0_le (i : ℕ) :
    LinearMap.ker (GradedModule.delta0 σ i)
      ≤ LinearMap.range (GradedModule.Hom.cochainMapKer σ.hom i)
theorem

delta0_vanish_on_bdry

L181 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.delta0_vanish_on_bdry
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule in
Lean source · statement
theorem GradedModule.delta0_vanish_on_bdry (j : ℕ)
    (z : ↥(LinearMap.ker (GradedModule.d D (j + 1))))
    (hz : z.1 ∈ LinearMap.range (GradedModule.d D j)) :
    GradedModule.delta0 σ (j + 1) z = 0
theorem

subsingleton_H_of_ses'

L207 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES.ProjSpaceCech.GradedModule.Presentation.subsingleton_H_of_ses'
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
namespace ProjSpaceCech
open _root_.ProjSpaceCech
open _root_.ProjSpaceCech
section SES
variable {R : Type u} [CommRing R] {n : ℕ} {D : GradedModule R n}
variable (σ : GradedModule.Presentation D)
local notation "ιC" => GradedModule.Hom.cochainMap (GradedModule.Presentation.kerIncl σ)
local notation "πC" => GradedModule.Hom.cochainMap σ.hom
open scoped _root_.ProjSpaceCech.GradedModule _root_.ProjSpaceCech.GradedModule.Presentation in
Lean source · statement
theorem GradedModule.Presentation.subsingleton_H_of_ses' (i : ℕ)
    (hF : Subsingleton (GradedModule.H σ.F i))
    (hK : Subsingleton (GradedModule.H σ.ker (i + 1))) :
    Subsingleton (GradedModule.H D i)
theorem

subsingleton_H_of_ses

L241 ↗
ProjSpaceCech.GradedModule.Presentation.subsingleton_H_of_ses
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GradedPresentationSES
universe u
noncomputable section
open Finset Function MvPolynomial
Lean source · statement
theorem _root_.ProjSpaceCech.GradedModule.Presentation.subsingleton_H_of_ses {R : Type u}
  [CommRing R] {n : ℕ} {D : ProjSpaceCech.GradedModule R n}
    (σ : ProjSpaceCech.GradedModule.Presentation D) (i : ℕ)
    (hF : Subsingleton (ProjSpaceCech.GradedModule.H σ.F i)) (hK : Subsingleton
      (ProjSpaceCech.GradedModule.H σ.ker (i + 1))) :
    Subsingleton (ProjSpaceCech.GradedModule.H D i)

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