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

FilteredRing/Basic.lean

@@ -4,12 +4,30 @@ universe u v w
 
 variable {R : Type u} {ι : Type v} [Ring R] [OrderedAddCommMonoid ι]
 
+section FilteredRing
+
 class FilteredRing (F : ι → AddSubgroup R) where
-  mono : ∀ i ≤ j, F i ≤ F j
+  mono {i j} : i ≤ j → F i ≤ F j
   one : 1 ∈ F 0
   mul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F j → x * y ∈ F (i + j)
 
-section FilteredRing
+instance trivialRingFiltration (comparable_with_zero : ∀ i : ι, Decidable (i ≥ 0)) :
+  FilteredRing (fun (i : ι) ↦ if i ≥ 0 then (⊤ : AddSubgroup R) else (⊥ : AddSubgroup R)) where
+    mono := by
+      intro i j ilej
+      by_cases ige0 : i ≥ 0
+      · simp only [ge_iff_le, ige0, reduceIte, top_le_iff, Preorder.le_trans 0 i j ige0 ilej]
+      · simp only [ge_iff_le, ige0, reduceIte, bot_le]
+    one := by simp only [ge_iff_le, le_refl, reduceIte, AddSubgroup.mem_top]
+    mul_mem := by
+      intro i j x y hx hy
+      by_cases ige0 : i ≥ 0
+      · by_cases jge0 : j ≥ 0
+        · simp only [ge_iff_le, Left.add_nonneg ige0 jge0, reduceIte, AddSubgroup.mem_top]
+        · simp only [ge_iff_le, jge0, reduceIte, AddSubgroup.mem_bot] at hy
+          simp only [ge_iff_le, hy, mul_zero, AddSubgroup.zero_mem (if 0 ≤ i + j then ⊤ else ⊥)]
+      · simp only [ge_iff_le, ige0, reduceIte, AddSubgroup.mem_bot] at hx
+        simp only [ge_iff_le, hx, zero_mul, AddSubgroup.zero_mem (if 0 ≤ i + j then ⊤ else ⊥)]
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
 
@@ -31,18 +49,36 @@ instance Module_of_zero_fil (i : ι) : Module (F 0) (F i) where
   add_smul := fun x y a ↦ SetLike.coe_eq_coe.mp (RightDistribClass.right_distrib (x : R) y a)
   zero_smul := fun x ↦ SetLike.coe_eq_coe.mp (zero_mul (x : R))
 
-
 end FilteredRing
 
 
 section FilteredModule
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
 
-variable (M : Type w) [AddCommGroup M] [Module R M]
+variable {M : Type w} [AddCommGroup M] [Module R M]
 
 class FilteredModule (F' : ι → AddSubgroup M) where
-  mono : ∀ i ≤ j, F' i ≤ F' j
+  mono : ∀ {i j}, i ≤ j → F' i ≤ F' j
   smul_mem : ∀ {i j x y}, x ∈ F i → y ∈ F' j → x • y ∈ F' (i + j)
 
+instance trivialModuleFiltration (comparable_with_zero : ∀ i : ι, Decidable (i ≥ 0)) :
+    FilteredModule
+      (fun (i : ι) ↦ if i ≥ 0 then (⊤ : AddSubgroup R) else (⊥ : AddSubgroup R))
+      (fun (i : ι) ↦ if i ≥ 0 then (⊤ : AddSubgroup M) else (⊥ : AddSubgroup M)) where
+  mono := by
+    intro i j ilej
+    by_cases ige0 : i ≥ 0
+    · simp only [ge_iff_le, ige0, reduceIte, top_le_iff, Preorder.le_trans 0 i j ige0 ilej]
+    · simp only [ge_iff_le, ige0, reduceIte, bot_le]
+  smul_mem := by
+    intro i j r m hr hm
+    by_cases ige0 : i ≥ 0
+    · by_cases jge0 : j ≥ 0
+      · simp only [ge_iff_le, Left.add_nonneg ige0 jge0, reduceIte, AddSubgroup.mem_top]
+      · simp only [ge_iff_le, jge0, reduceIte, AddSubgroup.mem_bot] at hm
+        simp only [ge_iff_le, hm, smul_zero, AddSubgroup.zero_mem (if 0 ≤ i + j then ⊤ else ⊥)]
+    · simp only [ge_iff_le, ige0, reduceIte, AddSubgroup.mem_bot] at hr
+      simp only [ge_iff_le, hr, zero_smul, AddSubgroup.zero_mem (if 0 ≤ i + j then ⊤ else ⊥)]
+
 end FilteredModule

FilteredRing/Polynomial.lean

@@ -0,0 +1,71 @@
+import FilteredRing.Basic
+import Mathlib.RingTheory.Polynomial.Basic
+
+namespace Polynomial
+variable (R : Type*) [Ring R]
+
+instance : FilteredRing (fun i ↦ (degreeLE R i).toAddSubgroup) where
+  mono {i j} hij p := by
+    simp_rw [Submodule.mem_toAddSubgroup, mem_degreeLE]
+    intro h
+    exact h.trans hij
+  one := by
+    simp_rw [Submodule.mem_toAddSubgroup, mem_degreeLE]
+    simp
+  mul_mem {i j x y} hx hy := by
+    simp_rw [Submodule.mem_toAddSubgroup, mem_degreeLE] at hx hy ⊢
+    exact (degree_mul_le _ _).trans (by mono)
+
+end Polynomial
+
+namespace PolynomialModule
+variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
+
+open scoped Polynomial
+
+@[simps]
+def lcoeff (n : ℕ) : (PolynomialModule R M) →ₗ[R] M where
+  toFun p := p n
+  map_add' p q := add_apply R p q n
+  map_smul' r p := by
+    dsimp
+    rw [← IsScalarTower.algebraMap_smul R[X], Polynomial.algebraMap_eq,
+      ← Polynomial.monomial_zero_left, monomial_smul_apply]
+    simp
+
+def degreeLE (n : WithBot ℕ) : Submodule R (PolynomialModule R M) :=
+  ⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff R M k)
+
+def degreeLT (n : ℕ) : Submodule R (PolynomialModule R M) :=
+  ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff R M k)
+
+instance : FilteredModule
+    (fun i ↦ (Polynomial.degreeLE R i).toAddSubgroup)
+    (fun i ↦ (degreeLE R M i).toAddSubgroup) where
+  mono {i j} hij p := by
+    simp? [degreeLE] says
+      simp only [degreeLE, gt_iff_lt, Submodule.mem_toAddSubgroup, Submodule.mem_iInf,
+        LinearMap.mem_ker, lcoeff_apply]
+    intro H k hk
+    exact H k (hij.trans_lt hk)
+  smul_mem {i j x y} hx hy := by
+    simp? [Polynomial.degreeLE, degreeLE] at hx hy ⊢ says
+      simp only [Polynomial.degreeLE, gt_iff_lt, Submodule.mem_toAddSubgroup, Submodule.mem_iInf,
+        LinearMap.mem_ker, Polynomial.lcoeff_apply, degreeLE, lcoeff_apply] at hx hy ⊢
+    intro k hk
+    rw [smul_apply]
+    apply Finset.sum_eq_zero
+    simp only [Finset.mem_antidiagonal, Prod.forall]
+    intro ix iy hixy
+    obtain (hik | hjk) : i < ix ∨ j < iy := by
+      cases i with | bot => exact .inl (WithBot.bot_lt_coe _) | coe i => ?_
+      cases j with | bot => exact .inr (WithBot.bot_lt_coe _) | coe j => ?_
+      rw [← WithBot.coe_add] at hk
+      erw [WithBot.coe_lt_coe] at hk
+      erw [WithBot.coe_lt_coe, WithBot.coe_lt_coe]
+      simp only [Nat.cast_id] at hk ⊢
+      omega
+    · simp [hx, hik]
+    · simp [hy, hjk]
+
+end PolynomialModule

FilteredRing/category.lean

@@ -10,7 +10,7 @@ variable (F : ι → AddSubgroup R)
 structure FilModCat where
   Mod : ModuleCat.{w, u} R
   fil : ι → AddSubgroup Mod.carrier
-  [f : FilteredModule F Mod.carrier fil]
+  [f : FilteredModule F fil]
 
 instance : Category (FilModCat F) where
   Hom M N := {f : M.Mod →ₗ[R] N.Mod // ∀ i, f '' M.fil i ≤ N.fil i}
@@ -30,7 +30,7 @@ instance {M N : FilModCat F} : FunLike (M ⟶ N) M.1 N.1 where
 
 /-- 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 : ι → AddSubgroup X)
-  [FilteredModule F X filX] : FilModCat F where
+  [FilteredModule F filX] : FilModCat F where
     Mod := ModuleCat.of R X
     fil := by
       simp only [ModuleCat.coe_of]
@@ -40,19 +40,19 @@ def of (X : Type w) [AddCommGroup X] [Module R X] (filX : ι → AddSubgroup X)
 @[simp] theorem of_coe (X : FilModCat 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 : ι → AddSubgroup X)
-  [FilteredModule F X filX] : (of F X filX).1 = X := rfl
+  [FilteredModule F filX] : (of 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 : ι → AddSubgroup X}
-  [FilteredModule F X filX] [AddCommGroup Y] [Module R Y] {filY : ι → AddSubgroup Y}
-  [FilteredModule F Y filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) :
+  [FilteredModule F filX] [AddCommGroup Y] [Module R Y] {filY : ι → AddSubgroup Y}
+  [FilteredModule F filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) :
   of F X filX ⟶ of F Y filY :=
     ⟨f, deg0⟩
 
 @[simp 1100]
 theorem ofHom_apply {X Y : Type w} [AddCommGroup X] [Module R X] {filX : ι → AddSubgroup X}
-  [FilteredModule F X filX] [AddCommGroup Y] [Module R Y] {filY : ι → AddSubgroup Y}
-  [FilteredModule F Y filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) (x : X) :
+  [FilteredModule F filX] [AddCommGroup Y] [Module R Y] {filY : ι → AddSubgroup Y}
+  [FilteredModule F filY] (f : X →ₗ[R] Y) (deg0 : ∀ i, f '' filX i ≤ filY i) (x : X) :
   ofHom F f deg0 x = f x := rfl
 
 /-- Forgetting to the underlying type and then building the bundled object returns the original
@@ -169,11 +169,11 @@ private def proofGP (m : ModuleCat.{w, u} R) (i j : ι) (x : R) : AddSubgroup m.
   neg_mem' := by
     simp only [Set.mem_setOf_eq, smul_neg, neg_mem_iff, imp_self, implies_true] }
 
-instance toFilMod (m : ModuleCat.{w, u} R) [hfilR : FilteredRing F] : FilteredModule F m (F' F m) where
-  mono := fun i hij ↦ by
+instance toFilMod (m : ModuleCat.{w, u} R) [hfilR : FilteredRing F] : FilteredModule F (F' F m) where
+  mono := fun hij ↦ by
     simp only [F', AddSubgroup.closure_le]
     rintro x ⟨r, ⟨hr, ⟨a, ha⟩⟩⟩
-    exact AddSubgroup.mem_closure.mpr fun K hk ↦ hk <| Exists.intro r ⟨hfilR.mono i hij hr, Exists.intro a ha⟩
+    exact AddSubgroup.mem_closure.mpr fun K hk ↦ hk <| Exists.intro r ⟨hfilR.mono hij hr, Exists.intro a ha⟩
   smul_mem := by
     intro j i x y hx hy
     have : F' F m i ≤ proofGP F m i j x := by

FilteredRing/graded.lean

@@ -6,7 +6,7 @@ suppress_compilation
 
 variable {R : Type u} [Ring R]
 
-variable {ι : Type v} [OrderedCancelAddCommMonoid ι] [DecidableEq ι]
+variable {ι : Type v} [OrderedCancelAddCommMonoid ι]
 
 variable (F : ι → AddSubgroup R) [FilteredRing F]
 
@@ -99,7 +99,7 @@ instance : DirectSum.GSemiring (GradedPiece F) where
   natCast_succ := sorry
 
 section integer
-variable {i : ι}
+variable [DecidableEq ι] {i : ι}
 #check DirectSum.of (GradedPiece F) i
 
 variable (F : ℤ → AddSubgroup R) [fil : FilteredRing F] (i : ℤ)
@@ -111,7 +111,7 @@ theorem fil_Z (i : ℤ) : F_lt F i = F (i - 1) := by
   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
+  · exact fun hx ↦ (iSup_le fun k ↦ iSup_le fil.mono) hx
   · intro hx
     have : F (i - 1) ≤ ⨆ k, ⨆ (_ : k ≤ i - 1), F k := by
       apply le_iSup_of_le (i - 1)