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

FilteredRing/category.lean

@@ -28,6 +28,48 @@ instance {M N : FilModCat R F} : FunLike (M ⟶ N) M.1 N.1 where
   coe f := f.1.toFun
   coe_injective' _ _ h := propext Subtype.val_inj |>.symm.mpr <| DFunLike.coe_injective' h
 
+/-- The object in the category of R-filt associated to an filtered R-module -/
+def of (X : Type w) [AddCommGroup X] [Module R X] (filX : ι → Submodule R X)
+  [FilteredModule F X filX] : FilModCat R F where
+    Mod := ModuleCat.of R X
+    fil := by
+      simp only [ModuleCat.coe_of]
+      use filX
+    f := by simpa [ModuleCat.coe_of]
+
+@[simp] theorem of_coe (X : FilModCat R F) : @of R _ _ _ F X.1 _ _ X.2 X.3 = X := rfl
+
+@[simp] theorem coe_of (X : Type w) [AddCommGroup X] [Module R X] (filX : ι → Submodule R X)
+  [FilteredModule F X filX] : (of R F X filX).1 = X := rfl
+
+/-- A `LinearMap` with degree 0 is a morphism in `Module R`. -/
+def ofHom {X Y : Type w} [AddCommGroup X] [Module R X] {filX : ι → Submodule R X}
+  [FilteredModule F X filX] [AddCommGroup Y] [Module R Y] {filY : ι → Submodule R Y}
+  [FilteredModule F Y filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) :
+  of R F X filX ⟶ of R F Y filY :=
+    ⟨f, deg0⟩
+
+@[simp 1100]
+theorem ofHom_apply {X Y : Type w} [AddCommGroup X] [Module R X] {filX : ι → Submodule R X}
+  [FilteredModule F X filX] [AddCommGroup Y] [Module R Y] {filY : ι → Submodule R Y}
+  [FilteredModule F Y filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) (x : X) :
+  ofHom R F f deg0 x = f x := rfl
+
+/-- Forgetting to the underlying type and then building the bundled object returns the original
+filtered module. -/
+-- Have no idea what ↑ means...
+@[simps]
+def ofSelfIso (M : FilModCat R F) : @of R _ _ _ F M.1 _ _ M.2 M.3 ≅ M where
+  hom := 𝟙 M
+  inv := 𝟙 M
+
+@[simp]
+theorem id_apply {M : FilModCat R F} (m : M.1) : (𝟙 M : M.1 → M.1) m = m := rfl
+
+@[simp]
+theorem coe_comp {M N U : FilModCat R F} (f : M ⟶ N) (g : N ⟶ U) : (f ≫ g : M.1 → U.1) = g ∘ f :=
+  rfl
+
 /-- ! To-do
 
 instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R) where
@@ -38,56 +80,12 @@ instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R) where
     dsimp at h
     rw [h])⟩
 
-
-/-- The object in the category of R-modules associated to an R-module -/
-def of (X : Type v) [AddCommGroup X] [Module R X] : ModuleCat R :=
-  ⟨X⟩
-
-
-/-- Typecheck a `LinearMap` as a morphism in `Module R`. -/
-def ofHom {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y]
-    [Module R Y] (f : X →ₗ[R] Y) : of R X ⟶ of R Y :=
-  f
-
-@[simp 1100]
-theorem ofHom_apply {R : Type u} [Ring R] {X Y : Type v} [AddCommGroup X] [Module R X]
-    [AddCommGroup Y] [Module R Y] (f : X →ₗ[R] Y) (x : X) : ofHom f x = f x :=
-  rfl
-
 instance : Inhabited (ModuleCat R) :=
   ⟨of R PUnit⟩
 
 instance ofUnique {X : Type v} [AddCommGroup X] [Module R X] [i : Unique X] : Unique (of R X) :=
   i
 
-@[simp] theorem of_coe (X : ModuleCat R) : of R X = X := rfl
-
--- Porting note: the simpNF linter complains, but we really need this?!
--- @[simp, nolint simpNF]
-theorem coe_of (X : Type v) [AddCommGroup X] [Module R X] : (of R X : Type v) = X :=
-  rfl
-
-variable {R}
-
-/-- Forgetting to the underlying type and then building the bundled object returns the original
-module. -/
-@[simps]
-def ofSelfIso (M : ModuleCat R) : ModuleCat.of R M ≅ M where
-  hom := 𝟙 M
-  inv := 𝟙 M
-
-
-@[simp]
-theorem id_apply (m : M) : (𝟙 M : M → M) m = m :=
-  rfl
-
-@[simp]
-theorem coe_comp (f : M ⟶ N) (g : N ⟶ U) : (f ≫ g : M → U) = g ∘ f :=
-  rfl
-
-theorem comp_def (f : M ⟶ N) (g : N ⟶ U) : f ≫ g = g.comp f :=
-  rfl
-
 @[simp] lemma forget_map (f : M ⟶ N) : (forget (ModuleCat R)).map f = (f : M → N) := rfl
 -/
 

FilteredRing/graded.lean

@@ -8,19 +8,14 @@ variable {R : Type u} [Ring R]
 
 variable {ι : Type v} [OrderedCancelAddCommMonoid ι] [DecidableEq ι]
 
-variable (F : ι → AddSubgroup R) [fil : FilteredRing F]
+variable (F : ι → AddSubgroup R) [FilteredRing F]
 
-open BigOperators Pointwise
+open BigOperators Pointwise DirectSum
 
 def F_lt (i : ι) := ⨆ k < i, F k
 
-abbrev GradedPiece (i : ι) : Type u := (F i) ⧸ (F_lt F i).addSubgroupOf (F i)
 
-protected lemma Filtration.iSup_le {i : ι} : ⨆ k < i, F k ≤ F i :=
-  iSup_le fun k ↦ iSup_le fun hk ↦ FilteredRing.mono k (le_of_lt hk)
-
-protected lemma Filtration.iSup_le' {i : ι} : ⨆ k < i, (F k : Set R) ≤ F i :=
-  iSup_le fun k ↦ iSup_le fun hk ↦ FilteredRing.mono k (le_of_lt hk)
+abbrev GradedPiece (i : ι) := (F i) ⧸ (F_lt F i).addSubgroupOf (F i)
 
 variable {F} in
 lemma Filtration.flt_mul_mem {i j : ι} {x y} (hx : x ∈ F_lt F i) (hy : y ∈ F j) :
@@ -60,13 +55,39 @@ def gradedMul {i j : ι} : GradedPiece F i → GradedPiece F j → GradedPiece F
   rw [eq]
   exact add_mem (Filtration.flt_mul_mem hx y₁.2) (Filtration.mul_flt_mem x₂.2 hy)
 
-instance : DirectSum.GSemiring (GradedPiece F) where
+instance : GradedMonoid.GMul (GradedPiece F) where
   mul := gradedMul F
-  mul_zero a := sorry
-  zero_mul := sorry
-  mul_add := sorry
+
+instance : GradedMonoid.GOne (GradedPiece F) where
+  one := by sorry
+
+
+instance : DirectSum.GSemiring (GradedPiece F) where
+  mul_zero := by
+    intro i j a
+    show gradedMul F a (0 : GradedPiece F j) = 0
+    unfold gradedMul
+    rw [← QuotientAddGroup.mk_zero, ← QuotientAddGroup.mk_zero]
+    induction a using Quotient.ind'
+    change Quotient.mk'' _ = Quotient.mk'' _
+    rw [Quotient.eq'']
+    simp [QuotientAddGroup.leftRel_apply, AddSubgroup.mem_addSubgroupOf]
+    exact zero_mem _
+  zero_mul := by sorry
+  mul_add := by
+    intro i j a b c
+    show gradedMul F a (b + c) = gradedMul F a b + gradedMul F a c
+    unfold gradedMul
+    induction a using Quotient.ind'
+    induction b using Quotient.ind'
+    induction c using Quotient.ind'
+    change Quotient.mk'' _ = Quotient.mk'' _
+    rw [Quotient.eq'']
+    simp [QuotientAddGroup.leftRel_apply, AddSubgroup.mem_addSubgroupOf]
+    rw [mul_add, neg_add_eq_zero.mpr]
+    exact zero_mem _
+    rfl
   add_mul := sorry
-  one := sorry
   one_mul := sorry
   mul_one := sorry
   mul_assoc := sorry
@@ -77,6 +98,46 @@ instance : DirectSum.GSemiring (GradedPiece F) where
   natCast_zero := sorry
   natCast_succ := sorry
 
+section integer
+variable {i : ι}
+#check DirectSum.of (GradedPiece F) i
+
+variable (F : ℤ → AddSubgroup R) [fil : FilteredRing F] (i : ℤ)
+abbrev GradedPieces := GradedPiece F '' Set.univ
+
+@[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
+
+-- instance : Semiring (⨁ i, GradedPiece F i) := by infer_instance
+
+-- variable {i : ι}
+-- #check DirectSum.of (GradedPiece F) i
+
+-- abbrev GradedPieces := GradedPiece F '' Set.univ
+
+
+-- instance : SetLike (GradedPieces F) (⨁ i, GradedPiece F i) where
+--   coe := by
+--     intro x
+
+--     sorry
+--   coe_injective' := sorry
 
 /-
 variable [PredOrder ι]