From 75cc002bef90567bf47193dde474eb7ebabadbd9 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 12:31:37 -0700
Subject: [PATCH] finished a case of polytype 0

---
 CommAlg/PolyTEST.lean      |  0
 CommAlg/final_hil_pol.lean | 12 ++++++------
 2 files changed, 6 insertions(+), 6 deletions(-)
 create mode 100644 CommAlg/PolyTEST.lean

diff --git a/CommAlg/PolyTEST.lean b/CommAlg/PolyTEST.lean
new file mode 100644
index 0000000..e69de29
diff --git a/CommAlg/final_hil_pol.lean b/CommAlg/final_hil_pol.lean
index e3c141e..eff9302 100644
--- a/CommAlg/final_hil_pol.lean
+++ b/CommAlg/final_hil_pol.lean
@@ -134,13 +134,11 @@ def graded_isomorphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 : 
 [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
 [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
 (f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
-(hf : graded_morphism (fun i => (𝒜 i)) (fun i => (𝓜 i)) (fun i => (𝓝 i)) f)
-: (f : (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) := by
+: IsLinearEquiv f := by
   sorry
-
-
--- (⊕ i, 𝒜 i) (⨁ i, 𝓜 i) (⊕ i, 𝓝 i)
-
+-- f ∈ (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)
+-- LinearEquivClass f (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) (⨁ i, 𝓝 i)
+-- #print IsLinearEquiv
 #check graded_isomorphism
 
 
@@ -284,6 +282,8 @@ theorem Hilbert_polynomial_d_0_reduced
 
 
 
+
+