From 1f251ddc9395123c905e5d0081afda3d951fe0c6 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 5 Oct 2024 15:41:33 +0800 Subject: [PATCH] Update graded.lean --- FilteredRing/graded.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean index 9d94970..1e22c5f 100644 --- 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