morphisms form a additive commutative group

Blackfeather007 · Oct 5, 2024 · 6996a7c · 6996a7c
1 parent e640564
commit 6996a7c
Showing 1 changed file with 48 additions and 73 deletions.
diff --git a/FilteredRing/category.lean b/FilteredRing/category.lean
@@ -3,40 +3,30 @@ open Pointwise CategoryTheory
 
 variable (R : Type u) {ι : Type v} [Ring R] [OrderedAddCommMonoid ι] [DecidableEq ι]
 variable (F : ι → AddSubgroup R)
--- instance RC : CategoryTheory.Bundled Ring
-
 
 structure FilModCat where
   Mod : ModuleCat R
-  -- carrier : Type v
-  -- [isAddCommGroup : AddCommGroup carrier]
-  -- [isModule : Module R carrier]
   fil : ι → Submodule R Mod
   [f : FilteredModule F Mod fil]
-  -- mono : ∀ i ≤ j, fil i ≤ fil j
-  -- smul_mem : ∀ i j, (F i : Set R) • fil j ≤ fil (i + j)
 
 instance : Category (FilModCat R F) where
   Hom M N := {f : M.Mod →ₗ[R] N.Mod // ∀ i, f '' M.fil i ≤ N.fil i}
   id _ := ⟨LinearMap.id, by intro i; simp⟩
-  comp f g := ⟨g.1.comp f.1, by
-    intro i
+  comp f g := ⟨g.1.comp f.1, fun i ↦ by
     have aux1 := f.2 i
     have aux2 := g.2 i
     simp_all only [Set.le_eq_subset, Set.image_subset_iff, LinearMap.coe_comp, Function.comp_apply]
     exact fun _ hx ↦ aux2 <| aux1 hx⟩
   id_comp _ := rfl
   comp_id _ := rfl
-  assoc f g h := rfl
+  assoc _ _ _ := rfl
 
 instance {M N : FilModCat R F} : FunLike (M ⟶ N) M.1 N.1 where
   coe f := f.1.toFun
   coe_injective' f g h := by
     cases f
     cases g
-    congr
-    apply DFunLike.coe_injective'
-    exact h
+    exact propext Subtype.val_inj |>.symm.mpr <| DFunLike.coe_injective' h
 
 
 
@@ -104,80 +94,65 @@ theorem comp_def (f : M ⟶ N) (g : N ⟶ U) : f ≫ g = g.comp f :=
 
 -/
 
-instance {M N : FilModCat R F} : AddCommGroup (M ⟶ N) where
+
+instance FilModCat.HomAddSemigroup {M N : FilModCat R F} : AddSemigroup (M ⟶ N) where
   add f g := ⟨f.1 + g.1, by
     simp only [Set.le_eq_subset, LinearMap.add_apply, Set.image_subset_iff]
-    intro i x hx
+    intro i _ hx
     have aux1 := f.2 i
     have aux2 := g.2 i
     simp_all only [SetLike.mem_coe, Set.le_eq_subset, Set.image_subset_iff, Set.mem_preimage]
     exact AddMemClass.add_mem (aux1 hx) (aux2 hx)⟩
-  add_assoc a b c:= by
-    suffices a.1 + b.1 + c.1 = a.1 + (b.1 + c.1) from Subtype.val_inj.1 this
-    rw [add_assoc]
-  zero := ⟨0, by simp⟩
-  zero_add a := by
-    suffices 0 + a.1 = a.1 from Subtype.val_inj.1 this
-    rw [zero_add]
-  add_zero a := by
-    suffices a.1 + 0 = a.1 from Subtype.val_inj.1 this
-    rw [add_zero]
+  add_assoc a b c := propext Subtype.val_inj |>.symm.mpr
+    <| add_assoc a.1 b.1 c.1
+
+instance FilModCat.HomAddMonoid {M N : FilModCat R F} : AddMonoid (M ⟶ N) where
+  zero := ⟨0, fun i ↦ by simp⟩
+  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, LinearMap.smul_apply, Set.image_subset_iff]
-    intro i x hx
+    intro i _ hx
     have aux := f.2 i
     simp_all only [SetLike.mem_coe, Set.le_eq_subset, Set.image_subset_iff, Set.mem_preimage]
     exact Submodule.smul_of_tower_mem (N.fil i) k (aux hx)⟩
-  neg a := ⟨-a.1, by
-    simp only [Set.le_eq_subset, LinearMap.neg_apply, Set.image_subset_iff]
-    intro i x hx
-    have aux := a.2 i
-    simp_all only [SetLike.mem_coe, Set.le_eq_subset, Set.image_subset_iff, Set.mem_preimage,
-      neg_mem_iff]
-    exact aux hx⟩
+  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
+
+instance FilModCat.HomSubNegMonoid {M N : FilModCat R F} : 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 x hx
+    intro i _ hx
     have aux := f.2 i
     simp_all only [SetLike.mem_coe, Set.le_eq_subset, Set.image_subset_iff, Set.mem_preimage]
     exact Submodule.smul_of_tower_mem (N.fil i) k (aux hx)⟩
-  neg_add_cancel a := by
-    suffices -a.1 + a.1 = 0 from Subtype.val_inj.1 this
-    rw [neg_add_cancel]
-  add_comm a b := by
-    suffices a.1 + b.1 = b.1 + a.1 from Subtype.val_inj.1 this
-    rw [add_comm]
-  nsmul_zero x := by
-    simp only [Set.le_eq_subset, zero_smul]; rfl
-  nsmul_succ n x := by
-    suffices (n + 1) • x.1 = n • x.1 + x.1 from Subtype.val_inj.1 this
-    rw [succ_nsmul]
-  zsmul_zero' a := by
+  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_all only [SetLike.mem_coe, Set.le_eq_subset, Set.image_subset_iff, Set.mem_preimage,
+      neg_mem_iff]
+    exact aux hx⟩
+  zsmul_zero' f := by
     simp only [Set.le_eq_subset, zero_smul]; rfl
-  zsmul_succ' n x := by
-    simp only [Set.le_eq_subset, Nat.succ_eq_add_one, Int.ofNat_eq_coe]
-    suffices Int.ofNat (n + 1) • x.1 = Int.ofNat n • x.1 + x.1 from Subtype.val_inj.1 this
-    rw [Int.ofNat_eq_coe, Int.ofNat_eq_coe, ← Int.ofNat_add_out, add_zsmul]
-    suffices Int.ofNat 1 • x.1 = x.1 from by
-      apply_fun fun j ↦ Int.ofNat n • x.1 + j at this
-      exact this
-    simp_all only [Int.ofNat_eq_coe, Nat.cast_one, Set.le_eq_subset, one_smul]
-  zsmul_neg' n a := by
-    simp only [Set.le_eq_subset, negSucc_zsmul, Nat.succ_eq_add_one]
-    suffices -((n + 1) • a.1) = -(Int.ofNat (n + 1) • a.1) from Subtype.val_inj.1 this
-    suffices (n + 1) • a.1 = Int.ofNat (n + 1) • a.1 from by
-      apply_fun fun j ↦ -j at this
-      exact this
-    suffices (n + 1) = Int.ofNat (n + 1) from by
-      apply_fun fun j ↦ j • a.1 at this
-      rw [← this]
-      norm_cast
-    simp_all only [Int.ofNat_eq_coe, Nat.cast_add, Nat.cast_one]
-
-
-instance : Preadditive (ModuleCat.{v} R) where
-  add_comp P Q R f f' g := by
-    ext
-    dsimp
-    erw [map_add]
-    rfl
+  zsmul_succ' k f := by
+    rw [← Subtype.val_inj]
+    simp only [Nat.succ_eq_add_one, Int.ofNat_eq_coe, Nat.cast_add, Nat.cast_one, Set.le_eq_subset,
+      natCast_zsmul]
+    norm_cast
+    exact succ_nsmul f.1 k
+  zsmul_neg' k f := by
+    rw [← Subtype.val_inj]
+    simp only [Set.le_eq_subset, negSucc_zsmul, Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one,
+      neg_inj]
+    norm_cast
+
+instance FilModCat.HomAddGroup {M N : FilModCat R F} : AddCommGroup (M ⟶ N) where
+  neg_add_cancel f := propext Subtype.val_inj |>.symm.mpr
+    <| neg_add_cancel f.1
+  add_comm f g := propext Subtype.val_inj |>.symm.mpr
+    <| AddCommMagma.add_comm f.1 g.1