NYLL
Module

OModulePresheaf_nonempty_cechEquiv_of_orderIso.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_of_orderIso
14 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty cech Equiv of order Iso

Imports3
Imported by2

Declarations

def

idx

L37 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.idx
Documentation

The equivalence of increasing Cech indices induced by the order isomorphism of the covers.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
Lean source · full declaration
def idx (i : ℕ) : K.Idx i ≃ K'.Idx i where
  toFun s := ⟨e ∘ s.1, e.strictMono.comp s.2⟩
  invFun s' := ⟨e.symm ∘ s'.1, e.symm.strictMono.comp s'.2⟩
  left_inv s := Subtype.ext (funext fun j => e.symm_apply_apply (s.1 j))
  right_inv s' := Subtype.ext (funext fun j => e.apply_symm_apply (s'.1 j))
theorem

idx_face

L43 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.idx_face
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
Lean source · statement
theorem idx_face {i : ℕ} (s : K.Idx (i + 1)) (j : Fin (i + 2)) :
    idx K K' e i (K.face s j) = K'.face (idx K K' e (i + 1) s) j
theorem

inter_idx

L49 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.inter_idx
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
include hU in
Lean source · statement
theorem inter_idx {i : ℕ} (s : K.Idx i) : K'.inter (idx K K' e i s) = K.inter s
theorem

inter_symm

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.inter_symm
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
include hU in
Lean source · statement
theorem inter_symm {i : ℕ} (s' : K'.Idx i) : K'.inter s' = K.inter ((idx K K' e i).symm s')
def

phi

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi
Documentation

The Cech cochain map induced by the order isomorphism and the corresponding restriction maps.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
def phi (i : ℕ) : F.cochain K i →ₗ[R] F.cochain K' i
theorem

phi_apply

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem phi_apply (i : ℕ) (c : F.cochain K i) (s' : K'.Idx i) :
    phi F K K' e hU i c s' = F.res (le_of_eq (inter_symm K K' e hU s')) (c ((idx K K' e i).symm
      s'))
theorem

res_eq_of_eq

L67 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.res_eq_of_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem res_eq_of_eq {U W : V.Opens} (h : U ≤ W) (h' : W ≤ U) (x : F.obj U) : F.res h (F.res h' x)
  = x
theorem

phi_apply_idx

L71 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi_apply_idx
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem phi_apply_idx (i : ℕ) (c : F.cochain K i) (s : K.Idx i) (h : K'.inter (idx K K' e i s) ≤
  K.inter s) :
    phi F K K' e hU i c (idx K K' e i s) = F.res h (c s)
theorem

phi_surjective

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem phi_surjective (i : ℕ) : Function.Surjective (phi F K K' e hU i)
theorem

phi_injective

L89 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem phi_injective (i : ℕ) : Function.Injective (phi F K K' e hU i)
theorem

phi_apply_face

L98 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.phi_apply_face
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem phi_apply_face (i : ℕ) (c : F.cochain K i) (s : K.Idx (i + 1)) (j : Fin (i + 2))
    (h : K'.inter (K'.face (idx K K' e (i + 1) s) j) ≤ K.inter (K.face s j)) :
    phi F K K' e hU i c (K'.face (idx K K' e (i + 1) s) j) = F.res h (c (K.face s j))
theorem

d_phi

L103 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.d_phi
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
Lean source · statement
theorem d_phi (i : ℕ) (c : F.cochain K i) :
    F.d K' i (phi F K K' e hU i c) = phi F K K' e hU (i + 1) (F.d K i c)
theorem

main

L116 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso.P2mCechReindex.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
namespace P2mCechReindex
variable {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
  (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι)
variable (hU : ∀ i, K'.U (e i) = K.U i)
include hU in
Lean source · statement
theorem main : Nonempty (F.H0 K ≃ₗ[R] F.H0 K') ∧ ∀ i : ℕ, Nonempty (F.HSucc K i ≃ₗ[R] F.HSucc K' i)
theorem

nonempty_cechEquiv_of_orderIso

L135 ↗
AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_of_orderIso
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.OModulePresheaf_nonempty_cechEquiv_of_orderIso
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_of_orderIso
    {R : Type u} [CommRing R] {V : Scheme.{u}} {π : V ⟶ Spec (.of R)} (F : OModulePresheaf π)
    (K K' : V.OrderedAffineCover) (e : K.ι ≃o K'.ι) (hU : ∀ i, K'.U (e i) = K.U i) :
    Nonempty (F.H0 K ≃ₗ[R] F.H0 K') ∧ ∀ i : ℕ, Nonempty (F.HSucc K i ≃ₗ[R] F.HSucc K' i)

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