refactor(Algebra/Homology/ShortComplex/ModuleCat, RepresentationTheory/GroupCohomology/*): unfold CategoryTheory.ShortComplex.moduleCatLeftHomologyData less eagerly (#24696)

`ShortComplex.moduleCatLeftHomologyData` represents the homology of a short complex in `ModuleCat` as a concrete quotient of a `LinearMap.ker` by a `LinearMap.range`. When working on the level of linear maps - i.e. `ModuleCat.Hom.hom` of a morphism in `ModuleCat` - simp lemmas unfolding this concrete definition are useful. But when reasoning about morphisms in `ModuleCat` it seems handy not to unfold the definition, so that `simp` can apply the general `LeftHomologyData` API.

To that end, this PR replaces simp lemmas `ShortComplex.moduleCatLeftHomologyData_i, ShortComplex.moduleCatLeftHomologyData_π` with their linear map versions, `ShortComplex.moduleCatLeftHomologyData_i_hom, ShortComplex.moduleCatLeftHomologyData_π_hom`. 
It also rephrases declarations about `ModuleCat` morphisms in the group cohomology folder in terms of `ShortComplex.moduleCatLeftHomologyData` rather than unfolding.

Deletions:
- CategoryTheory.ShortComplex.moduleCatHomology
- CategoryTheory.ShortComplex.moduleCatHomologyπ
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π
- CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'



Co-authored-by: 101damnations <al3717@ic.ac.uk>

Author: Amelia Livingston

Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

@@ -95,83 +95,102 @@ def moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g.hom where
   map_add' x y := by aesop
   map_smul' a x := by aesop
 
-/-- The homology of `S`, defined as the quotient of the kernel of `S.g` by
-the image of `S.moduleCatToCycles` -/
-abbrev moduleCatHomology :=
-  ModuleCat.of R (LinearMap.ker S.g.hom ⧸ LinearMap.range S.moduleCatToCycles)
-
-/-- The canonical map `ModuleCat.of R (LinearMap.ker S.g) ⟶ S.moduleCatHomology`. -/
-abbrev moduleCatHomologyπ : ModuleCat.of R (LinearMap.ker S.g.hom) ⟶ S.moduleCatHomology :=
-  ModuleCat.ofHom (LinearMap.range S.moduleCatToCycles).mkQ
-
 /-- The explicit left homology data of a short complex of modules that is
-given by a kernel and a quotient given by the `LinearMap` API. -/
-@[simps K H i π]
+given by a kernel and a quotient given by the `LinearMap` API. The projections to `K` and `H` are
+not simp lemmas because the generic lemmas about `LeftHomologyData` are more useful here. -/
+@[simps! i_hom π_hom, simps! -isSimp K H]
 def moduleCatLeftHomologyData : S.LeftHomologyData where
   K := ModuleCat.of R (LinearMap.ker S.g.hom)
-  H := S.moduleCatHomology
+  H := ModuleCat.of R (LinearMap.ker S.g.hom ⧸ LinearMap.range S.moduleCatToCycles)
   i := ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype
-  π := S.moduleCatHomologyπ
+  π := ModuleCat.ofHom (LinearMap.range S.moduleCatToCycles).mkQ
   wi := by aesop
   hi := ModuleCat.kernelIsLimit _
   wπ := by aesop
   hπ := ModuleCat.cokernelIsColimit (ModuleCat.ofHom S.moduleCatToCycles)
 
+/-- The homology of a short complex of modules as a concrete quotient. -/
+@[deprecated "This abbreviation is now inlined" (since := "2025-05-14")]
+abbrev moduleCatHomology := S.moduleCatLeftHomologyData.H
+
+/-- The natural projection map to the homology of a short complex of modules as a
+concrete quotient. -/
+@[deprecated "This abbreviation is now inlined" (since := "2025-05-14")]
+abbrev moduleCatHomologyπ := S.moduleCatLeftHomologyData.π
+
+@[deprecated (since := "2025-05-09")]
+alias moduleCatLeftHomologyData_i := moduleCatLeftHomologyData_i_hom
+
+@[deprecated (since := "2025-05-09")]
+alias moduleCatLeftHomologyData_π := moduleCatLeftHomologyData_π_hom
+
 @[simp]
-lemma moduleCatLeftHomologyData_f' :
-    S.moduleCatLeftHomologyData.f' = ModuleCat.ofHom S.moduleCatToCycles := rfl
+lemma moduleCatLeftHomologyData_f'_hom :
+    S.moduleCatLeftHomologyData.f'.hom = S.moduleCatToCycles := rfl
 
-instance : Epi S.moduleCatHomologyπ :=
-  (inferInstance : Epi S.moduleCatLeftHomologyData.π)
+@[deprecated (since := "2025-05-09")]
+alias moduleCatLeftHomologyData_f' := moduleCatLeftHomologyData_f'_hom
+
+@[simp]
+lemma moduleCatLeftHomologyData_descH_hom {M : ModuleCat R}
+    (φ : S.moduleCatLeftHomologyData.K ⟶ M) (h : S.moduleCatLeftHomologyData.f' ≫ φ = 0) :
+    (S.moduleCatLeftHomologyData.descH φ h).hom =
+      (LinearMap.range <| ModuleCat.Hom.hom _).liftQ
+         φ.hom (LinearMap.range_le_ker_iff.2 <| ModuleCat.hom_ext_iff.1 h) := rfl
+
+@[simp]
+lemma moduleCatLeftHomologyData_liftK_hom {M : ModuleCat R} (φ : M ⟶ S.X₂) (h : φ ≫ S.g = 0) :
+    (S.moduleCatLeftHomologyData.liftK φ h).hom =
+      φ.hom.codRestrict (LinearMap.ker S.g.hom) (fun m => congr($h m)) := rfl
 
 /-- Given a short complex `S` of modules, this is the isomorphism between
 the abstract `S.cycles` of the homology API and the more concrete description as
 `LinearMap.ker S.g`. -/
-noncomputable def moduleCatCyclesIso : S.cycles ≅ ModuleCat.of R (LinearMap.ker S.g.hom) :=
+noncomputable def moduleCatCyclesIso : S.cycles ≅ S.moduleCatLeftHomologyData.K :=
   S.moduleCatLeftHomologyData.cyclesIso
 
 @[reassoc (attr := simp, elementwise)]
-lemma moduleCatCyclesIso_hom_subtype :
-    S.moduleCatCyclesIso.hom ≫ ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype = S.iCycles :=
+lemma moduleCatCyclesIso_hom_i :
+    S.moduleCatCyclesIso.hom ≫ S.moduleCatLeftHomologyData.i = S.iCycles :=
   S.moduleCatLeftHomologyData.cyclesIso_hom_comp_i
 
+@[deprecated (since := "2025-05-09")]
+alias moduleCatCyclesIso_hom_subtype := moduleCatCyclesIso_hom_i
+
 @[reassoc (attr := simp, elementwise)]
 lemma moduleCatCyclesIso_inv_iCycles :
-    S.moduleCatCyclesIso.inv ≫ S.iCycles = ModuleCat.ofHom (LinearMap.ker S.g.hom).subtype :=
+    S.moduleCatCyclesIso.inv ≫ S.iCycles = S.moduleCatLeftHomologyData.i :=
   S.moduleCatLeftHomologyData.cyclesIso_inv_comp_iCycles
 
 @[reassoc (attr := simp, elementwise)]
 lemma toCycles_moduleCatCyclesIso_hom :
-    S.toCycles ≫ S.moduleCatCyclesIso.hom = ModuleCat.ofHom S.moduleCatToCycles := by
-  rw [← cancel_mono S.moduleCatLeftHomologyData.i, moduleCatLeftHomologyData_i,
-    Category.assoc, S.moduleCatCyclesIso_hom_subtype, toCycles_i]
-  rfl
+    S.toCycles ≫ S.moduleCatCyclesIso.hom = S.moduleCatLeftHomologyData.f' := by
+  simp [← cancel_mono S.moduleCatLeftHomologyData.i]
 
 /-- Given a short complex `S` of modules, this is the isomorphism between
 the abstract `S.homology` of the homology API and the more explicit
 quotient of `LinearMap.ker S.g` by the image of
 `S.moduleCatToCycles : S.X₁ →ₗ[R] LinearMap.ker S.g`. -/
 noncomputable def moduleCatHomologyIso :
-    S.homology ≅ S.moduleCatHomology :=
+    S.homology ≅ S.moduleCatLeftHomologyData.H :=
   S.moduleCatLeftHomologyData.homologyIso
 
 @[reassoc (attr := simp, elementwise)]
 lemma π_moduleCatCyclesIso_hom :
     S.homologyπ ≫ S.moduleCatHomologyIso.hom =
-      S.moduleCatCyclesIso.hom ≫ S.moduleCatHomologyπ :=
+      S.moduleCatCyclesIso.hom ≫ S.moduleCatLeftHomologyData.π :=
   S.moduleCatLeftHomologyData.homologyπ_comp_homologyIso_hom
 
 @[reassoc (attr := simp, elementwise)]
 lemma moduleCatCyclesIso_inv_π :
     S.moduleCatCyclesIso.inv ≫ S.homologyπ =
-       S.moduleCatHomologyπ ≫ S.moduleCatHomologyIso.inv :=
+       S.moduleCatLeftHomologyData.π ≫ S.moduleCatHomologyIso.inv :=
   S.moduleCatLeftHomologyData.π_comp_homologyIso_inv
 
 lemma exact_iff_surjective_moduleCatToCycles :
     S.Exact ↔ Function.Surjective S.moduleCatToCycles := by
-  rw [S.moduleCatLeftHomologyData.exact_iff_epi_f', moduleCatLeftHomologyData_f',
-    ModuleCat.epi_iff_surjective]
-  rfl
+  simp [S.moduleCatLeftHomologyData.exact_iff_epi_f',
+    ModuleCat.epi_iff_surjective, moduleCatLeftHomologyData_K]
 
 end ShortComplex
 

Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean

@@ -194,6 +194,12 @@ theorem H0Map_id_eq_invariantsFunctor_map {A B : Rep k G} (f : A ⟶ B) :
     H0Map (MonoidHom.id G) f = (invariantsFunctor k G).map f := by
   rfl
 
+@[reassoc (attr := simp), elementwise (attr := simp)]
+lemma H0Map_comp_f :
+    H0Map f φ ≫ (shortComplexH0 B).f = (shortComplexH0 A).f ≫ φ.hom := by
+  ext
+  simp [shortComplexH0]
+
 instance mono_H0Map_of_mono {A B : Rep k G} (f : A ⟶ B) [Mono f] :
     Mono (H0Map (MonoidHom.id G) f) :=
   (ModuleCat.mono_iff_injective _).2 fun _ _ hxy => Subtype.ext <|
@@ -202,10 +208,8 @@ instance mono_H0Map_of_mono {A B : Rep k G} (f : A ⟶ B) [Mono f] :
 @[reassoc (attr := simp), elementwise (attr := simp)]
 theorem cocyclesMap_comp_isoZeroCocycles_hom :
     cocyclesMap f φ 0 ≫ (isoZeroCocycles B).hom = (isoZeroCocycles A).hom ≫ H0Map f φ := by
-  rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq, ← cancel_mono (iCocycles _ _)]
-  ext x
-  have := congr($((CommSq.vert_inv ⟨cochainsMap_f_0_comp_zeroCochainsLequiv f φ⟩).w.symm) x)
-  simp_all
+  have := cochainsMap_f_0_comp_zeroCochainsLequiv f φ
+  simp_all [← cancel_mono (shortComplexH0 B).f]
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 theorem map_comp_isoH0_hom :
@@ -259,19 +263,20 @@ noncomputable abbrev mapOneCocycles :
   ShortComplex.cyclesMap' (mapShortComplexH1 f φ) (shortComplexH1 A).moduleCatLeftHomologyData
     (shortComplexH1 B).moduleCatLeftHomologyData
 
-@[reassoc (attr := simp), elementwise (attr := simp)]
-lemma mapOneCocycles_comp_subtype :
-    mapOneCocycles f φ ≫ ModuleCat.ofHom (oneCocycles B).subtype =
-      ModuleCat.ofHom (oneCocycles A).subtype ≫ ModuleCat.ofHom (fOne f φ) :=
-  ShortComplex.cyclesMap'_i (mapShortComplexH1 f φ) (moduleCatLeftHomologyData _)
-    (moduleCatLeftHomologyData _)
+@[reassoc, elementwise]
+lemma mapOneCocycles_comp_i :
+    mapOneCocycles f φ ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i =
+      (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ ModuleCat.ofHom (fOne f φ) := by
+  simp
+
+@[deprecated (since := "2025-05-09")]
+alias mapOneCocycles_comp_subtype := mapOneCocycles_comp_i
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma cocyclesMap_comp_isoOneCocycles_hom :
     cocyclesMap f φ 1 ≫ (isoOneCocycles B).hom = (isoOneCocycles A).hom ≫ mapOneCocycles f φ := by
-  simp_rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapOneCocycles,
-      Category.assoc, cyclesMap'_i, isoOneCocycles, ← Category.assoc]
-  simp [cochainsMap_f_1_comp_oneCochainsLequiv f, mapShortComplexH1, ← LinearEquiv.toModuleIso_hom]
+  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, mapShortComplexH1,
+    cochainsMap_f_1_comp_oneCochainsLequiv f, ← LinearEquiv.toModuleIso_hom]
 
 /-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
 this is induced map `H¹(H, A) ⟶ H¹(G, B)`. -/
@@ -296,10 +301,10 @@ theorem H1Map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
     H1Map (MonoidHom.id G) (φ ≫ ψ) = H1Map (MonoidHom.id G) φ ≫ H1Map (MonoidHom.id G) ψ :=
   H1Map_comp (MonoidHom.id G) (MonoidHom.id G) _ _
 
-@[reassoc (attr := simp), elementwise (attr := simp)]
+@[reassoc, elementwise]
 lemma H1π_comp_H1Map :
-    H1π A ≫ H1Map f φ = mapOneCocycles f φ ≫ H1π B :=
-  leftHomologyπ_naturality' (mapShortComplexH1 f φ) _ _
+    H1π A ≫ H1Map f φ = mapOneCocycles f φ ≫ H1π B := by
+  simp
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma map_comp_isoH1_hom :
@@ -353,19 +358,20 @@ noncomputable abbrev mapTwoCocycles :
   ShortComplex.cyclesMap' (mapShortComplexH2 f φ) (shortComplexH2 A).moduleCatLeftHomologyData
     (shortComplexH2 B).moduleCatLeftHomologyData
 
-@[reassoc (attr := simp), elementwise (attr := simp)]
-lemma mapTwoCocycles_comp_subtype :
-    mapTwoCocycles f φ ≫ ModuleCat.ofHom (twoCocycles B).subtype =
-      ModuleCat.ofHom (twoCocycles A).subtype ≫ ModuleCat.ofHom (fTwo f φ) :=
-  ShortComplex.cyclesMap'_i (mapShortComplexH2 f φ) (moduleCatLeftHomologyData _)
-    (moduleCatLeftHomologyData _)
+@[reassoc, elementwise]
+lemma mapTwoCocycles_comp_i :
+    mapTwoCocycles f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
+      (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ ModuleCat.ofHom (fTwo f φ) := by
+  simp
+
+@[deprecated (since := "2025-05-09")]
+alias mapTwoCocycles_comp_subtype := mapTwoCocycles_comp_i
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma cocyclesMap_comp_isoTwoCocycles_hom :
     cocyclesMap f φ 2 ≫ (isoTwoCocycles B).hom = (isoTwoCocycles A).hom ≫ mapTwoCocycles f φ := by
-  simp_rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapTwoCocycles,
-      Category.assoc, cyclesMap'_i, isoTwoCocycles, ← Category.assoc]
-  simp [cochainsMap_f_2_comp_twoCochainsLequiv f, mapShortComplexH2, ← LinearEquiv.toModuleIso_hom]
+  simp [← cancel_mono (moduleCatLeftHomologyData (shortComplexH2 B)).i, mapShortComplexH2,
+    cochainsMap_f_2_comp_twoCochainsLequiv f, ← LinearEquiv.toModuleIso_hom]
 
 /-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
 this is induced map `H²(H, A) ⟶ H²(G, B)`. -/
@@ -390,10 +396,10 @@ theorem H2Map_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
     H2Map (MonoidHom.id G) (φ ≫ ψ) = H2Map (MonoidHom.id G) φ ≫ H2Map (MonoidHom.id G) ψ :=
   H2Map_comp (MonoidHom.id G) (MonoidHom.id G) _ _
 
-@[reassoc (attr := simp), elementwise (attr := simp)]
+@[reassoc, elementwise]
 lemma H2π_comp_H2Map :
-    H2π A ≫ H2Map f φ = mapTwoCocycles f φ ≫ H2π B :=
-  leftHomologyπ_naturality' (mapShortComplexH2 f φ) _ _
+    H2π A ≫ H2Map f φ = mapTwoCocycles f φ ≫ H2π B := by
+  simp
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma map_comp_isoH2_hom :

Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

@@ -703,10 +703,11 @@ abbrev H0 := ModuleCat.of k A.ρ.invariants
 /-- We define the 1st group cohomology of a `k`-linear `G`-representation `A`, `H¹(G, A)`, to be
 1-cocycles (i.e. `Z¹(G, A) := Ker(d¹ : Fun(G, A) → Fun(G², A)`) modulo 1-coboundaries
 (i.e. `B¹(G, A) := Im(d⁰: A → Fun(G, A))`). -/
-abbrev H1 := (shortComplexH1 A).moduleCatHomology
+abbrev H1 := (shortComplexH1 A).moduleCatLeftHomologyData.H
 
 /-- The quotient map `Z¹(G, A) → H¹(G, A).` -/
-abbrev H1π : ModuleCat.of k (oneCocycles A) ⟶ H1 A := (shortComplexH1 A).moduleCatHomologyπ
+abbrev H1π : ModuleCat.of k (oneCocycles A) ⟶ H1 A :=
+  (shortComplexH1 A).moduleCatLeftHomologyData.π
 
 variable {A} in
 lemma H1π_eq_zero_iff (x : oneCocycles A) : H1π A x = 0 ↔ ⇑x ∈ oneCoboundaries A := by
@@ -716,10 +717,11 @@ lemma H1π_eq_zero_iff (x : oneCocycles A) : H1π A x = 0 ↔ ⇑x ∈ oneCoboun
 /-- We define the 2nd group cohomology of a `k`-linear `G`-representation `A`, `H²(G, A)`, to be
 2-cocycles (i.e. `Z²(G, A) := Ker(d² : Fun(G², A) → Fun(G³, A)`) modulo 2-coboundaries
 (i.e. `B²(G, A) := Im(d¹: Fun(G, A) → Fun(G², A))`). -/
-abbrev H2 := (shortComplexH2 A).moduleCatHomology
+abbrev H2 := (shortComplexH2 A).moduleCatLeftHomologyData.H
 
 /-- The quotient map `Z²(G, A) → H²(G, A).` -/
-abbrev H2π : ModuleCat.of k (twoCocycles A) ⟶ H2 A := (shortComplexH2 A).moduleCatHomologyπ
+abbrev H2π : ModuleCat.of k (twoCocycles A) ⟶ H2 A :=
+  (shortComplexH2 A).moduleCatLeftHomologyData.π
 
 variable {A} in
 lemma H2π_eq_zero_iff (x : twoCocycles A) : H2π A x = 0 ↔ ⇑x ∈ twoCoboundaries A := by
@@ -802,17 +804,20 @@ def isoZeroCocycles : cocycles A 0 ≅ H0 A :=
       (dZeroArrowIso A)
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma isoZeroCocycles_hom_comp_subtype :
-    (isoZeroCocycles A).hom ≫ ModuleCat.ofHom A.ρ.invariants.subtype =
+lemma isoZeroCocycles_hom_comp_f :
+    (isoZeroCocycles A).hom ≫ (shortComplexH0 A).f =
       iCocycles A 0 ≫ (zeroCochainsLequiv A).toModuleIso.hom := by
   dsimp [isoZeroCocycles]
   apply KernelFork.mapOfIsLimit_ι
 
+@[deprecated (since := "2025-05-09")]
+alias isoZeroCocycles_hom_comp_subtype := isoZeroCocycles_hom_comp_f
+
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma isoZeroCocycles_inv_comp_iCocycles :
     (isoZeroCocycles A).inv ≫ iCocycles A 0 =
-        ModuleCat.ofHom A.ρ.invariants.subtype ≫ (zeroCochainsLequiv A).toModuleIso.inv := by
-  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, isoZeroCocycles_hom_comp_subtype]
+      (shortComplexH0 A).f ≫ (zeroCochainsLequiv A).toModuleIso.inv := by
+  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, isoZeroCocycles_hom_comp_f]
 
 /-- The 0th group cohomology of `A`, defined as the 0th cohomology of the complex of inhomogeneous
 cochains, is isomorphic to the invariants of the representation on `A`. -/
@@ -844,17 +849,19 @@ def isoOneCocycles : cocycles A 1 ≅ ModuleCat.of k (oneCocycles A) :=
     cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma isoOneCocycles_hom_comp_subtype :
-    (isoOneCocycles A).hom ≫ ModuleCat.ofHom (oneCocycles A).subtype =
+lemma isoOneCocycles_hom_comp_i :
+    (isoOneCocycles A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.i =
       iCocycles A 1 ≫ (oneCochainsLequiv A).toModuleIso.hom := by
-  have := (shortComplexH1 A).moduleCatCyclesIso_hom_subtype
-  simp_all [shortComplexH1, isoOneCocycles, oneCocycles]
+  simp [shortComplexH1, isoOneCocycles, oneCocycles]
+
+@[deprecated (since := "2025-05-09")]
+alias isoOneCocycles_hom_comp_subtype := isoOneCocycles_hom_comp_i
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma toCocycles_comp_isoOneCocycles_hom :
     toCocycles A 0 1 ≫ (isoOneCocycles A).hom =
       (zeroCochainsLequiv A).toModuleIso.hom ≫
-        ModuleCat.ofHom (shortComplexH1 A).moduleCatToCycles := by
+      (shortComplexH1 A).moduleCatLeftHomologyData.f' := by
   simp [isoOneCocycles]
 
 /-- The 1st group cohomology of `A`, defined as the 1st cohomology of the complex of inhomogeneous
@@ -889,17 +896,18 @@ def isoTwoCocycles : cocycles A 2 ≅ ModuleCat.of k (twoCocycles A) :=
     cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
-lemma isoTwoCocycles_hom_comp_subtype :
-    (isoTwoCocycles A).hom ≫ ModuleCat.ofHom (twoCocycles A).subtype =
+lemma isoTwoCocycles_hom_comp_i :
+    (isoTwoCocycles A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.i =
       iCocycles A 2 ≫ (twoCochainsLequiv A).toModuleIso.hom := by
-  have := (shortComplexH2 A).moduleCatCyclesIso_hom_subtype
-  simp_all [shortComplexH2, isoTwoCocycles, twoCocycles]
+  simp [shortComplexH2, isoTwoCocycles, twoCocycles]
+
+@[deprecated (since := "2025-05-09")]
+alias isoTwoCocycles_hom_comp_subtype := isoTwoCocycles_hom_comp_i
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma toCocycles_comp_isoTwoCocycles_hom :
     toCocycles A 1 2 ≫ (isoTwoCocycles A).hom =
-      (oneCochainsLequiv A).toModuleIso.hom ≫
-        ModuleCat.ofHom (shortComplexH2 A).moduleCatToCycles := by
+      (oneCochainsLequiv A).toModuleIso.hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f' := by
   simp [isoTwoCocycles]
 
 /-- The 2nd group cohomology of `A`, defined as the 2nd cohomology of the complex of inhomogeneous