NYLL
Module

OModulePresheaf_d_unitPullback.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OModulePresheaf_d_unitPullback
11 declarations indexed from sourceView source ↗

Module documentation

OModule Presheaf d unit Pullback

Imports11
Imported by5

Declarations

theorem

units_pow_mul_self

L43 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.units_pow_mul_self
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem units_pow_mul_self (m : ℕ) : ((-1 : ℤˣ) ^ m) * ((-1 : ℤˣ) ^ m) = 1
theorem

sorted_face_apply

L45 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.sorted_face_apply
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem sorted_face_apply (u : Fin (n + 1) → ι) (hu : Function.Injective u) (j : Fin (n + 1)) (k :
  Fin n) :
    (u ∘ j.succAbove) (Tuple.sort (u ∘ j.succAbove) k) = (u ∘ Tuple.sort u) (((Tuple.sort u).symm
      j).succAbove k)
theorem

sign_sort_face

L53 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.sign_sort_face
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem sign_sort_face (u : Fin (n + 1) → ι) (hu : Function.Injective u) (j : Fin (n + 1)) :
    Equiv.Perm.sign (Tuple.sort (u ∘ j.succAbove)) =
      (-1) ^ ((((Tuple.sort u).symm j) : ℕ) + (j : ℕ)) * Equiv.Perm.sign (Tuple.sort u)
theorem

collision

L68 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.collision
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem collision (u : Fin (n + 1) → ι) {a b : Fin (n + 1)} (hab : a ≠ b) (huab : u a = u b)
    (ha : Function.Injective (u ∘ a.succAbove)) :
    Function.Injective (u ∘ b.succAbove) ∧
    (u ∘ b.succAbove) ∘ Tuple.sort (u ∘ b.succAbove) = (u ∘ a.succAbove) ∘ Tuple.sort (u ∘
      a.succAbove) ∧
    Equiv.Perm.sign (Tuple.sort (u ∘ b.succAbove)) = -((-1) ^ ((a : ℕ) + (b : ℕ)) * Equiv.Perm.sign
      (Tuple.sort (u ∘ a.succAbove)))
theorem

exists_partner

L112 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.exists_partner
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open Equiv
section Comb
variable {ι : Type*} [LinearOrder ι] {n : ℕ}
Lean source · statement
theorem exists_partner (u : Fin (n + 1) → ι) (hu : ¬ Function.Injective u) {a : Fin (n + 1)}
    (ha : Function.Injective (u ∘ a.succAbove)) :
    ∃ b, b ≠ a ∧ u a = u b ∧ ∀ c, c ≠ a → c ≠ b → ¬ Function.Injective (u ∘ c.succAbove)
def

pb

L150 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.pb
Documentation

Pull a cochain component back along h and restrict it to an open subset of its inverse image.

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
section Sheaf
variable {R : Type u} [CommRing R] {X Y : Scheme.{u}} {πY : Y ⟶ Spec (.of R)}
  (h : X ⟶ Y) (𝒦 : Y.OrderedAffineCover) {m : ℕ} (z : (OModulePresheaf.unit πY).cochain 𝒦 m)
Lean source · statement
def pb (T : 𝒦.Idx m) (W : X.Opens) (hW : W ≤ h ⁻¹ᵁ 𝒦.inter T) : Γ(X, W)
theorem

map_pb

L153 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.map_pb
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
section Sheaf
variable {R : Type u} [CommRing R] {X Y : Scheme.{u}} {πY : Y ⟶ Spec (.of R)}
  (h : X ⟶ Y) (𝒦 : Y.OrderedAffineCover) {m : ℕ} (z : (OModulePresheaf.unit πY).cochain 𝒦 m)
Lean source · statement
theorem map_pb (T : 𝒦.Idx m) {W W' : X.Opens} (hW : W ≤ h ⁻¹ᵁ 𝒦.inter T) (hW' : W' ≤ W) (hW'' : W'
  ≤ h ⁻¹ᵁ 𝒦.inter T) :
    (X.presheaf.map (homOfLE hW').op).hom (pb h 𝒦 z T W hW) = pb h 𝒦 z T W' hW''
theorem

pb_congr

L160 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.pb_congr
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
section Sheaf
variable {R : Type u} [CommRing R] {X Y : Scheme.{u}} {πY : Y ⟶ Spec (.of R)}
  (h : X ⟶ Y) (𝒦 : Y.OrderedAffineCover) {m : ℕ} (z : (OModulePresheaf.unit πY).cochain 𝒦 m)
Lean source · statement
theorem pb_congr {T T' : 𝒦.Idx m} (e : T = T') (W : X.Opens) (hW : W ≤ h ⁻¹ᵁ 𝒦.inter T) (hW' : W ≤
  h ⁻¹ᵁ 𝒦.inter T') :
    pb h 𝒦 z T W hW = pb h 𝒦 z T' W hW'
theorem

map_app_map_eq_pb

L165 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.map_app_map_eq_pb
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
section Sheaf
variable {R : Type u} [CommRing R] {X Y : Scheme.{u}} {πY : Y ⟶ Spec (.of R)}
  (h : X ⟶ Y) (𝒦 : Y.OrderedAffineCover) {m : ℕ} (z : (OModulePresheaf.unit πY).cochain 𝒦 m)
Lean source · statement
theorem map_app_map_eq_pb (S : 𝒦.Idx (m + 1)) (i : Fin (m + 2)) (W : X.Opens) (hW : W ≤ h ⁻¹ᵁ
  𝒦.inter S) :
    (X.presheaf.map (homOfLE hW).op).hom ((h.app (𝒦.inter S)).hom
      ((Y.presheaf.map (homOfLE (𝒦.inter_le_inter_face S i)).op).hom (z (𝒦.face S i)))) =
      pb h 𝒦 z (𝒦.face S i) W (hW.trans (h.preimage_mono (𝒦.inter_le_inter_face S i)))
theorem

val_negOne_pow

L183 ↗
AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback.DCommAux.val_negOne_pow
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
namespace DCommAux
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
Lean source · statement
theorem val_negOne_pow (m : ℕ) : (((-1 : ℤˣ) ^ m : ℤˣ) : ℤ) = (-1 : ℤ) ^ m
theorem

d_unitPullback

L192 ↗
AlgebraicGeometry.OModulePresheaf.d_unitPullback
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Sheaves.Proofs.OModulePresheaf_d_unitPullback
universe u
open CategoryTheory Opposite TopologicalSpace AlgebraicGeometry
open DCommAux in
Lean source · statement
theorem _root_.AlgebraicGeometry.OModulePresheaf.d_unitPullback
    {R R' : Type u} [CommRing R] [CommRing R'] {X Y : Scheme.{u}}
    (πX : X ⟶ Spec (CommRingCat.of R')) (πY : Y ⟶ Spec (CommRingCat.of R))
    (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ) (z : (OModulePresheaf.unit πY).cochain 𝒦 n) :
    (OModulePresheaf.unit πX).d 𝒲 n (OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z) =
      OModulePresheaf.unitPullback (πX := πX) h 𝒲 𝒦 lam hlam (n + 1) ((OModulePresheaf.unit πY).d 𝒦
        n z)

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