NYLL
Module

OModulePresheaf_nonempty_cechEquiv_of_orderIso_orderDual.lean

Nyll.AlgebraicCurves.Cohomology.Cech.OModulePresheaf_nonempty_cechEquiv_of_orderIso_orderDual
20 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf nonempty cech Equiv of order Iso order Dual

Imports3
Imported by2

Declarations

def

idx

L37 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.idx
Documentation

The equivalence of increasing Cech indices induced by reversing their order.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 := ⟨fun k => ofDual (e (s.1 (Fin.rev k))), fun k k' h =>
    ofDual_lt_ofDual.mpr (e.strictMono (s.2 (Fin.rev_lt_rev.mpr h)))⟩
  invFun s' := ⟨fun k => e.symm (toDual (s'.1 (Fin.rev k))), fun k k' h =>
    e.symm.strictMono (toDual_lt_toDual.mpr (s'.2 (Fin.rev_lt_rev.mpr h)))⟩
  left_inv s := Subtype.ext (funext fun j => by simp [Fin.rev_rev])
  right_inv s' := Subtype.ext (funext fun j => by simp [Fin.rev_rev])
theorem

idx_apply

L45 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.idx_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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_apply {i : ℕ} (s : K.Idx i) (k : Fin (i + 1)) : (idx K K' e i s).1 k = ofDual (e (s.1
  (Fin.rev k)))
theorem

idx_face

L49 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.idx_face
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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) (Fin.rev j)
theorem

inter_idx

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.inter_idx
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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

L66 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.inter_symm
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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

sgn

L71 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.sgn
Documentation

The degree-dependent sign correcting the reversed order in the Cech differential.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · full declaration
def sgn : ℕ → ℤ
  | 0 => 1
  | n + 1 => (-1) ^ (n + 1) * sgn n
theorem

sgn_succ

L75 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.sgn_succ
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
theorem sgn_succ (n : ℕ) : sgn (n + 1) = (-1) ^ (n + 1) * sgn n
theorem

sgn_mul_self

L77 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.sgn_mul_self
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
theorem sgn_mul_self (n : ℕ) : sgn n * sgn n = 1
def

phi

L84 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi
Documentation

The signed Cech cochain map induced by order reversal 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.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
def phi (i : ℕ) : F.cochain K i →ₗ[R] F.cochain K' i
theorem

phi_apply

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi_apply
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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' =
      (sgn i : ℤ) • 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

L92 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.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.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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

L96 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi_apply_idx
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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) = (sgn i : ℤ) • F.res h (c s)
theorem

phi_apply_face

L107 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi_apply_face
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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) (Fin.rev j)) ≤ K.inter (K.face s j)) :
    phi F K K' e hU i c (K'.face (idx K K' e (i + 1) s) (Fin.rev j)) = (sgn i : ℤ) • F.res h (c
      (K.face s j))
theorem

inter_face_le

L120 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.inter_face_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
include hU in
Lean source · statement
theorem inter_face_le (i : ℕ) (s : K.Idx (i + 1)) (j : Fin (i + 2)) :
    K'.inter (K'.face (idx K K' e (i + 1) s) (Fin.rev j)) ≤ K.inter (K.face s j)
theorem

phi_surjective

L124 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
theorem phi_surjective (i : ℕ) : Function.Surjective (phi F K K' e hU i)
theorem

phi_injective

L134 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.phi_injective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
theorem phi_injective (i : ℕ) : Function.Injective (phi F K K' e hU i)
theorem

neg_one_pow_rev

L144 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.neg_one_pow_rev
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (e i)) = K.U i)
Lean source · statement
theorem neg_one_pow_rev {i : ℕ} (j : Fin (i + 2)) :
    ((-1 : ℤ) ^ ((Fin.rev j : Fin (i + 2)) : ℕ)) * sgn i = sgn (i + 1) * (-1) ^ (j : ℕ)
theorem

d_phi

L157 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.d_phi
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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

L171 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual.P2mCechReverse.main
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
namespace P2mCechReverse
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 (ofDual (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_orderDual

L190 ↗
AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_of_orderIso_orderDual
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.SheafCechEquivOrderIsoOrderDual
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry OrderDual
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.nonempty_cechEquiv_of_orderIso_orderDual
    {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 (OrderDual.ofDual (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.