Update

Blackfeather007 · Oct 5, 2024 · 37dedcb · 37dedcb
1 parent 96e563f
commit 37dedcb
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 10 deletions.
diff --git a/FilteredRing/Basic.lean b/FilteredRing/Basic.lean
@@ -6,7 +6,7 @@ open Pointwise
 
 variable {R : Type u} {ι : Type v} [Ring R] [OrderedAddCommMonoid ι] [DecidableEq ι]
 
-class FilteredRing (F : ι → AddSubgroup R)where
+class FilteredRing (F : ι → AddSubgroup R) where
   mono : ∀ i ≤ j, F i ≤ F j
   one : 1 ∈ F 0
   mul_mem : ∀ i j : ι, (F i : Set R) * F j ≤ F (i + j)

diff --git a/FilteredRing/category.lean b/FilteredRing/category.lean
@@ -7,19 +7,21 @@ variable (F : ι → AddSubgroup R)
 
 
 structure FilModCat where
-  M : ModuleCat R
+  Mod : ModuleCat R
   -- carrier : Type v
   -- [isAddCommGroup : AddCommGroup carrier]
   -- [isModule : Module R carrier]
-  fil : ι → Submodule R M
-  [f :FilteredModule F M fil]
+  fil : ι → Submodule R Mod
+  [f : FilteredModule F Mod fil]
   -- mono : ∀ i ≤ j, fil i ≤ fil j
   -- smul_mem : ∀ i j, (F i : Set R) • fil j ≤ fil (i + j)
 
 instance : Category (FilModCat R F) where
-  Hom := sorry
-  id := sorry
-  comp := sorry
-  id_comp := sorry
-  comp_id := sorry
-  assoc := sorry
+  Hom M N := {f : M.Mod →ₗ[R] N.Mod // ∀ i, f '' M.fil i ≤ N.fil i}
+  id _ := ⟨LinearMap.id, by intro i; simp⟩
+  comp f g := ⟨g.1.comp f.1, by
+    intro i
+    sorry⟩
+  id_comp _ := rfl
+  comp_id _ := rfl
+  assoc f g h := rfl