DerivedLocalCohomologyInjectiveComplex.lean

abbrev torsionShortComplex
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ)

abbrev torsionCocycleQuotient
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ)

def quotientHomToPowerTorsion
    (I : Ideal R) (V : ModuleCat.{u} R) (k : ℕ) :
    (ModuleCat.of R (R ⧸ I ^ k) ⟶ V) →ₗ[R] Ideal.primaryComponent V I where
  toFun f := ⟨f (Ideal.Quotient.mk (I ^ k) 1),
    (Ideal.primaryComponent_mem (M := V) (I := I) _).mpr
      ⟨k, (quotientHomEquivTorsionBySet (I ^ k) f.hom).property⟩⟩
  map_add' _ _ := Subtype.ext rfl
  map_smul' _ _ := Subtype.ext rfl

def quotientCyclesToPowerTorsionCycles
    (I : Ideal R) (J : InjectiveResolution M) (n k : ℕ) :
    LinearMap.ker (injectiveResolutionLinearCoyonedaShortComplexSucc J
      (ModuleCat.of R (R ⧸ I ^ k)) n).g.hom →ₗ[R]
        LinearMap.ker (torsionShortComplex I J n).g.hom where
  toFun f := ⟨quotientHomToPowerTorsion I (J.cocomplex.X (n + 1)) k f.1, by
    apply Subtype.ext
    exact ConcreteCategory.congr_hom f.2 (Ideal.Quotient.mk (I ^ k) 1)⟩
  map_add' f g := Subtype.ext (Subtype.ext rfl)
  map_smul' a f := Subtype.ext (Subtype.ext rfl)

def quotientCocyclesToTorsionCocycleQuotient
    (I : Ideal R) (J : InjectiveResolution M) (n k : ℕ) :
    ((LinearMap.ker (injectiveResolutionLinearCoyonedaShortComplexSucc J
      (ModuleCat.of R (R ⧸ I ^ k)) n).g.hom) ⧸
        LinearMap.range (injectiveResolutionLinearCoyonedaShortComplexSucc J
          (ModuleCat.of R (R ⧸ I ^ k)) n).moduleCatToCycles) →ₗ[R]
      torsionCocycleQuotient I J n

def extToTorsionCocycleQuotient
    (I : Ideal R) (J : InjectiveResolution M) (n k : ℕ) :
    Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ k)) M (n + 1) →ₗ[R]
      torsionCocycleQuotient I J n

theorem extToTorsionCocycleQuotient_extMk
    (I : Ideal R) (J : InjectiveResolution M) (n k : ℕ)
    (f : ModuleCat.of R (R ⧸ I ^ k) ⟶ J.cocomplex.X (n + 1))
    (hf : f ≫ J.cocomplex.d (n + 1) (n + 2) = 0) :
    extToTorsionCocycleQuotient I J n k (J.extMk f (n + 2) (by omega) hf) =
      Submodule.Quotient.mk (quotientCyclesToPowerTorsionCycles I J n k ⟨f, hf⟩) := by
  change quotientCocyclesToTorsionCocycleQuotient I J n k
    ((injectiveResolutionCocycleQuotientEquivExtSucc J
      (ModuleCat.of R (R ⧸ I ^ k)) n).symm
        (J.extMk f (n + 2) (by omega) hf)) = _
  rw [injectiveResolutionCocycleQuotientEquivExtSucc_symm_extMk]
  rfl

def torsionCocycleQuotientCocone
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    Cocone (derivedLocalCohomologyPowersDiagram I M (n + 1)) where
  pt := AddCommGrpCat.of (torsionCocycleQuotient I J n)
  ι :=
    { app := fun k => AddCommGrpCat.ofHom
        (extToTorsionCocycleQuotient I J n (unop (unop k))).toAddMonoidHom
      naturality := by
        intro j k g
        ext α
        let q : ModuleCat.of R (R ⧸ I ^ unop (unop k)) ⟶
            ModuleCat.of R (R ⧸ I ^ unop (unop j)) :=
          (localCohomology.ringModIdeals (localCohomology.idealPowersDiagram I)).map g.unop
        change extToTorsionCocycleQuotient I J n (unop (unop k))
            ((Abelian.Ext.mk₀ q).comp α (zero_add (n + 1))) =
          extToTorsionCocycleQuotient I J n (unop (unop j)) α
        obtain ⟨f, hf, rfl⟩ := J.extMk_surjective α (n + 2) (by omega)
        change (ModuleCat.of R (R ⧸ I ^ unop (unop j)) ⟶
          J.cocomplex.X (n + 1)) at f
        refine (congrArg (extToTorsionCocycleQuotient I J n (unop (unop k)))
          (J.mk₀_comp_extMk f (n + 2) (by omega) hf q)).trans ?_
        refine (extToTorsionCocycleQuotient_extMk I J n (unop (unop k)) (q ≫ f)
          (by
            exact (Category.assoc q f (J.cocomplex.d (n + 1) (n + 2))).trans
              ((congrArg (fun k => q ≫ k) hf).trans (Limits.comp_zero)))).trans
            (Eq.trans ?_ (extToTorsionCocycleQuotient_extMk I J n
              (unop (unop j)) f hf).symm)
        apply congrArg Submodule.Quotient.mk
        exact Subtype.ext (Subtype.ext rfl) }

def localCohomologyToTorsionCocycleQuotientAddHom
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    derivedLocalCohomology I M (n + 1) ⟶
      AddCommGrpCat.of (torsionCocycleQuotient I J n)

theorem localCohomologyToTorsionCocycleQuotientAddHom_ι
    (I : Ideal R) (J : InjectiveResolution M) (n k : ℕ)
    (α : Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ k)) M (n + 1)) :
    localCohomologyToTorsionCocycleQuotientAddHom I J n
        (colimit.ι (derivedLocalCohomologyPowersDiagram I M (n + 1)) (op (op k)) α) =
      extToTorsionCocycleQuotient I J n k α

def localCohomologyToTorsionCocycleQuotient
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    derivedLocalCohomologyModule I M (n + 1) →ₗ[R]
      torsionCocycleQuotient I J n where
  toFun := localCohomologyToTorsionCocycleQuotientAddHom I J n
  map_add' := (localCohomologyToTorsionCocycleQuotientAddHom I J n).hom.map_add
  map_smul' a z := by
    let : PreservesFilteredColimitsOfSize.{0, 0} (forget AddCommGrpCat.{u}) :=
      preservesSmallestFilteredColimits_of_preservesFilteredColimits _
    obtain ⟨k, α, hα⟩ :=
      Concrete.colimit_exists_rep (derivedLocalCohomologyPowersDiagram I M (n + 1)) z
    rcases k with ⟨⟨k⟩⟩
    change localCohomologyToTorsionCocycleQuotientAddHom I J n
        (derivedLocalCohomologyScalarMap I M (n + 1) a z) =
      a • localCohomologyToTorsionCocycleQuotientAddHom I J n z
    rw [← hα]
    change Abelian.Ext.{u} (ModuleCat.of R (R ⧸ I ^ k)) M (n + 1) at α
    exact (congrArg (localCohomologyToTorsionCocycleQuotientAddHom I J n)
      (derivedLocalCohomologyScalarMap_ι_apply I M (n + 1) a k α)).trans
        ((localCohomologyToTorsionCocycleQuotientAddHom_ι I J n k (a • α)).trans
          ((map_smul (extToTorsionCocycleQuotient I J n k) a α).trans
            (congrArg (fun z : torsionCocycleQuotient I J n => a • z)
              (localCohomologyToTorsionCocycleQuotientAddHom_ι I J n k α).symm)))

theorem localCohomologyToTorsionCocycleQuotient_surjective
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    Function.Surjective (localCohomologyToTorsionCocycleQuotient I J n)

theorem localCohomologyToTorsionCocycleQuotient_injective
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    Function.Injective (localCohomologyToTorsionCocycleQuotient I J n)

def derivedLocalCohomologyInjectiveComplexHomologyIsoSucc
    (I : Ideal R) (J : InjectiveResolution M) (n : ℕ) :
    (derivedLocalCohomologyInjectiveComplex I J).homology (n + 1) ≅
      derivedLocalCohomologyModule I M (n + 1)