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

FilteredRing/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib
 
-universe u v
+universe u v w
 
 variable {R : Type u} {ι : Type v} [Ring R] [OrderedAddCommMonoid ι]
 
@@ -10,7 +10,7 @@ class FilteredRing (F : ι → AddSubgroup R) where
   mul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F j → x * y ∈ F (i + j)
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
-variable (M : Type u) [AddCommGroup M] [Module R M]
+variable (M : Type w) [AddCommGroup M] [Module R M]
 
 class FilteredModule (F' : ι → Submodule R M) where
   mono : ∀ i ≤ j, F' i ≤ F' j

FilteredRing/category.lean

@@ -1,11 +1,14 @@
 import FilteredRing.Basic
+
+universe u v w
+
 open Pointwise CategoryTheory
 
 variable (R : Type u) {ι : Type v} [Ring R] [OrderedAddCommMonoid ι]
 variable (F : ι → AddSubgroup R)
 
 structure FilModCat where
-  Mod : ModuleCat R
+  Mod : ModuleCat.{w, u} R
   fil : ι → Submodule R Mod
   [f : FilteredModule F Mod fil]
 
@@ -153,3 +156,7 @@ instance FilModCat.HomAddCommGroup {M N : FilModCat R F} : AddCommGroup (M ⟶ N
 instance : Preadditive (FilModCat R F) where
   add_comp P Q R f f' g := by
     exact propext Subtype.val_inj |>.symm.mpr <| LinearMap.comp_add f.1 f'.1 g.1
+
+-- instance : CategoryTheory.Functor (ModuleCat.{w, u} R) (FilModCat R F) where
+--   obj m := by
+--     have := m.3

FilteredRing/graded.lean

@@ -36,6 +36,21 @@ lemma Filtration.flt_mul_mem {i j : ι} {x y} (hx : x ∈ F_lt F i) (hy : y ∈
     rw [add_mul]
     exact add_mem ih₁ ih₂
 
+variable {F} in
+lemma Filtration.flt_mul_mem' {i j : ι} {x y} (hx : x ∈ F_lt F i) (hy : y ∈ F j) :
+    x * y ∈ F_lt F (i + j) := by
+  let S : AddSubgroup R := {
+    carrier := {x | x * y ∈ F_lt F (i + j) }
+    add_mem' := fun hu hv ↦ by simp only [Set.mem_setOf_eq, add_mul , add_mem hu.out hv.out]
+    zero_mem' := by simp only [Set.mem_setOf_eq, zero_mul, zero_mem]
+    neg_mem' := by simp only [Set.mem_setOf_eq, neg_mul, neg_mem_iff, imp_self, implies_true] }
+  have : F_lt F i ≤ S := by
+    simp only [F_lt, iSup_le_iff]
+    intro a ha b hb
+    have le : F (a + j) ≤ F_lt F (i + j) := le_biSup F (add_lt_add_right ha j)
+    exact le (FilteredRing.mul_mem hb hy)
+  exact this hx
+
 variable {F} in
 lemma Filtration.mul_flt_mem {i j : ι} {x y} (hx : x ∈ F i) (hy : y ∈ F_lt F j) :
     x * y ∈ F_lt F (i + j) := by
@@ -50,6 +65,21 @@ lemma Filtration.mul_flt_mem {i j : ι} {x y} (hx : x ∈ F i) (hy : y ∈ F_lt
     rw [mul_add]
     exact add_mem ih₁ ih₂
 
+variable {F} in
+lemma Filtration.mul_flt_mem' {i j : ι} {x y} (hx : x ∈ F i) (hy : y ∈ F_lt F j) :
+    x * y ∈ F_lt F (i + j) := by
+  let S : AddSubgroup R := {
+    carrier := {y | x * y ∈ F_lt F (i + j) }
+    add_mem' := fun hu hv ↦ by simp only [Set.mem_setOf_eq, mul_add , add_mem hu.out hv.out]
+    zero_mem' := by simp only [Set.mem_setOf_eq, mul_zero, zero_mem]
+    neg_mem' := by simp only [Set.mem_setOf_eq, mul_neg, neg_mem_iff, imp_self, implies_true] }
+  have : F_lt F j ≤ S := by
+    simp only [F_lt, iSup_le_iff]
+    intro a ha b hb
+    have le : F (i + a) ≤ F_lt F (i + j) := le_biSup F (add_lt_add_left ha i)
+    exact le (FilteredRing.mul_mem hx hb)
+  exact this hy
+
 def gradedMul {i j : ι} : GradedPiece F i → GradedPiece F j → GradedPiece F (i + j) := by
   intro x y
   refine Quotient.map₂' (fun x y ↦ ⟨x.1 * y.1, FilteredRing.mul_mem x.2 y.2⟩)