From 9e810c61c91b4deb7d99652b577f74adaef3910f Mon Sep 17 00:00:00 2001
From: Suzuka Yu <109365723+Yu-Misaka@users.noreply.github.com>
Date: Sun, 27 Oct 2024 15:35:49 +0800
Subject: [PATCH] =?UTF-8?q?Rebase=20filtered=F0=9F=90=B1=20(not=20elegant?=
 =?UTF-8?q?=20though...)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 FilteredRing/filtered_category.lean | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

diff --git a/FilteredRing/filtered_category.lean b/FilteredRing/filtered_category.lean
index 8d039cf..8ba3a7a 100644
--- a/FilteredRing/filtered_category.lean
+++ b/FilteredRing/filtered_category.lean
@@ -15,18 +15,10 @@ namespace FilteredModuleCat
 
 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.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
-    have aux1 := f.2 i
-    have aux2 := g.2 i
-    simp only [Set.le_eq_subset, Set.image_subset_iff] at *
-    exact fun _ hx ↦ aux2 <| aux1 hx⟩
+  Hom M N := (IndexedModuleCategory R ι).Hom M.toIndexedModuleCat N.toIndexedModuleCat
+  id M := (IndexedModuleCategory R ι).id M.toIndexedModuleCat
+  comp := (IndexedModuleCategory R ι).comp
   id_comp _ := rfl
   comp_id _ := rfl
   assoc _ _ _ := rfl