NYLL
Module

OModulePresheaf_eulerChar_eq_add_of_affSES.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_eulerChar_eq_add_of_affSES
21 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf euler Char eq add of aff SES

Imports10
Imported by8

Declarations

def

cx

L43 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cx
Documentation

The cochain complex whose differential is the ordered cover Cech differential.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
Lean source · statement
def cx (F : OModulePresheaf π) (K : V.OrderedAffineCover) : CochainComplex
  (ModuleCat.{u} k) ℕ
theorem

cx_d_hom

L50 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cx_d_hom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
Lean source · statement
theorem cx_d_hom (F : OModulePresheaf π) (K : V.OrderedAffineCover) (i : ℕ) :
    ((cx F K).d i (i + 1)).hom = F.d K i
theorem

cx_d_zero_zero_hom

L55 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cx_d_zero_zero_hom
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
Lean source · statement
theorem cx_d_zero_zero_hom (F : OModulePresheaf π) (K : V.OrderedAffineCover) :
    ((cx F K).d 0 0).hom = 0
def

cxMap

L64 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cxMap
Documentation

The cochain complex morphism induced by an affine morphism of module presheaves.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
Lean source · statement
def cxMap {F G : OModulePresheaf π} (φ : AffHom F G) (K : V.OrderedAffineCover) :
    cx F K ⟶ cx G K
theorem

cxMap_f_hom

L70 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cxMap_f_hom
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
Lean source · statement
theorem cxMap_f_hom {F G : OModulePresheaf π} (φ : AffHom F G) (K : V.OrderedAffineCover) (i : ℕ) :
    ((cxMap φ K).f i).hom = φ.cochainMap K i
theorem

proj_inc_apply

L76 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.proj_inc_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
omit [IsSeparated π] in
Lean source · statement
theorem proj_inc_apply (U : V.affineOpens) (x : F₁.obj U.1) : S.proj.app U (S.inc.app U x) = 0
theorem

cochainMap_injective

L79 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cochainMap_injective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
theorem cochainMap_injective (i : ℕ) : Function.Injective (S.inc.cochainMap K i)
theorem

cochainMap_surjective

L82 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cochainMap_surjective
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
theorem cochainMap_surjective (i : ℕ) : Function.Surjective (S.proj.cochainMap K i)
theorem

cochainMap_exact

L86 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.cochainMap_exact
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
theorem cochainMap_exact (i : ℕ) : Function.Exact (S.inc.cochainMap K i) (S.proj.cochainMap K i)
def

T

L99 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.T
Documentation

The short complex of Cech cochain complexes induced by the affine short exact sequence.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
def T : ShortComplex (CochainComplex (ModuleCat.{u} k) ℕ)
theorem

T_shortExact

L108 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.T_shortExact
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
theorem T_shortExact : (T S K).ShortExact
theorem

quotEquiv_aux

L118 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.quotEquiv_aux
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
Lean source · statement
theorem quotEquiv_aux {M N P : Type u} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N]
    [AddCommGroup P] [Module k P] (f f' : M →ₗ[k] N) (g g' : N →ₗ[k] P) (hf : f' = f) (hg : g' = g)
    (h' : ∀ x, g' (f' x) = 0) :
    Nonempty ((LinearMap.ker g' ⧸ LinearMap.range (f'.codRestrict (LinearMap.ker g') h')) ≃ₗ[k]
      (LinearMap.ker g ⧸ (LinearMap.range f).comap (LinearMap.ker g).subtype))
theorem

quotEquiv_aux₀

L126 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.quotEquiv_aux₀
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
Lean source · statement
theorem quotEquiv_aux₀ {M N P : Type u} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N]
    [AddCommGroup P] [Module k P] (f' : M →ₗ[k] N) (g g' : N →ₗ[k] P) (hf : f' = 0) (hg : g' = g)
    (h' : ∀ x, g' (f' x) = 0) :
    Nonempty ((LinearMap.ker g' ⧸ LinearMap.range (f'.codRestrict (LinearMap.ker g') h')) ≃ₗ[k]
      LinearMap.ker g)
theorem

nonempty_equiv_HSucc

L139 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.nonempty_equiv_HSucc
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
variable (F : OModulePresheaf π)
Lean source · statement
theorem nonempty_equiv_HSucc (i : ℕ) : Nonempty (((cx F K).homology (i + 1)) ≃ₗ[k] F.HSucc K i)
theorem

nonempty_equiv_H0

L149 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.nonempty_equiv_H0
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
variable (F : OModulePresheaf π)
Lean source · statement
theorem nonempty_equiv_H0 : Nonempty (((cx F K).homology 0) ≃ₗ[k] F.H0 K)
theorem

finrank_homology_eq

L158 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.finrank_homology_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
variable (F : OModulePresheaf π)
Lean source · statement
theorem finrank_homology_eq (i : ℕ) : Module.finrank k ((cx F K).homology i) = F.cechFinrank K i
theorem

finite_homology

L164 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.finite_homology
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
variable (F : OModulePresheaf π)
Lean source · statement
theorem finite_homology (h : F.CechFinite K) (i : ℕ) : Module.Finite k ((cx F K).homology i)
theorem

subsingleton_homology_card_succ

L170 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.subsingleton_homology_card_succ
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
section Ident
omit [IsSeparated π]
variable (F : OModulePresheaf π)
Lean source · statement
theorem subsingleton_homology_card_succ :
    Subsingleton ((cx F K).homology (Fintype.card K.ι + 1))
theorem

injective_homologyMap_zero

L179 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.injective_homologyMap_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
Lean source · statement
theorem injective_homologyMap_zero : Function.Injective (HomologicalComplex.homologyMap (T S K).f
  0)
theorem

main

L187 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES.P2mEulerAdd.main
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mEulerAdd
open AlgebraicGeometry.OModulePresheaf
variable {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)}
variable [IsSeparated π]
variable {F₁ F₂ F₃ : OModulePresheaf π} (S : AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
include S in
Lean source · statement
theorem main (h₁ : F₁.CechFinite K) (h₂ : F₂.CechFinite K) (h₃ : F₃.CechFinite K) :
    F₂.eulerChar K = F₁.eulerChar K + F₃.eulerChar K
theorem

eulerChar_eq_add_of_affSES

L226 ↗
AlgebraicGeometry.OModulePresheaf.eulerChar_eq_add_of_affSES
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_eulerChar_eq_add_of_affSES
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.eulerChar_eq_add_of_affSES
    {k : Type u} [Field k] {V : Scheme.{u}} {π : V ⟶ Spec (.of k)} [IsSeparated π]
    {F₁ F₂ F₃ : OModulePresheaf π} (S : OModulePresheaf.AffSES F₁ F₂ F₃) (K : V.OrderedAffineCover)
    (h₁ : F₁.CechFinite K) (h₂ : F₂.CechFinite K) (h₃ : F₃.CechFinite K) :
    F₂.eulerChar K = F₁.eulerChar K + F₃.eulerChar K

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