InjectiveResolutionExtLinear.lean

def injectiveResolutionLinearCoyonedaComplex
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) :
    CochainComplex (ModuleCat.{u} R) ℕ

def injectiveResolutionLinearCoyonedaShortComplexSucc
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ) :
    ShortComplex (ModuleCat.{u} R)

theorem injectiveResolution_extMk_smul
    (J : InjectiveResolution M) {X : ModuleCat.{u} R} {n : ℕ}
    (f : X ⟶ J.cocomplex.X n) (m : ℕ) (hm : n + 1 = m)
    (hf : f ≫ J.cocomplex.d n m = 0) (a : R) :
    J.extMk (a • f) m hm (by
      rw [Linear.smul_comp, hf, smul_zero]) =
      a • J.extMk f m hm hf := by
  have h := J.mk₀_comp_extMk f m hm hf (a • 𝟙 X)
  simpa only [Linear.smul_comp, Category.id_comp,
    Abelian.Ext.mk₀_smul, Abelian.Ext.smul_comp,
    Abelian.Ext.mk₀_id_comp] using h.symm

def injectiveResolutionCyclesToExtSucc
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ) :
    LinearMap.ker
        (injectiveResolutionLinearCoyonedaShortComplexSucc J X n).g.hom →ₗ[R]
      Abelian.Ext.{u} X M (n + 1) where
  toFun f := J.extMk f.1 (n + 2) (by omega) (by
    change f.1 ≫ J.cocomplex.d (n + 1) (n + 2) = 0
    exact f.2)
  map_add' f g := (J.add_extMk f.1 g.1 (n + 2) (by omega) f.2 g.2).symm
  map_smul' a f := injectiveResolution_extMk_smul J f.1 (n + 2) (by omega) f.2 a

theorem injectiveResolutionCyclesToExtSucc_surjective
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ) :
    Function.Surjective (injectiveResolutionCyclesToExtSucc J X n)

theorem injectiveResolutionCyclesToExtSucc_ker_eq_range
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ) :
    LinearMap.ker (injectiveResolutionCyclesToExtSucc J X n) =
      LinearMap.range
        (injectiveResolutionLinearCoyonedaShortComplexSucc J X n).moduleCatToCycles

def injectiveResolutionCocycleQuotientEquivExtSucc
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ) :
    ((LinearMap.ker
        (injectiveResolutionLinearCoyonedaShortComplexSucc J X n).g.hom) ⧸
      LinearMap.range
        (injectiveResolutionLinearCoyonedaShortComplexSucc J X n).moduleCatToCycles) ≃ₗ[R]
      Abelian.Ext.{u} X M (n + 1)

theorem injectiveResolutionCocycleQuotientEquivExtSucc_apply_mk
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ)
    (f : LinearMap.ker
      (injectiveResolutionLinearCoyonedaShortComplexSucc J X n).g.hom) :
    injectiveResolutionCocycleQuotientEquivExtSucc J X n (Submodule.Quotient.mk f) =
      J.extMk f.1 (n + 2) (by omega) f.2 :=
  rfl

theorem injectiveResolutionCocycleQuotientEquivExtSucc_symm_extMk
    (J : InjectiveResolution M) (X : ModuleCat.{u} R) (n : ℕ)
    (f : X ⟶ J.cocomplex.X (n + 1))
    (hf : f ≫ J.cocomplex.d (n + 1) (n + 2) = 0) :
    (injectiveResolutionCocycleQuotientEquivExtSucc J X n).symm
        (J.extMk f (n + 2) (by omega) hf) =
      Submodule.Quotient.mk ⟨f, hf⟩ :=
  (injectiveResolutionCocycleQuotientEquivExtSucc J X n).symm_apply_apply
    (Submodule.Quotient.mk ⟨f, hf⟩)