OModulePresheafLerayBicomplex.lean

theorem _root_.AlgebraicGeometry.Scheme.OrderedAffineCover.fiberAffineOpen
    (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
    {W : V'.Opens} (hW : IsAffineOpen W) {U : Z.Opens} (hU : IsAffineOpen U) :
    IsAffineOpen (W ⊓ (Opens.map p.base).obj U)

def restrictToPreimage
    (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
    (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U) :
    Scheme.OrderedAffineCoverOf ((Opens.map p.base).obj U) where
  ι := K'.ι
  U := fun i => K'.U i ⊓ (Opens.map p.base).obj U
  isAffineOpen := fun i => Scheme.OrderedAffineCover.fiberAffineOpen p πZ (K'.isAffineOpen i) hU
  le := fun _ => inf_le_right
  iSup_eq := by rw [← iSup_inf_eq, K'.iSup_eq_top, top_inf_eq]

theorem restrictToPreimage_U
    (p : V' ⟶ Z) (πZ : Z ⟶ Spec (CommRingCat.of R)) [IsSeparated πZ]
    (K' : Scheme.OrderedAffineCover V') {U : Z.Opens} (hU : IsAffineOpen U) (i : K'.ι) :
    (restrictToPreimage p πZ K' hU).U i = K'.U i ⊓ (Opens.map p.base).obj U

abbrev HIdx (a : ℕ)

abbrev VIdx (b : ℕ)

abbrev biOpen (a b : ℕ)
    (σ : HIdx K a) (τ : VIdx K' b) : V'.Opens

abbrev BiIdx (a b : ℕ) : Type u

abbrev biC (a b : ℕ) : Type u

instance biC_abGrp (a b : ℕ) :
    AddCommGroup (biC p πZ K K' a b)

instance biC_module (a b : ℕ) :
    Module R (biC p πZ K K' a b)

def dH (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    biC p πZ K K' a b →ₗ[R] biC p πZ K K' (a + 1) b :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun στ => ∑ j : Fin (a + 2), ((-1 : ℤ) ^ (j : ℕ)) •
    ((Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
      (inf_le_inf_left _ ((Opens.map p.base).monotone
        (K.inter_le_inter_face στ.1 j)))).comp
      (LinearMap.proj (R := R) (⟨K.face στ.1 j, στ.2⟩ :
        BiIdx K K' a b)))

def dV (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    biC p πZ K K' a b →ₗ[R] biC p πZ K K' a (b + 1) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun στ => ∑ j : Fin (b + 2), ((-1 : ℤ) ^ (j : ℕ)) •
    ((Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
      (inf_le_inf_right _ (K'.inter_le_inter_face στ.2 j))).comp
      (LinearMap.proj (R := R) (⟨στ.1, K'.face στ.2 j⟩ :
        BiIdx K K' a b)))

theorem dH_apply (a b : ℕ) (f : biC p πZ K K' a b)
    (στ : BiIdx K K' (a + 1) b) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    dH p πZ K K' a b f στ
      = ∑ j : Fin (a + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
            (inf_le_inf_left _ ((Opens.map p.base).monotone
              (K.inter_le_inter_face στ.1 j)))
            (f ⟨K.face στ.1 j, στ.2⟩) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  simp only [dH, LinearMap.pi_apply, LinearMap.sum_apply]
  exact Finset.sum_congr rfl fun j _ => rfl

theorem dH_apply' (a b : ℕ) (f : biC p πZ K K' a b)
    (στ : BiIdx K K' (a + 1) b) :
    dH p πZ K K' a b f στ
      = ∑ j : Fin (a + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          (V'.presheaf.map (homOfLE (inf_le_inf_left (K'.inter στ.2)
            ((Opens.map p.base).monotone (K.inter_le_inter_face στ.1 j)))).op).hom
            (f ⟨K.face στ.1 j, στ.2⟩)

theorem dV_apply (a b : ℕ) (f : biC p πZ K K' a b)
    (στ : BiIdx K K' a (b + 1)) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    dV p πZ K K' a b f στ
      = ∑ j : Fin (b + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
            (inf_le_inf_right _ (K'.inter_le_inter_face στ.2 j))
            (f ⟨στ.1, K'.face στ.2 j⟩) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  simp only [dV, LinearMap.pi_apply, LinearMap.sum_apply]
  exact Finset.sum_congr rfl fun j _ => rfl

theorem dV_apply' (a b : ℕ) (f : biC p πZ K K' a b)
    (στ : BiIdx K K' a (b + 1)) :
    dV p πZ K K' a b f στ
      = ∑ j : Fin (b + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          (V'.presheaf.map (homOfLE (inf_le_inf_right
            ((Opens.map p.base).obj (K.inter στ.1))
            (K'.inter_le_inter_face στ.2 j))).op).hom
            (f ⟨στ.1, K'.face στ.2 j⟩)

theorem biC_subsingleton (a b : ℕ)
    (h : max (Fintype.card K.ι) (Fintype.card K'.ι) ≤ a
          ∨ max (Fintype.card K.ι) (Fintype.card K'.ι) ≤ b) :
    Subsingleton (biC p πZ K K' a b)

abbrev relAltC (U : Z.Opens) (b : ℕ) : Type u

def relAltd (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltC p πZ K' U b →ₗ[R] relAltC p πZ K' U (b + 1) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun τ => ∑ j : Fin (b + 2), ((-1 : ℤ) ^ (j : ℕ)) •
    ((Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
      (inf_le_inf_right _ (K'.inter_le_inter_face τ j))).comp
      (LinearMap.proj (R := R) (K'.face τ j)))

theorem relAltd_apply' (U : Z.Opens) (b : ℕ)
    (f : relAltC p πZ K' U b) (τ : K'.Idx (b + 1)) :
    relAltd p πZ K' U b f τ
      = ∑ j : Fin (b + 2), ((-1 : ℤ) ^ (j : ℕ)) •
          (V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U)
            (K'.inter_le_inter_face τ j))).op).hom
            (f (K'.face τ j))

def relAltHB (U : Z.Opens) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (b : ℕ) → Submodule R (LinearMap.ker (relAltd p πZ K' U b)) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  fun b => match b with
  | 0 => ⊥
  | b' + 1 => (LinearMap.range (relAltd p πZ K' U b')).comap
      (LinearMap.ker (relAltd p πZ K' U (b' + 1))).subtype

abbrev relAltH (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    Type u :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.ker (relAltd p πZ K' U b) ⧸ relAltHB p πZ K' U b

def pushOpen (U : Z.Opens) : OModulePresheaf (p ≫ πZ) where
  obj W := Γ(V', W ⊓ (Opens.map p.base).obj U)
  addCommGroup _ := inferInstance
  module W := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ) _
  moduleSections W := Module.compHom _
    (V'.presheaf.map (homOfLE (inf_le_left : W ⊓ (Opens.map p.base).obj U ≤ W)).op).hom
  isScalarTower W := by
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ) W
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ) (W ⊓ (Opens.map p.base).obj U)
    let : Module Γ(V', W) Γ(V', W ⊓ (Opens.map p.base).obj U) := Module.compHom _
      (V'.presheaf.map (homOfLE (inf_le_left : W ⊓ (Opens.map p.base).obj U ≤ W)).op).hom
    refine ⟨fun r a x => ?_⟩
    change (V'.presheaf.map (homOfLE (inf_le_left (b := (Opens.map p.base).obj U))).op).hom
          ((V'.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom
            ((p ≫ πZ).appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom r)) * a) * x
      = (V'.presheaf.map (homOfLE (le_top : W ⊓ (Opens.map p.base).obj U ≤ ⊤)).op).hom
            ((p ≫ πZ).appTop.hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom r))
          * ((V'.presheaf.map (homOfLE inf_le_left).op).hom a * x)
    rw [map_mul, ← mul_assoc, ← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
      homOfLE_comp]
  res h := Scheme.OrderedAffineCoverOf.res (p ≫ πZ) (inf_le_inf_right _ h)
  res_smul {W W'} h a x := by
    change (V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U) h)).op).hom
          ((V'.presheaf.map (homOfLE inf_le_left).op).hom a * x)
      = (V'.presheaf.map (homOfLE inf_le_left).op).hom ((V'.presheaf.map (homOfLE h).op).hom a)
          * (V'.presheaf.map (homOfLE (inf_le_inf_right _ h)).op).hom x
    rw [map_mul, ← CommRingCat.comp_apply, ← CommRingCat.comp_apply, ← Functor.map_comp,
      ← Functor.map_comp, ← op_comp, ← op_comp, homOfLE_comp, homOfLE_comp]
  res_refl W := (OModulePresheaf.unit (p ≫ πZ)).res_refl _
  res_comp h h' := (OModulePresheaf.unit (p ≫ πZ)).res_comp _ _

theorem relAltd_eq_d (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltd p πZ K' U b
      = OModulePresheaf.d (pushOpen p πZ U) K' b := rfl

def pullOpen (W : V'.Opens) : OModulePresheaf πZ where
  obj U := Γ(V', W ⊓ (Opens.map p.base).obj U)
  addCommGroup _ := inferInstance
  module U := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ) _
  moduleSections U := Module.compHom _
    (p.appLE U (W ⊓ (Opens.map p.base).obj U) inf_le_right).hom
  isScalarTower U := by
    let := Scheme.OrderedAffineCoverOf.moduleSections πZ U
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ) (W ⊓ (Opens.map p.base).obj U)
    let : Module Γ(Z, U) Γ(V', W ⊓ (Opens.map p.base).obj U) :=
      Module.compHom _ (p.appLE U (W ⊓ (Opens.map p.base).obj U) inf_le_right).hom
    refine ⟨fun r a x => ?_⟩
    change (p.appLE U (W ⊓ (Opens.map p.base).obj U) inf_le_right).hom
          ((Z.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op).hom
            ((πZ.app ⊤).hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom r)) * a) * x
      = (V'.presheaf.map (homOfLE (le_top : W ⊓ (Opens.map p.base).obj U ≤ ⊤)).op).hom
            (((p ≫ πZ).app ⊤).hom ((Scheme.ΓSpecIso (CommRingCat.of R)).inv.hom r))
          * ((p.appLE U (W ⊓ (Opens.map p.base).obj U) inf_le_right).hom a * x)
    rw [map_mul, ← mul_assoc]
    congr 2
    erw [← CommRingCat.comp_apply, Scheme.Hom.map_appLE]
    rfl
  res h := Scheme.OrderedAffineCoverOf.res (p ≫ πZ) (inf_le_inf_left W ((Opens.map
    p.base).monotone h))
  res_smul {U U'} h a x := by
    change (V'.presheaf.map (homOfLE (inf_le_inf_left W ((Opens.map p.base).monotone h))).op).hom
          ((p.appLE U' (W ⊓ (Opens.map p.base).obj U') inf_le_right).hom a * x)
      = (p.appLE U (W ⊓ (Opens.map p.base).obj U) inf_le_right).hom
            ((Z.presheaf.map (homOfLE h).op).hom a)
          * (V'.presheaf.map (homOfLE (inf_le_inf_left W ((Opens.map p.base).monotone h))).op).hom x
    rw [map_mul, ← CommRingCat.comp_apply, ← CommRingCat.comp_apply (f := Z.presheaf.map _),
      Scheme.Hom.appLE_map, Scheme.Hom.map_appLE]
  res_refl U := (OModulePresheaf.unit (p ≫ πZ)).res_refl _
  res_comp h h' := (OModulePresheaf.unit (p ≫ πZ)).res_comp _ _

instance relAltC_modΓ (U : Z.Opens) (b : ℕ) :
    Module Γ(Z, U) (relAltC p πZ K' U b)

theorem relAltd_Γsmul (U : Z.Opens) (b : ℕ) (a : Γ(Z, U))
    (f : relAltC p πZ K' U b) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltd p πZ K' U b (a • f) = a • relAltd p πZ K' U b f := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  have hstep : ∀ (W₁ W₂ : V'.Opens) (h : W₁ ≤ W₂)
      (e₁ : W₁ ⊓ (Opens.map p.base).obj U ≤ p ⁻¹ᵁ U)
      (e₂ : W₂ ⊓ (Opens.map p.base).obj U ≤ p ⁻¹ᵁ U)
      (x : Γ(V', W₂ ⊓ (Opens.map p.base).obj U)),
      (V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U) h)).op).hom
          ((p.appLE U (W₂ ⊓ (Opens.map p.base).obj U) e₂).hom a * x)
        = (p.appLE U (W₁ ⊓ (Opens.map p.base).obj U) e₁).hom a
          * (V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U) h)).op).hom x :=
    fun _ _ _ _ _ _ => by rw [map_mul, ← CommRingCat.comp_apply, Scheme.Hom.appLE_map]
  funext τ
  refine (relAltd_apply' p πZ K' U b (a • f) τ).trans
    ((Finset.sum_congr rfl fun (j : Fin (b + 2)) _ =>
      (congrArg (((-1 : ℤ) ^ (j : ℕ)) • ·)
        (hstep (K'.inter τ) (K'.inter (K'.face τ j))
          (K'.inter_le_inter_face τ j) inf_le_right inf_le_right
          (f (K'.face τ j)))).trans (mul_smul_comm _ _ _).symm).trans ?_)
  rw [← Finset.mul_sum, ← relAltd_apply' p πZ K' U b f τ]
  rfl

instance relAltC_scalarTower (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections πZ U
    IsScalarTower R Γ(Z, U) (relAltC p πZ K' U b) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections πZ U
  exact ⟨fun r a f => funext fun τ =>
    ((pullOpen p πZ (K'.inter τ)).isScalarTower U).smul_assoc
      r a (f τ)⟩

instance ker_relAltd_smul (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    SMul Γ(Z, U) ↥(LinearMap.ker (relAltd p πZ K' U b)) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  ⟨fun a x => ⟨a • x.1, LinearMap.mem_ker.mpr <| by
    rw [relAltd_Γsmul, LinearMap.mem_ker.mp x.2, smul_zero]⟩⟩

instance ker_relAltd_modΓ (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    Module Γ(Z, U) ↥(LinearMap.ker (relAltd p πZ K' U b)) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  Function.Injective.module Γ(Z, U) ⟨⟨Subtype.val, rfl⟩, fun _ _ => rfl⟩
    Subtype.val_injective (fun _ _ => rfl)

theorem relAltHB_Γsmul (U : Z.Opens) (b : ℕ) (a : Γ(Z, U))
    (x : letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
      ↥(LinearMap.ker (relAltd p πZ K' U b)))
    (hx : x ∈ relAltHB p πZ K' U b) :
    a • x ∈ relAltHB p πZ K' U b := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  rcases b with _ | b'
  · exact (Submodule.mem_bot R).mpr (by rw [(Submodule.mem_bot R).mp hx, smul_zero])
  · obtain ⟨y, hy⟩ := hx
    exact ⟨a • y, (relAltd_Γsmul p πZ K' U b' a y).trans
      (congrArg (a • ·) hy)⟩

instance relAltH_smul (U : Z.Opens) (b : ℕ) :
    SMul Γ(Z, U) (relAltH p πZ K' U b)

instance relAltH_modΓ (U : Z.Opens) (b : ℕ) :
    Module Γ(Z, U) (relAltH p πZ K' U b)

instance relAltH_scalarTower (U : Z.Opens) (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections πZ U
    IsScalarTower R Γ(Z, U) (relAltH p πZ K' U b) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections πZ U
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine ⟨fun r a => Quotient.ind' fun x => congrArg Submodule.Quotient.mk
    (Subtype.ext ?_)⟩
  exact (relAltC_scalarTower p πZ K' U b).smul_assoc r a x.1

def relRes {U U' : Z.Opens} (h : U ≤ U') (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltC p πZ K' U' b →ₗ[R] relAltC p πZ K' U b :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  LinearMap.pi fun τ => (Scheme.OrderedAffineCoverOf.res (p ≫ πZ)
    (inf_le_inf_left (K'.inter τ) ((Opens.map p.base).monotone h))).comp (LinearMap.proj τ)

theorem relRes_apply {U U' : Z.Opens} (h : U ≤ U') (b : ℕ) (f : relAltC p πZ K' U' b) (τ : K'.Idx
    b) :
    relRes p πZ K' h b f τ
      = (V'.presheaf.map (homOfLE (inf_le_inf_left (K'.inter τ) ((Opens.map p.base).monotone
        h))).op).hom
          (f τ)

theorem relRes_comm {U U' : Z.Opens} (h : U ≤ U') (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relRes p πZ K' h (b + 1) ∘ₗ relAltd p πZ K' U' b = relAltd p πZ K' U b ∘ₗ relRes p πZ K' h b
      := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  refine LinearMap.ext fun f => funext fun τ => ?_
  rw [LinearMap.comp_apply, LinearMap.comp_apply, relRes_apply, relAltd_apply', relAltd_apply',
    map_sum]
  refine Finset.sum_congr rfl fun j _ => ?_
  rw [map_zsmul, relRes_apply]
  congr 1
  have hmaps :
      V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U')
        (K'.inter_le_inter_face τ j))).op ≫
        V'.presheaf.map (homOfLE (inf_le_inf_left (K'.inter τ)
          ((Opens.map p.base).monotone h))).op =
      V'.presheaf.map (homOfLE (inf_le_inf_left (K'.inter (K'.face τ j))
        ((Opens.map p.base).monotone h))).op ≫
        V'.presheaf.map (homOfLE (inf_le_inf_right ((Opens.map p.base).obj U)
          (K'.inter_le_inter_face τ j))).op :=
    (V'.presheaf.map_comp _ _).symm.trans
      ((congrArg V'.presheaf.map (Subsingleton.elim _ _)).trans
        (V'.presheaf.map_comp _ _))
  exact ConcreteCategory.congr_hom hmaps (f (K'.face τ j))

def relResKer {U U' : Z.Opens} (h : U ≤ U') (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    LinearMap.ker (relAltd p πZ K' U' b) →ₗ[R] LinearMap.ker (relAltd p πZ K' U b) :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  (relRes p πZ K' h b).restrict fun f hf => LinearMap.mem_ker.mpr <| by
    rw [← LinearMap.comp_apply, ← relRes_comm, LinearMap.comp_apply, LinearMap.mem_ker.mp hf,
      map_zero]

theorem relResKer_coe {U U' : Z.Opens} (h : U ≤ U') (b : ℕ)
    (x : letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ); ↥(LinearMap.ker (relAltd p
      πZ K' U' b))) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    (relResKer p πZ K' h b x : relAltC p πZ K' U b) = relRes p πZ K' h b x := rfl

theorem relAltHB_res_le {U U' : Z.Opens} (h : U ≤ U') (b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    relAltHB p πZ K' U' b
      ≤ (relAltHB p πZ K' U b).comap
          (relResKer p πZ K' h b) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  rcases b with _ | b'
  · exact bot_le
  · rintro x ⟨y, hy⟩
    exact ⟨relRes p πZ K' h b' y,
      (LinearMap.congr_fun (relRes_comm p πZ K' h b') y).symm.trans
        (congrArg (relRes p πZ K' h (b' + 1)) hy)⟩

def relHPresheaf (b : ℕ) : OModulePresheaf πZ where
  obj U := relAltH p πZ K' U b
  addCommGroup _ :=
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    inferInstance
  module U :=
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    inferInstance
  moduleSections U := relAltH_modΓ p πZ K' U b
  isScalarTower U := relAltH_scalarTower p πZ K' U b
  res {U U'} h :=
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    Submodule.mapQ _ _ (relResKer p πZ K' h b) (relAltHB_res_le p πZ K' h b)
  res_smul {U U'} h a z := by
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    induction z using Quotient.inductionOn' with | _ x => ?_
    exact congrArg Submodule.Quotient.mk (Subtype.ext (funext fun τ =>
      (pullOpen p πZ (K'.inter τ)).res_smul h a (x.1 τ)))
  res_refl U := by
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    refine LinearMap.ext fun z => z.inductionOn' fun x =>
      congrArg Submodule.Quotient.mk (Subtype.ext (funext fun τ => ?_))
    exact LinearMap.congr_fun ((OModulePresheaf.unit (p ≫ πZ)).res_refl _) (x.1 τ)
  res_comp {U U' U''} h h' := by
    let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    refine LinearMap.ext fun z => z.inductionOn' fun x =>
      congrArg Submodule.Quotient.mk (Subtype.ext (funext fun τ => ?_))
    exact LinearMap.congr_fun ((OModulePresheaf.unit (p ≫ πZ)).res_comp
      (inf_le_inf_left _ ((Opens.map p.base).monotone h))
      (inf_le_inf_left _ ((Opens.map p.base).monotone h'))) (x.1 τ)

def biC_uncurry (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    biC p πZ K K' a b ≃ₗ[R]
      ∀ σ : K.Idx a,
        relAltC p πZ K' (K.inter σ) b :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  { toFun := fun f σ τ => f (σ, τ)
    invFun := fun g στ => g στ.1 στ.2
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }

theorem dV_uncurry (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    ∀ x σ, biC_uncurry p πZ K K' a (b + 1)
        (dV p πZ K K' a b x) σ
      = relAltd p πZ K' (K.inter σ) b
          (biC_uncurry p πZ K K' a b x σ) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  intro x σ; funext τ
  simp only [biC_uncurry, dV, relAltd,
    LinearEquiv.coe_mk, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.pi_apply,
    LinearMap.sum_apply]
  exact Finset.sum_congr rfl fun d _ => rfl

def biC_uncurry' (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    biC p πZ K K' a b ≃ₗ[R]
      ∀ τ : K'.Idx b,
        OModulePresheaf.cochain (pullOpen p πZ (K'.inter τ))
          K a :=
  letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  { toFun := fun f τ σ => f (σ, τ)
    invFun := fun g στ => g στ.2 στ.1
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl
    left_inv := fun _ => rfl
    right_inv := fun _ => rfl }

theorem dH_uncurry (a b : ℕ) :
    letI := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
    ∀ x τ, biC_uncurry' p πZ K K' (a + 1) b
        (dH p πZ K K' a b x) τ
      = OModulePresheaf.d (pullOpen p πZ (K'.inter τ))
          K a (biC_uncurry' p πZ K K' a b x τ) := by
  let := Scheme.OrderedAffineCoverOf.moduleSections (p ≫ πZ)
  intro x τ; funext σ
  change dH p πZ K K' a b x (σ, τ) =
    OModulePresheaf.d (pullOpen p πZ (K'.inter τ)) K a (fun σ => x (σ, τ)) σ
  erw [dH_apply, OModulePresheaf.d_apply]
  exact Finset.sum_congr rfl fun j _ => rfl