Merge branch 'main' of https://github.com/Blackfeather007/Filtered_Ring

Blackfeather007 · Oct 5, 2024 · 96e563f · 96e563f
2 parents 1c52357 + 1f251dd
commit 96e563f
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean
@@ -7,7 +7,9 @@ variable {ι : Type v} [OrderedAddCommMonoid ι] [DecidableEq ι] [PredOrder ι]
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
 
+instance {i : ι}: F (PredOrder.pred i) ≤ F i :=
+  FilteredRing.mono (PredOrder.pred i) (PredOrder.pred_le i)
 
-def gradedMap (F : ι → AddSubgroup R) [FilteredRing F] : ι → AddSubgroup R := sorry
+def gradedMap {i : ι} : Module R ((F i) ⧸ (F (PredOrder.pred i)).addSubgroupOf (F i)) := sorry
 
-instance : GradedRing (gradedMap F) := sorry
+-- instance : GradedRing (gradedMap F) := sorry