diff --git a/FilteredRing/filtered_category.lean b/FilteredRing/filtered_category.lean
index bb1ea79..8d039cf 100644
--- a/FilteredRing/filtered_category.lean
+++ b/FilteredRing/filtered_category.lean
@@ -8,41 +8,18 @@ open Pointwise CategoryTheory
 variable {R : Type u} {ι : Type v} [Ring R] [OrderedAddCommMonoid ι] {σ : Type o} [SetLike σ R]
   (F : ι → σ)
 
-structure FilteredModuleCat where
-  Mod : ModuleCat.{w, u} R
-  {σMod : Type*}
-  [instSetLike : SetLike σMod Mod.carrier]
-  [instAddSubmonoidClass : AddSubmonoidClass σMod Mod.carrier]
-  fil : ι → σMod
-  [f : FilteredModule F fil]
-
-attribute [instance] FilteredModuleCat.instSetLike FilteredModuleCat.instAddSubmonoidClass
-  FilteredModuleCat.f
-
-instance {M : FilteredModuleCat F} : IndexedModuleCat F where
-  Mod := M.Mod
-  σMod := M.σMod
-  instSetLike := M.instSetLike
-  instAddSubmonoidClass := M.instAddSubmonoidClass
-  fil := M.fil
-  f := {smul_mem := fun _ _ _ _ ha hb ↦ M.f.smul_mem ha hb}
+structure FilteredModuleCat extends IndexedModuleCat R ι where
+  [instFilteredModule : FilteredModule F ind]
 
 namespace FilteredModuleCat
 
-instance {M : FilteredModuleCat F} {i : ι} : AddSubmonoid M.Mod where
-  carrier := Set.range (AddSubmonoidClass.subtype (M.fil i))
-  add_mem' {a b} ha hb := by
-    rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq] at *
-    exact add_mem ha hb
-  zero_mem' := by
-    show 0 ∈ Set.range ⇑(AddSubmonoidClass.subtype (M.fil i))
-    rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq]
-    exact zero_mem (M.fil i)
+instance {M : FilteredModuleCat F} (i : ι) : AddSubmonoid M.Mod := IndexedModuleSubmonoid R ι i
 
+-- 并不容易直接用IndexedModuleCategory，可能需用forget functor? Not sure...
 instance filteredModuleCategory : Category (FilteredModuleCat F) where
   Hom M N := {f : M.Mod →ₗ[R] N.Mod //
-    ∀ i, f '' Set.range (AddSubmonoidClass.subtype (M.fil i))
-    ≤ Set.range (AddSubmonoidClass.subtype (N.fil i))}
+    ∀ i, f '' Set.range (AddSubmonoidClass.subtype (M.ind i))
+    ≤ Set.range (AddSubmonoidClass.subtype (N.ind i))}
   id _ := ⟨LinearMap.id, fun i ↦ by
     simp only [LinearMap.id_coe, id_eq, Set.image_id', le_refl]⟩
   comp f g := ⟨g.1.comp f.1, fun i ↦ by
@@ -54,9 +31,7 @@ instance filteredModuleCategory : Category (FilteredModuleCat F) where
   comp_id _ := rfl
   assoc _ _ _ := rfl
 
-instance {M N : FilteredModuleCat F} : FunLike (M ⟶ N) M.1 N.1 where
-  coe f := f.1.toFun
-  coe_injective' _ _ h := propext Subtype.val_inj |>.symm.mpr <| DFunLike.coe_injective' h
+instance {M N : FilteredModuleCat F} : FunLike (M ⟶ N) M.Mod N.Mod := IndexedModuleFunLike R ι
 
 instance filteredModuleConcreteCategory : ConcreteCategory (FilteredModuleCat F) where
   forget :=
@@ -73,14 +48,14 @@ def of {X : Type w} [AddCommGroup X] [Module R X] {σX : Type*} [SetLike σX X]
     Mod := ModuleCat.of R X
     σMod := σX
     instAddSubmonoidClass := by trivial
-    fil := filX
+    ind := filX
 
-instance {X : FilteredModuleCat F} : FilteredModule F X.fil := X.f
+instance {X : FilteredModuleCat F} : FilteredModule F X.ind := X.instFilteredModule
 
-@[simp] theorem of_coe (X : FilteredModuleCat F) : of F X.fil = X := rfl
+@[simp] theorem of_coe (X : FilteredModuleCat F) : of F X.ind = X := rfl
 
 @[simp] theorem coe_of (X : Type w) [AddCommGroup X] [Module R X] {σX : Type*} [SetLike σX X]
-  [AddSubmonoidClass σX X] (filX : ι → σX) [FilteredModule F filX] : (of F filX).1 = X := rfl
+  [AddSubmonoidClass σX X] (filX : ι → σX) [FilteredModule F filX] : (of F filX).Mod = X := rfl
 
 /-- A `LinearMap` with degree 0 is a morphism in `Module R`. -/
 def ofHom {X Y : Type w} {σX σY : Type o} [AddCommGroup X] [Module R X] [SetLike σX X]
@@ -103,16 +78,16 @@ theorem ofHom_apply {X Y : Type w} {σX σY : Type o} [AddCommGroup X] [Module R
 filtered module. -/
 -- Have no idea what ↑ means...
 @[simps]
-def ofSelfIso (M : FilteredModuleCat F) : of F M.fil ≅ M where
+def ofSelfIso (M : FilteredModuleCat F) : of F M.ind ≅ M where
   hom := 𝟙 M
   inv := 𝟙 M
 
 @[simp]
-theorem id_apply {M : FilteredModuleCat F} (m : M.1) : (𝟙 M : M.1 → M.1) m = m := rfl
+theorem id_apply {M : FilteredModuleCat F} (m : M.Mod) : (𝟙 M : M.Mod → M.Mod) m = m := rfl
 
 @[simp]
 theorem coe_comp {M N U : FilteredModuleCat F} (f : M ⟶ N) (g : N ⟶ U) :
-  (f ≫ g : M.1 → U.1) = g ∘ f := rfl
+  (f ≫ g : M.Mod → U.Mod) = g ∘ f := rfl
 
 -- instance : Inhabited (FilteredModuleCat F) := {
 --   default := {
@@ -122,75 +97,8 @@ theorem coe_comp {M N U : FilteredModuleCat F} (f : M ⟶ N) (g : N ⟶ U) :
 --   }
 -- }
 
-private instance {M N : FilteredModuleCat F} : AddSemigroup (M ⟶ N) where
-  add f g := ⟨f.1 + g.1, by
-    simp only [Set.le_eq_subset, Set.image_subset_iff]
-    intro i _ hx
-    have aux1 := f.2 i
-    have aux2 := g.2 i
-    simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.le_eq_subset,
-      Set.image_subset_iff, Set.preimage_setOf_eq] at *
-    exact add_mem (aux1 hx) (aux2 hx)⟩
-  add_assoc a b c := propext Subtype.val_inj |>.symm.mpr
-    <| add_assoc a.1 b.1 c.1
-
-private instance {M N : FilteredModuleCat F} : AddCommMonoid (M ⟶ N) where
-  zero := ⟨0, fun i ↦ by
-    simp only [Set.le_eq_subset]
-    repeat rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype]
-    rw [Set.image_subset_iff]
-    exact fun a _ ↦ zero_mem (N.fil i)⟩
-  zero_add a := propext Subtype.val_inj |>.symm.mpr
-    <| AddZeroClass.zero_add a.1
-  add_zero a := propext Subtype.val_inj |>.symm.mpr
-    <| AddZeroClass.add_zero a.1
-  nsmul k f := ⟨k • f.1, by
-    simp only [Set.le_eq_subset, Set.image_subset_iff]
-    intro i _ hx
-    have aux := f.2 i
-    simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
-      Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq] at *
-    exact nsmul_mem (aux hx) k⟩
-  nsmul_zero _ := by
-    simp only [Set.le_eq_subset, zero_smul]; rfl
-  nsmul_succ n x := propext Subtype.val_inj |>.symm.mpr
-    <| succ_nsmul x.1 n
-  add_comm f g := propext Subtype.val_inj |>.symm.mpr
-    <| AddCommMagma.add_comm f.1 g.1
-
-private instance {M N : FilteredModuleCat F} [AddSubgroupClass N.σMod N.Mod.carrier] :
-  SubNegMonoid (M ⟶ N) where
-  zsmul k f := ⟨k • f.1, by
-    simp only [Set.le_eq_subset, LinearMap.smul_apply, Set.image_subset_iff]
-    intro i _ hx
-    have aux := f.2 i
-    simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
-      Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq] at *
-    exact zsmul_mem (aux hx) k⟩
-  neg f := ⟨- f.1, by
-    simp only [Set.le_eq_subset, LinearMap.neg_apply, Set.image_subset_iff]
-    intro i _ hx
-    have aux := f.2 i
-    simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
-      Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq,
-      neg_mem_iff] at *
-    exact aux hx⟩
-  zsmul_zero' f := by
-    simp only [Set.le_eq_subset, zero_smul]; rfl
-  zsmul_succ' k f := by
-    rw [← Subtype.val_inj]
-    simp only [Nat.succ_eq_add_one, Int.ofNat_eq_coe, Nat.cast_one, Set.le_eq_subset, natCast_zsmul]
-    exact succ_nsmul f.1 k
-  zsmul_neg' k f := by
-    rw [← Subtype.val_inj]
-    simp only [Set.le_eq_subset, negSucc_zsmul, Nat.cast_add, Nat.cast_one, neg_inj]
-    norm_cast
-
 instance {M N : FilteredModuleCat F} [AddSubgroupClass N.σMod N.Mod.carrier] :
-  AddCommGroup (M ⟶ N) where
-  neg_add_cancel f := propext Subtype.val_inj |>.symm.mpr
-    <| neg_add_cancel f.1
-  add_comm := AddCommMagma.add_comm
+  AddCommGroup (M ⟶ N) := AddCommGroupMorphisms R ι
 
 instance (h : ∀ P : FilteredModuleCat F, AddSubgroupClass P.σMod P.Mod.carrier) :
   Preadditive (FilteredModuleCat F) where
@@ -209,8 +117,7 @@ private def proofGP (m : ModuleCat.{w, u} R) (i j : ι) (x : R) : AddSubmonoid m
     congrArg (Membership.mem (F' F m (j + i))) (smul_zero x) |>.mpr (F' F m (j + i)).zero_mem }
 
 open AddSubmonoid in
-instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F] :
-  FilteredModule F (F' F m) where
+instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F]: FilteredModule F (F' F m) where
   mono := fun hij ↦ by
     simp only [F', closure_le]
     rintro x ⟨r, ⟨hr, ⟨a, ha⟩⟩⟩
@@ -227,7 +134,7 @@ instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F] :
 open AddSubmonoid in
 def DeducedFunctor [FilteredRing F] : CategoryTheory.Functor (ModuleCat.{w, u} R)
   (FilteredModuleCat F) where
-    obj m := { Mod := m, fil := F' F m, f := toFilteredModule F m }
+    obj m := { Mod := m, ind := F' F m, instFilteredModule := toFilteredModule F m }
     map := fun {X Y} hom ↦ ⟨hom, by
       rintro i p ⟨x, ⟨hx1, hx2⟩⟩
       set toAddGP := (closure {x : Y.1 | ∃ r ∈ F i, ∃ a, x = r • a}).comap hom.toAddMonoidHom