NYLL
Module

OModulePresheaf_cechFinite_iff_of_cochain_equiv.lean

Nyll.SchemeTheory.Cohomology.Cech.OModulePresheaf_cechFinite_iff_of_cochain_equiv
8 declarations indexed from sourceView source ↗

Module documentation

Finiteness of Cech cohomology is invariant under a cochain equivalence commuting with differentials.

Imports2
Imported by2

Declarations

theorem

d_comp_equiv

L50 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.d_comp_equiv
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
include he in
Lean source · statement
theorem d_comp_equiv (q : ℕ) :
    G.d K' q ∘ₗ (e q : F.cochain K q →ₗ[R] G.cochain K' q) = (e (q + 1) : _ →ₗ[R] _) ∘ₗ F.d K q
theorem

map_ker_d

L55 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.map_ker_d
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
include he in
Lean source · statement
theorem map_ker_d (q : ℕ) :
    Submodule.map (e q : F.cochain K q →ₗ[R] G.cochain K' q) (LinearMap.ker (F.d K q)) =
      LinearMap.ker (G.d K' q)
def

kerEquiv

L67 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.kerEquiv
Documentation

The induced equivalence of cocycles from a cochain equivalence commuting with the differentials.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
Lean source · statement
def kerEquiv (q : ℕ) : LinearMap.ker (F.d K q) ≃ₗ[R] LinearMap.ker (G.d K' q)
theorem

kerEquiv_apply_coe

L70 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.kerEquiv_apply_coe
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
Lean source · statement
theorem kerEquiv_apply_coe (q : ℕ) (x : LinearMap.ker (F.d K q)) :
    (kerEquiv F G K K' e he q x).1 = e q x.1
theorem

map_comap_range

L74 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.map_comap_range
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
include he in
Lean source · statement
theorem map_comap_range (q : ℕ) :
    Submodule.map (kerEquiv F G K K' e he (q + 1) : _ →ₗ[R] _)
        ((LinearMap.range (F.d K q)).comap (LinearMap.ker (F.d K (q + 1))).subtype)
      = (LinearMap.range (G.d K' q)).comap (LinearMap.ker (G.d K' (q + 1))).subtype
def

hSuccEquiv

L94 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.hSuccEquiv
Documentation

The induced equivalence on positive Cech cohomology, obtained by quotienting the cocycle equivalence.

Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
Lean source · statement
def hSuccEquiv (q : ℕ) : F.HSucc K q ≃ₗ[R] G.HSucc K' q
theorem

cechFinite_iff_of_cochainEquiv

L98 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv.AlgebraicGeometry.OModulePresheaf.cechFinite_iff_of_cochainEquiv
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
section CochainEquiv
variable {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of
  R)}
variable (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
  V'.OrderedAffineCover)
variable (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q)
variable (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e q x))
include he in
Lean source · statement
theorem cechFinite_iff_of_cochainEquiv : F.CechFinite K ↔ G.CechFinite K'
theorem

cechFinite_iff_of_cochain_equiv

L112 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_iff_of_cochain_equiv
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_iff_of_cochain_equiv
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_iff_of_cochain_equiv
    {R : Type u} [CommRing R] {V V' : Scheme.{u}} {π : V ⟶ Spec (.of R)} {π' : V' ⟶ Spec (.of R)}
    (F : OModulePresheaf π) (G : OModulePresheaf π') (K : V.OrderedAffineCover) (K' :
      V'.OrderedAffineCover)
    (e : ∀ q, F.cochain K q ≃ₗ[R] G.cochain K' q) (he : ∀ q x, e (q + 1) (F.d K q x) = G.d K' q (e
      q x)) :
    F.CechFinite K ↔ G.CechFinite K'

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