From 93dbfe4228547710ad773a8bca4744174c9abc71 Mon Sep 17 00:00:00 2001
From: WuSH <2300017743@stu.pku.edu.cn>
Date: Sun, 6 Oct 2024 10:27:23 +0800
Subject: [PATCH] add GradedPiece for integers

---
 FilteredRing/graded.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean
index 3b0f1c1..60d066c 100644
--- a/FilteredRing/graded.lean
+++ b/FilteredRing/graded.lean
@@ -78,6 +78,29 @@ instance : DirectSum.GSemiring (GradedPiece F) where
   natCast_succ := sorry
 
 
+section integer
+
+variable (F : ℤ → AddSubgroup R) [fil : FilteredRing F] (i : ℤ)
+
+@[simp]
+theorem fil_Z (i : ℤ) : F_lt F i = F (i - 1) := by
+  dsimp [F_lt]
+  ext x
+  simp only [Iff.symm Int.le_sub_one_iff]
+  constructor
+  · exact fun hx ↦ (iSup_le fun k ↦ iSup_le fun hk ↦ fil.mono k hk) hx
+  · intro hx
+    have : F (i - 1) ≤ ⨆ k, ⨆ (_ : k ≤ i - 1), F k := by
+      apply le_iSup_of_le (i - 1)
+      simp only [le_refl, iSup_pos]
+    exact this hx
+
+@[simp]
+theorem GradedPiece_Z (i : ℤ) : GradedPiece F i = ((F i) ⧸ (F (i - 1)).addSubgroupOf (F i)) := by
+  simp only [GradedPiece, fil_Z]
+
+end integer
+
 /-
 variable [PredOrder ι]
 abbrev GradedPiece (i : ι) : Type u := (F i) ⧸ (F (Order.pred i)).addSubgroupOf (F i)