NYLL
Module

OModulePresheaf_cechFinite_pushforward_iff.lean

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

Module documentation

Cech finiteness for a pushforward is equivalent to finiteness on the preimage cover.

Imports4
Imported by3

Declarations

def

resEq

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.resEq
Documentation

The section equivalence induced by equality of two opens, expressed using restrictions.

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Transport
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {ρ : Z ⟶ Spec (.of R)} (H : OModulePresheaf ρ)
Lean source · full declaration
def resEq {U U' : Z.Opens} (h : U = U') : H.obj U ≃ₗ[R] H.obj U' where
  toFun := H.res h.ge
  invFun := H.res h.le
  map_add' := map_add _
  map_smul' := map_smul _
  left_inv x := by
    change (H.res h.le ∘ₗ H.res h.ge) x = x
    rw [← H.res_comp]; exact LinearMap.congr_fun (H.res_refl U) x
  right_inv x := by
    change (H.res h.ge ∘ₗ H.res h.le) x = x
    rw [← H.res_comp]; exact LinearMap.congr_fun (H.res_refl U') x
theorem

resEq_apply

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.resEq_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Transport
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {ρ : Z ⟶ Spec (.of R)} (H : OModulePresheaf ρ)
Lean source · statement
theorem resEq_apply {U U' : Z.Opens} (h : U = U') (x : H.obj U) : resEq H h x = H.res h.ge x
theorem

res_res_apply

L61 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.res_res_apply
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Transport
variable {R : Type u} [CommRing R] {Z : Scheme.{u}} {ρ : Z ⟶ Spec (.of R)} (H : OModulePresheaf ρ)
Lean source · statement
theorem res_res_apply {U₁ U₂ U₃ : Z.Opens} (h₁ : U₂ ≤ U₁) (h₂ : U₃ ≤ U₂) (x : H.obj U₁) :
    H.res h₂ (H.res h₁ x) = H.res (h₂.trans h₁) x
theorem

map_iInf_fin'

L73 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.map_iInf_fin'
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Pushforward
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} {π : V ⟶ Spec (.of R)} (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (H : OModulePresheaf (i ≫ π)) (K : V.OrderedAffineCover)
Lean source · statement
theorem map_iInf_fin' {X Y : Scheme.{u}} (f : X ⟶ Y) {n : ℕ} (U : Fin (n + 1) → Y.Opens) :
    (Opens.map f.base).obj (⨅ j, U j) = ⨅ j, (Opens.map f.base).obj (U j)
theorem

inter_preimage

L89 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.inter_preimage
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Pushforward
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} {π : V ⟶ Spec (.of R)} (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (H : OModulePresheaf (i ≫ π)) (K : V.OrderedAffineCover)
Lean source · full declaration
theorem inter_preimage {q : ℕ} (s : (K.preimage i).Idx q) :
    (K.preimage i).inter s = i ⁻¹ᵁ K.inter (show K.Idx q from s) :=
  (map_iInf_fin' i _).symm
def

pushforwardCochainEquiv

L97 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.pushforwardCochainEquiv
Documentation

The cochain equivalence between a module presheaf on the preimage cover and its pushforward on the original cover.

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Pushforward
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} {π : V ⟶ Spec (.of R)} (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (H : OModulePresheaf (i ≫ π)) (K : V.OrderedAffineCover)
Lean source · statement
def pushforwardCochainEquiv (q : ℕ) : H.cochain (K.preimage i) q ≃ₗ[R] (pushforward π i H).cochain
    K q
theorem

pushforwardCochainEquiv_d

L113 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff.AlgebraicGeometry.OModulePresheaf.pushforwardCochainEquiv_d
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
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 Pushforward
variable {R : Type u} [CommRing R] {V Z : Scheme.{u}} {π : V ⟶ Spec (.of R)} (i : Z ⟶ V)
  [IsClosedImmersion i]
variable (H : OModulePresheaf (i ≫ π)) (K : V.OrderedAffineCover)
Lean source · statement
theorem pushforwardCochainEquiv_d (q : ℕ) (x : H.cochain (K.preimage i) q) :
    pushforwardCochainEquiv i H K (q + 1) (H.d (K.preimage i) q x)
      = (pushforward π i H).d K q (pushforwardCochainEquiv i H K q x)
theorem

cechFinite_pushforward_iff

L133 ↗
AlgebraicGeometry.OModulePresheaf.cechFinite_pushforward_iff
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_cechFinite_pushforward_iff
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.cechFinite_pushforward_iff
    {R : Type u} [CommRing R] {V Z : Scheme.{u}} {π : V ⟶ Spec (.of R)} (i : Z ⟶ V)
      [IsClosedImmersion i]
    (H : OModulePresheaf (i ≫ π)) (K : V.OrderedAffineCover) :
    (OModulePresheaf.pushforward π i H).CechFinite K ↔ H.CechFinite (K.preimage i)

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