From 871f38239c89e357335caa4b36e65494a07b7b48 Mon Sep 17 00:00:00 2001
From: monula95 dutta <monula95@gmail.com>
Date: Mon, 12 Jun 2023 20:59:28 +0000
Subject: [PATCH] TESTMOna

---
 comm_alg/Defhil.lean | 41 +++++++++++++++++++++++++++++++++++++++++
 comm_alg/hilpol.lean | 14 ++++++++++++++
 2 files changed, 55 insertions(+)
 create mode 100644 comm_alg/Defhil.lean
 create mode 100644 comm_alg/hilpol.lean

diff --git a/comm_alg/Defhil.lean b/comm_alg/Defhil.lean
new file mode 100644
index 0000000..63c140a
--- /dev/null
+++ b/comm_alg/Defhil.lean
@@ -0,0 +1,41 @@
+import Mathlib
+
+variable {R : Type _} (M A B C : Type _) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup A] [Module R A] [AddCommGroup B] [Module R B] [AddCommGroup C] [Module R C]
+variable (A' B' C' : ModuleCat R)
+#check ModuleCat.of R A
+
+example : Module R A' := inferInstance
+
+#check ModuleCat.of R B
+
+example : Module R B' := inferInstance
+
+#check ModuleCat.of R C
+
+example : Module R C' := inferInstance
+
+namespace CategoryTheory
+
+noncomputable instance abelian : Abelian (ModuleCat.{v} R) := inferInstance
+noncomputable instance haszero : Limits.HasZeroMorphisms (ModuleCat.{v} R) := inferInstance
+
+#check (A B : Submodule _ _) → (A ≤ B)
+
+#check Preorder (Submodule _ _)
+
+#check krullDim (Submodule _ _)
+
+noncomputable def length := krullDim (Submodule R M) 
+ 
+open ZeroObject
+
+namespace HasZeroMorphisms
+
+open LinearMap
+
+#check length M
+
+#check ModuleCat.of R
+
+lemma length_additive_shortexact {f : A ⟶ B} {g : B ⟶ C} (h : ShortExact f g) : length B = length A + length C := sorry
+
diff --git a/comm_alg/hilpol.lean b/comm_alg/hilpol.lean
new file mode 100644
index 0000000..957bade
--- /dev/null
+++ b/comm_alg/hilpol.lean
@@ -0,0 +1,14 @@
+import Mathlib
+
+
+--class GradedRing 
+
+variable [GradedRing S]
+
+namespace DirectSum
+
+namespace ideal
+
+def S_+ := ⊕ (i ≥ 0) S_i
+
+lemma  A set of homogeneous elements fi∈S+ generates S as an algebra over S0 ↔ they generate S+ as an ideal of S.
\ No newline at end of file