From 3760ec1d60cff21cbda4d929811d526a527f6a48 Mon Sep 17 00:00:00 2001 From: AlbertJ-314 Date: Sun, 6 Oct 2024 15:40:23 +0800 Subject: [PATCH 1/2] Add trivial filtration for rings and modules --- FilteredRing/Basic.lean | 39 +++++++++++++++++++++++++++++++++++++-- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/FilteredRing/Basic.lean b/FilteredRing/Basic.lean index 0d67119..103985f 100644 --- a/FilteredRing/Basic.lean +++ b/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 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 j i 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,7 +49,6 @@ 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 @@ -45,4 +62,22 @@ class FilteredModule (F' : ι → AddSubgroup M) where mono : ∀ 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)) M + (fun (i : ι) ↦ if i ≥ 0 then (⊤ : AddSubgroup M) else (⊥ : AddSubgroup M)) where + mono := by + intro j i 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 From ae1bd480381685e00dd84a535c5315de5369e20e Mon Sep 17 00:00:00 2001 From: FR-vdash-bot Date: Sun, 6 Oct 2024 16:04:18 +0800 Subject: [PATCH 2/2] cleanup, polynomial --- FilteredRing/Basic.lean | 41 +++++++++++---------- FilteredRing/Polynomial.lean | 71 ++++++++++++++++++++++++++++++++++++ FilteredRing/category.lean | 14 +++---- FilteredRing/graded.lean | 6 +-- 4 files changed, 102 insertions(+), 30 deletions(-) create mode 100644 FilteredRing/Polynomial.lean diff --git a/FilteredRing/Basic.lean b/FilteredRing/Basic.lean index 103985f..4e2adcf 100644 --- a/FilteredRing/Basic.lean +++ b/FilteredRing/Basic.lean @@ -7,14 +7,14 @@ 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) 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 j i ilej + 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] @@ -56,28 +56,29 @@ 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)) M - (fun (i : ι) ↦ if i ≥ 0 then (⊤ : AddSubgroup M) else (⊥ : AddSubgroup M)) where - mono := by - intro j i 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 ⊥)] + 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 diff --git a/FilteredRing/Polynomial.lean b/FilteredRing/Polynomial.lean new file mode 100644 index 0000000..66a6c74 --- /dev/null +++ b/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 diff --git a/FilteredRing/category.lean b/FilteredRing/category.lean index 4fae0ca..bcc47c7 100644 --- a/FilteredRing/category.lean +++ b/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 diff --git a/FilteredRing/graded.lean b/FilteredRing/graded.lean index 6b27cda..0b89f67 100644 --- a/FilteredRing/graded.lean +++ b/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)