Skip to content

Commit

Permalink
filter based on index
Browse files Browse the repository at this point in the history
  • Loading branch information
@AlbertJ-314
AlbertJ-314 committed Oct 27, 2024
1 parent a714729 commit 4cef9fc
Showing 1 changed file with 17 additions and 110 deletions.
127 changes: 17 additions & 110 deletions FilteredRing/filtered_category.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,41 +8,18 @@ open Pointwise CategoryTheory
variable {R : Type u} {ι : Type v} [Ring R] [OrderedAddCommMonoid ι] {σ : Type o} [SetLike σ R]
(F : ι → σ)

structure FilteredModuleCat where
Mod : ModuleCat.{w, u} R
{σMod : Type*}
[instSetLike : SetLike σMod Mod.carrier]
[instAddSubmonoidClass : AddSubmonoidClass σMod Mod.carrier]
fil : ι → σMod
[f : FilteredModule F fil]

attribute [instance] FilteredModuleCat.instSetLike FilteredModuleCat.instAddSubmonoidClass
FilteredModuleCat.f

instance {M : FilteredModuleCat F} : IndexedModuleCat F where
Mod := M.Mod
σMod := M.σMod
instSetLike := M.instSetLike
instAddSubmonoidClass := M.instAddSubmonoidClass
fil := M.fil
f := {smul_mem := fun _ _ _ _ ha hb ↦ M.f.smul_mem ha hb}
structure FilteredModuleCat extends IndexedModuleCat R ι where
[instFilteredModule : FilteredModule F ind]

namespace FilteredModuleCat

instance {M : FilteredModuleCat F} {i : ι} : AddSubmonoid M.Mod where
carrier := Set.range (AddSubmonoidClass.subtype (M.fil i))
add_mem' {a b} ha hb := by
rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq] at *
exact add_mem ha hb
zero_mem' := by
show 0 ∈ Set.range ⇑(AddSubmonoidClass.subtype (M.fil i))
rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq]
exact zero_mem (M.fil i)
instance {M : FilteredModuleCat F} (i : ι) : AddSubmonoid M.Mod := IndexedModuleSubmonoid R ι i

-- 并不容易直接用IndexedModuleCategory，可能需用forget functor? Not sure...
instance filteredModuleCategory : Category (FilteredModuleCat F) where
Hom M N := {f : M.Mod →ₗ[R] N.Mod //
∀ i, f '' Set.range (AddSubmonoidClass.subtype (M.fil i))
≤ Set.range (AddSubmonoidClass.subtype (N.fil i))}
∀ i, f '' Set.range (AddSubmonoidClass.subtype (M.ind i))
≤ Set.range (AddSubmonoidClass.subtype (N.ind i))}
id _ := ⟨LinearMap.id, fun i ↦ by
simp only [LinearMap.id_coe, id_eq, Set.image_id', le_refl]⟩
comp f g := ⟨g.1.comp f.1, fun i ↦ by
Expand All @@ -54,9 +31,7 @@ instance filteredModuleCategory : Category (FilteredModuleCat F) where
comp_id _ := rfl
assoc _ _ _ := rfl

instance {M N : FilteredModuleCat 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
instance {M N : FilteredModuleCat F} : FunLike (M ⟶ N) M.Mod N.Mod := IndexedModuleFunLike R ι

instance filteredModuleConcreteCategory : ConcreteCategory (FilteredModuleCat F) where
forget :=
Expand All @@ -73,14 +48,14 @@ def of {X : Type w} [AddCommGroup X] [Module R X] {σX : Type*} [SetLike σX X]
Mod := ModuleCat.of R X
σMod := σX
instAddSubmonoidClass := by trivial
fil := filX
ind := filX

instance {X : FilteredModuleCat F} : FilteredModule F X.fil := X.f
instance {X : FilteredModuleCat F} : FilteredModule F X.ind := X.instFilteredModule

@[simp] theorem of_coe (X : FilteredModuleCat F) : of F X.fil = X := rfl
@[simp] theorem of_coe (X : FilteredModuleCat F) : of F X.ind = X := rfl

@[simp] theorem coe_of (X : Type w) [AddCommGroup X] [Module R X] {σX : Type*} [SetLike σX X]
[AddSubmonoidClass σX X] (filX : ι → σX) [FilteredModule F filX] : (of F filX).1 = X := rfl
[AddSubmonoidClass σX X] (filX : ι → σX) [FilteredModule F filX] : (of F filX).Mod = X := rfl

/-- A `LinearMap` with degree 0 is a morphism in `Module R`. -/
def ofHom {X Y : Type w} {σX σY : Type o} [AddCommGroup X] [Module R X] [SetLike σX X]
Expand All @@ -103,16 +78,16 @@ theorem ofHom_apply {X Y : Type w} {σX σY : Type o} [AddCommGroup X] [Module R
filtered module. -/
-- Have no idea what ↑ means...
@[simps]
def ofSelfIso (M : FilteredModuleCat F) : of F M.fil ≅ M where
def ofSelfIso (M : FilteredModuleCat F) : of F M.ind ≅ M where
hom := 𝟙 M
inv := 𝟙 M

@[simp]
theorem id_apply {M : FilteredModuleCat F} (m : M.1) : (𝟙 M : M.1 → M.1) m = m := rfl
theorem id_apply {M : FilteredModuleCat F} (m : M.Mod) : (𝟙 M : M.Mod → M.Mod) m = m := rfl

@[simp]
theorem coe_comp {M N U : FilteredModuleCat F} (f : M ⟶ N) (g : N ⟶ U) :
(f ≫ g : M.1 → U.1) = g ∘ f := rfl
(f ≫ g : M.Mod → U.Mod) = g ∘ f := rfl

-- instance : Inhabited (FilteredModuleCat F) := {
-- default := {
Expand All @@ -122,75 +97,8 @@ theorem coe_comp {M N U : FilteredModuleCat F} (f : M ⟶ N) (g : N ⟶ U) :
-- }
-- }

private instance {M N : FilteredModuleCat F} : AddSemigroup (M ⟶ N) where
add f g := ⟨f.1 + g.1, by
simp only [Set.le_eq_subset, Set.image_subset_iff]
intro i _ hx
have aux1 := f.2 i
have aux2 := g.2 i
simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.le_eq_subset,
Set.image_subset_iff, Set.preimage_setOf_eq] at *
exact add_mem (aux1 hx) (aux2 hx)⟩
add_assoc a b c := propext Subtype.val_inj |>.symm.mpr
<| add_assoc a.1 b.1 c.1

private instance {M N : FilteredModuleCat F} : AddCommMonoid (M ⟶ N) where
zero := ⟨0, fun i ↦ by
simp only [Set.le_eq_subset]
repeat rw [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype]
rw [Set.image_subset_iff]
exact fun a _ ↦ zero_mem (N.fil i)⟩
zero_add a := propext Subtype.val_inj |>.symm.mpr
<| AddZeroClass.zero_add a.1
add_zero a := propext Subtype.val_inj |>.symm.mpr
<| AddZeroClass.add_zero a.1
nsmul k f := ⟨k • f.1, by
simp only [Set.le_eq_subset, Set.image_subset_iff]
intro i _ hx
have aux := f.2 i
simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq] at *
exact nsmul_mem (aux hx) k⟩
nsmul_zero _ := by
simp only [Set.le_eq_subset, zero_smul]; rfl
nsmul_succ n x := propext Subtype.val_inj |>.symm.mpr
<| succ_nsmul x.1 n
add_comm f g := propext Subtype.val_inj |>.symm.mpr
<| AddCommMagma.add_comm f.1 g.1

private instance {M N : FilteredModuleCat F} [AddSubgroupClass N.σMod N.Mod.carrier] :
SubNegMonoid (M ⟶ N) where
zsmul k f := ⟨k • f.1, by
simp only [Set.le_eq_subset, LinearMap.smul_apply, Set.image_subset_iff]
intro i _ hx
have aux := f.2 i
simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq] at *
exact zsmul_mem (aux hx) k⟩
neg f := ⟨- f.1, by
simp only [Set.le_eq_subset, LinearMap.neg_apply, Set.image_subset_iff]
intro i _ hx
have aux := f.2 i
simp only [AddSubmonoidClass.coe_subtype, Subtype.range_coe_subtype, Set.mem_setOf_eq,
Set.le_eq_subset, Set.image_subset_iff, Set.preimage_setOf_eq,
neg_mem_iff] at *
exact aux hx⟩
zsmul_zero' f := by
simp only [Set.le_eq_subset, zero_smul]; rfl
zsmul_succ' k f := by
rw [← Subtype.val_inj]
simp only [Nat.succ_eq_add_one, Int.ofNat_eq_coe, Nat.cast_one, Set.le_eq_subset, natCast_zsmul]
exact succ_nsmul f.1 k
zsmul_neg' k f := by
rw [← Subtype.val_inj]
simp only [Set.le_eq_subset, negSucc_zsmul, Nat.cast_add, Nat.cast_one, neg_inj]
norm_cast

instance {M N : FilteredModuleCat F} [AddSubgroupClass N.σMod N.Mod.carrier] :
AddCommGroup (M ⟶ N) where
neg_add_cancel f := propext Subtype.val_inj |>.symm.mpr
<| neg_add_cancel f.1
add_comm := AddCommMagma.add_comm
AddCommGroup (M ⟶ N) := AddCommGroupMorphisms R ι

instance (h : ∀ P : FilteredModuleCat F, AddSubgroupClass P.σMod P.Mod.carrier) :
Preadditive (FilteredModuleCat F) where
Expand All @@ -209,8 +117,7 @@ private def proofGP (m : ModuleCat.{w, u} R) (i j : ι) (x : R) : AddSubmonoid m
congrArg (Membership.mem (F' F m (j + i))) (smul_zero x) |>.mpr (F' F m (j + i)).zero_mem }

open AddSubmonoid in
instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F] :
FilteredModule F (F' F m) where
instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F]: FilteredModule F (F' F m) where
mono := fun hij ↦ by
simp only [F', closure_le]
rintro x ⟨r, ⟨hr, ⟨a, ha⟩⟩⟩
Expand All @@ -227,7 +134,7 @@ instance toFilteredModule (m : ModuleCat.{w, u} R) [FilteredRing F] :
open AddSubmonoid in
def DeducedFunctor [FilteredRing F] : CategoryTheory.Functor (ModuleCat.{w, u} R)
(FilteredModuleCat F) where
obj m := { Mod := m, fil := F' F m, f := toFilteredModule F m }
obj m := { Mod := m, ind := F' F m, instFilteredModule := toFilteredModule F m }
map := fun {X Y} hom ↦ ⟨hom, by
rintro i p ⟨x, ⟨hx1, hx2⟩⟩
set toAddGP := (closure {x : Y.1 | ∃ r ∈ F i, ∃ a, x = r • a}).comap hom.toAddMonoidHom
Expand Down

0 comments on commit 4cef9fc

Please sign in to comment.