Module

OrderedAffineCoverCochainPullback.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.OrderedAffineCoverCochainPullback

6 declarations indexed from sourceView source ↗

Module documentation

Ordered Affine Cover Cochain Pullback

Imports4

Mathlib.Data.Fin.Tuple.Sort
Mathlib.GroupTheory.Perm.Sign
Nyll.SchemeTheory.Cohomology.Cech.OrderedAffineCoverCech
Nyll.AlgebraicCurves.Geometry.Schemes.OrderedAffineCoverComap

Imported by28

def

sortIdx

L36 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.sortIdx

Documentation

Sort the image of an injective cover index tuple to obtain a strictly increasing tuple in the target cover.

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory Opposite TopologicalSpace
variable {X Y : Scheme.{u}} (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam
  : 𝒲.ι → 𝒦.ι)

Lean source · statement

def sortIdx {n : ℕ} (s : 𝒲.Idx n) (hinj : Function.Injective (lam ∘ s.1)) : 𝒦.Idx n

theorem

sortIdx_val

L41 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.sortIdx_val

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory Opposite TopologicalSpace
variable {X Y : Scheme.{u}} (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam
  : 𝒲.ι → 𝒦.ι)

Lean source · statement

theorem sortIdx_val {n : ℕ} (s : 𝒲.Idx n) (hinj : Function.Injective (lam ∘ s.1)) :
    (𝒲.sortIdx 𝒦 lam s hinj).1 = (lam ∘ s.1) ∘ (Tuple.sort (lam ∘ s.1))

theorem

inter_le_preimage_inter_sortIdx

L45 ↗

AlgebraicGeometry.Scheme.OrderedAffineCover.inter_le_preimage_inter_sortIdx

Source context 5 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.Scheme.OrderedAffineCover
open CategoryTheory Opposite TopologicalSpace
variable {X Y : Scheme.{u}} (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam
  : 𝒲.ι → 𝒦.ι)

Lean source · statement

theorem inter_le_preimage_inter_sortIdx (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w))
    {n : ℕ} (s : 𝒲.Idx n) (hinj : Function.Injective (lam ∘ s.1)) :
    𝒲.inter s ≤ h ⁻¹ᵁ 𝒦.inter (𝒲.sortIdx 𝒦 lam s hinj)

def

unitPullback

L64 ↗

AlgebraicGeometry.OModulePresheaf.unitPullback

Documentation

Pull back unit-module cochains along a map of ordered covers, including the sign of sorting the image tuple and assigning zero when that tuple is not injective.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable {X Y : Scheme.{u}} {πX : X ⟶ Spec (.of R')} {πY : Y ⟶ Spec (.of R)}

Lean source · statement

def unitPullback (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 : Y.OrderedAffineCover) (lam : 𝒲.ι → 𝒦.ι)
    (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ)
    (z : (unit πY).cochain 𝒦 n) : (unit πX).cochain 𝒲 n

theorem

unitPullback_apply_of_injective

L75 ↗

AlgebraicGeometry.OModulePresheaf.unitPullback_apply_of_injective

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable {X Y : Scheme.{u}} {πX : X ⟶ Spec (.of R')} {πY : Y ⟶ Spec (.of R)}

Lean source · statement

theorem unitPullback_apply_of_injective (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 :
  Y.OrderedAffineCover)
    (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ)
    (z : (unit πY).cochain 𝒦 n) (s : 𝒲.Idx n) (hinj : Function.Injective (lam ∘ s.1)) :
    unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z s =
      ((Equiv.Perm.sign (Tuple.sort (lam ∘ s.1)) : ℤˣ) : ℤ) •
        (X.presheaf.map (homOfLE (𝒲.inter_le_preimage_inter_sortIdx h 𝒦 lam hlam s hinj)).op).hom
          ((h.app (𝒦.inter (𝒲.sortIdx 𝒦 lam s hinj))).hom (z (𝒲.sortIdx 𝒦 lam s hinj)))

theorem

unitPullback_apply_of_not_injective

L86 ↗

AlgebraicGeometry.OModulePresheaf.unitPullback_apply_of_not_injective

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry.OModulePresheaf
open CategoryTheory Opposite TopologicalSpace
variable {R : Type u} [CommRing R] {R' : Type u} [CommRing R']
variable {X Y : Scheme.{u}} {πX : X ⟶ Spec (.of R')} {πY : Y ⟶ Spec (.of R)}

Lean source · statement

theorem unitPullback_apply_of_not_injective (h : X ⟶ Y) (𝒲 : X.OrderedAffineCover) (𝒦 :
  Y.OrderedAffineCover)
    (lam : 𝒲.ι → 𝒦.ι) (hlam : ∀ w, 𝒲.U w ≤ h ⁻¹ᵁ 𝒦.U (lam w)) (n : ℕ)
    (z : (unit πY).cochain 𝒦 n) (s : 𝒲.Idx n) (hinj : ¬ Function.Injective (lam ∘ s.1)) :
    unitPullback (πX := πX) h 𝒲 𝒦 lam hlam n z s = 0

Module documentation

Ordered Affine Cover Cochain Pullback

Declarations

sortIdx

sortIdx_val

inter_le_preimage_inter_sortIdx

unitPullback

unitPullback_apply_of_injective

unitPullback_apply_of_not_injective