CechLocalizationDegreeZero.lean

def tensorZeroSummandOut (K L : CochainComplex (ModuleCat.{u} R) ℕ)
    (i j : ℕ) (hij : ComplexShape.π (ComplexShape.up ℕ) (ComplexShape.up ℕ)
      (ComplexShape.up ℕ) (i, j) = 0) :
    ((curriedTensor (ModuleCat.{u} R)).obj (K.X i)).obj (L.X j) ⟶ K.X 0 ⊗ L.X 0

def tensorComplexZeroIso (K L : CochainComplex (ModuleCat.{u} R) ℕ) :
    K.X 0 ⊗ L.X 0 ≅ (HomologicalComplex.tensorObj K L).X 0 where
  hom := ιTensorObj K L 0 0 0 rfl
  inv := mapBifunctorDesc (F := curriedTensor (ModuleCat.{u} R))
    (c := ComplexShape.up ℕ) (tensorZeroSummandOut K L)
  hom_inv_id := by
    rw [ι_mapBifunctorDesc]
    change (𝟙 (K.X 0) ⊗ₘ 𝟙 (L.X 0)) = 𝟙 _
    exact id_tensorHom_id (K.X 0) (L.X 0)
  inv_hom_id := by
    apply mapBifunctor.hom_ext
    intro i j hij
    have h : i + j = 0 := hij
    have hi : i = 0 := by omega
    have hj : j = 0 := by omega
    subst i
    subst j
    rw [← Category.assoc, ι_mapBifunctorDesc]
    change (𝟙 (K.X 0) ⊗ₘ 𝟙 (L.X 0)) ≫ ιTensorObj K L 0 0 0 rfl =
      ιTensorObj K L 0 0 0 rfl ≫ 𝟙 _
    rw [id_tensorHom_id, Category.id_comp, Category.comp_id]

def cechLocalizationZeroIso : (xs : List R) →
    (cechLocalizationComplex xs).X 0 ≅ ModuleCat.of R R
  | [] => singleObjXSelf (ComplexShape.up ℕ) 0 (ModuleCat.of R R)
  | x :: xs =>
    (tensorComplexZeroIso (principalLocalizationComplex x (ModuleCat.of R R))
      (cechLocalizationComplex xs)).symm ≪≫
      (tensorLeft (ModuleCat.of R R)).mapIso (cechLocalizationZeroIso xs) ≪≫
      λ_ (ModuleCat.of R R)

def cechCoefficientZeroIso (xs : List R) (M : ModuleCat.{u} R) :
    (((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (cechLocalizationComplex xs)).X 0 ≅ M

theorem cechCoefficientZeroIso_naturality (xs : List R)
    {M N : ModuleCat.{u} R} (f : M ⟶ N) :
    ((tensorComplexCoefficientFunctor (cechLocalizationComplex xs)).map f).f 0 ≫
      (cechCoefficientZeroIso xs N).hom = (cechCoefficientZeroIso xs M).hom ≫ f

def cechHomologyZeroToModule (xs : List R) (M : ModuleCat.{u} R) :
    ((((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (cechLocalizationComplex xs)).homology 0) ⟶ M

instance cechHomologyZeroToModule_mono (xs : List R) (M : ModuleCat.{u} R) :
    Mono (cechHomologyZeroToModule xs M)

theorem cechHomologyZeroToModule_naturality (xs : List R)
    {M N : ModuleCat.{u} R} (f : M ⟶ N) :
    homologyMap ((tensorComplexCoefficientFunctor (cechLocalizationComplex xs)).map f) 0 ≫
      cechHomologyZeroToModule xs N = cechHomologyZeroToModule xs M ≫ f