NYLL
Module

OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
12 declarations indexed from sourceView source ↗

Module documentation

Identification of relative cohomology sections on an affine open with fibre-cover Cech cohomology.

Imports2
Imported by2

Declarations

theorem

res_res

L54 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.res_res
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
Lean source · statement
theorem res_res {O₁ O₂ O₃ : V'.Opens} (h₂₁ : O₂ ≤ O₁) (h₃₂ : O₃ ≤ O₂) (x : Γ(V', O₁)) :
    (V'.presheaf.map (homOfLE h₃₂).op).hom ((V'.presheaf.map (homOfLE h₂₁).op).hom x)
      = (V'.presheaf.map (homOfLE (h₃₂.trans h₂₁)).op).hom x
theorem

res_self

L60 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.res_self
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
Lean source · statement
theorem res_self {O : V'.Opens} (h : O ≤ O) (x : Γ(V', O)) :
    (V'.presheaf.map (homOfLE h).op).hom x = x
def

cochainEquiv

L69 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.cochainEquiv
Documentation

The section equivalence identifying relative cochains with the induced preimage cover.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
def cochainEquiv (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltC p πZ K' U b ≃ₗ[R] (restrictToPreimage p πZ K' hU).cochain b :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  { toFun := fun f τ => (V'.presheaf.map
      (homOfLE (inter_restrictToPreimage p πZ K' hU τ).le).op).hom (f τ)
    invFun := fun g τ => (V'.presheaf.map
      (homOfLE (inter_restrictToPreimage p πZ K' hU τ).ge).op).hom (g τ)
    left_inv := fun f => funext fun τ => by
      change (V'.presheaf.map _).hom ((V'.presheaf.map _).hom (f τ)) = f τ
      erw [res_res, res_self]
    right_inv := fun g => funext fun τ => by
      change (V'.presheaf.map _).hom ((V'.presheaf.map _).hom (g τ)) = g τ
      erw [res_res, res_self]
    map_add' := fun _ _ => funext fun τ => map_add _ _ _
    map_smul' := fun r f => funext fun τ =>
      (Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
        (inter_restrictToPreimage p πZ K' hU τ).le).map_smul r (f τ) }
theorem

cochainEquiv_apply

L88 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.cochainEquiv_apply
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · statement
theorem cochainEquiv_apply (b : ℕ) (f : relAltC p πZ K' U b) (τ : (restrictToPreimage p πZ K'
    hU).Idx b) :
    cochainEquiv p πZ K' hU b f τ
      = (V'.presheaf.map (homOfLE (inter_restrictToPreimage p πZ K' hU τ).le).op).hom (f τ)
theorem

cochainEquiv_relAltd

L94 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.cochainEquiv_relAltd
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
theorem cochainEquiv_relAltd (b : ℕ) (f : relAltC p πZ K' U b) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    cochainEquiv p πZ K' hU (b + 1) (relAltd p πZ K' U b f)
      = (restrictToPreimage p πZ K' hU).d (p ≫ πZ) b (cochainEquiv p πZ K' hU b f) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  funext τ
  erw [cochainEquiv_apply, relAltd_apply', Scheme.OrderedAffineCoverOf.d_apply, map_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  erw [map_zsmul, cochainEquiv_apply, res_res, res_res]
  rfl
def

kerEquiv

L106 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.kerEquiv
Documentation

The induced equivalence of relative and preimage-cover Čech cocycles.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
def kerEquiv (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    LinearMap.ker (relAltd p πZ K' U b)
      ≃ₗ[R] LinearMap.ker ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) b) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearEquiv.ofLinearMap
    ((cochainEquiv p πZ K' hU b).toLinearMap.restrict fun x hx =>
      LinearMap.mem_ker.mpr
        (((cochainEquiv_relAltd p πZ K' hU b x).symm.trans
          (congrArg (cochainEquiv p πZ K' hU (b + 1)) (LinearMap.mem_ker.mp hx))).trans
          (map_zero _)))
    ((cochainEquiv p πZ K' hU b).symm.toLinearMap.restrict fun y hy =>
      LinearMap.mem_ker.mpr ((cochainEquiv p πZ K' hU (b + 1)).injective
        ((cochainEquiv_relAltd p πZ K' hU b _).trans
          (((congrArg ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) b)
              ((cochainEquiv p πZ K' hU b).apply_symm_apply y)).trans
            (LinearMap.mem_ker.mp hy)).trans (map_zero _).symm))))
    (LinearMap.ext fun y => Subtype.ext
      ((cochainEquiv p πZ K' hU b).apply_symm_apply y.1))
    (LinearMap.ext fun x => Subtype.ext
      ((cochainEquiv p πZ K' hU b).symm_apply_apply x.1))
theorem

kerEquiv_apply_coe

L128 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.kerEquiv_apply_coe
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
theorem kerEquiv_apply_coe (b : ℕ)
    (x : letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ); ↥(LinearMap.ker (relAltd p
      πZ K' U b))) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    ((kerEquiv p πZ K' hU b x : LinearMap.ker ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) b))
        : (restrictToPreimage p πZ K' hU).cochain b)
      = cochainEquiv p πZ K' hU b x.1 :=
  rfl
theorem

kerEquiv_symm_apply_coe

L137 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.kerEquiv_symm_apply_coe
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
theorem kerEquiv_symm_apply_coe (b : ℕ)
    (y : letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
      ↥(LinearMap.ker ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) b))) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (((kerEquiv p πZ K' hU b).symm y : LinearMap.ker (relAltd p πZ K' U b)) : relAltC p πZ K' U b)
      = (cochainEquiv p πZ K' hU b).symm y.1 :=
  rfl
def

H0Equiv

L146 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.H0Equiv
Documentation

The equivalence from degree-zero relative cohomology to preimage-cover Čech cohomology.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · statement
def H0Equiv :
    (relHPresheaf p πZ K' 0).obj U ≃ₗ[R] (restrictToPreimage p πZ K' hU).H0 (p ≫ πZ)
theorem

relAltHB_map_kerEquiv

L151 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.relAltHB_map_kerEquiv
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · full declaration
theorem relAltHB_map_kerEquiv (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (relAltHB p πZ K' U (b + 1)).map (kerEquiv p πZ K' hU (b + 1)).toLinearMap
      = (LinearMap.range ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) b)).comap
          (LinearMap.ker ((restrictToPreimage p πZ K' hU).d (p ≫ πZ) (b + 1))).subtype := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine le_antisymm (Submodule.map_le_iff_le_comap.mpr ?_) ?_
  · rintro x ⟨y, hy⟩
    exact ⟨cochainEquiv p πZ K' hU b y,
      (cochainEquiv_relAltd p πZ K' hU b y).symm.trans (congrArg (cochainEquiv p πZ K' hU (b + 1))
        hy)⟩
  · rintro y ⟨g, hg⟩
    refine ⟨(kerEquiv p πZ K' hU (b + 1)).symm y, ⟨(cochainEquiv p πZ K' hU b).symm g, ?_⟩,
      (kerEquiv p πZ K' hU (b + 1)).apply_symm_apply y⟩
    change _ = (cochainEquiv p πZ K' hU (b + 1)).symm y.1
    apply (cochainEquiv p πZ K' hU (b + 1)).injective
    rw [cochainEquiv_relAltd, LinearEquiv.apply_symm_apply, LinearEquiv.apply_symm_apply]
    exact hg
def

HSuccEquiv

L171 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen.AlgebraicGeometry.OModulePresheaf.Leray.CoverMatch.HSuccEquiv
Documentation

The equivalence from successive relative cohomology to preimage-cover Čech cohomology.

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
noncomputable section
section
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf
namespace Leray
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
namespace CoverMatch
open _root_.AlgebraicGeometry.OModulePresheaf.Leray
open _root_.AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {V' Z : Scheme.{u}}
variable (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
variable (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U)
Lean source · statement
def HSuccEquiv (b : ℕ) :
    (relHPresheaf p πZ K' (b + 1)).obj U ≃ₗ[R] (restrictToPreimage p πZ K' hU).HSucc (p ≫ πZ) b
theorem

nonempty_relHPresheaf_obj_equiv_of_isAffineOpen

L192 ↗
AlgebraicGeometry.OModulePresheaf.Leray.nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs
namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
with_weak_namespace AlgebraicGeometry.OModulePresheaf
open _root_.AlgebraicGeometry.OModulePresheaf.Leray Leray in
with_weak_namespace _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs
with_weak_namespace OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
open _root_.AlgebraicCurves.Cohomology.Sheaves.Proofs in
open OModulePresheaf_Leray_nonempty_relHPresheaf_obj_equiv_of_isAffineOpen in
with_weak_namespace _root_.AlgebraicGeometry.OModulePresheaf.Leray
Lean source · statement
theorem nonempty_relHPresheaf_obj_equiv_of_isAffineOpen
    {R : Type u} [CommRing R] {V' Z : Scheme.{u}} (p : V' ⟶ Z) (πZ : Z ⟶ Spec (.of R))
      [IsSeparated πZ]
    (K' : V'.OrderedAffineCover) {U : Z.Opens} (hU : IsAffineOpen U) :
    Nonempty ((OModulePresheaf.Leray.relHPresheaf p πZ K' 0).obj U
        ≃ₗ[R] (OModulePresheaf.Leray.restrictToPreimage p πZ K' hU).H0 (p ≫ πZ)) ∧
      ∀ b : ℕ, Nonempty ((OModulePresheaf.Leray.relHPresheaf p πZ K' (b + 1)).obj U
        ≃ₗ[R] (OModulePresheaf.Leray.restrictToPreimage p πZ K' hU).HSucc (p ≫ πZ) b)

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