SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 07:38:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

finished a case of polytype 0

Browse source
This commit is contained in:
chelseaandmadrid 2023-06-15 12:31:37 -07:00
parent 766c740c8d
commit 75cc002bef
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
CommAlg/PolyTEST.lean Normal file
View file

12
CommAlg/final_hil_pol.lean
View file

@ -134,13 +134,11 @@ def graded_isomorphism (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) (𝓝 :
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)] [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝓝 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝] [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜][DirectSum.Gmodule 𝒜 𝓝]
(f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) (f : (⨁ i, 𝓜 i) →ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i))
(hf : graded_morphism (fun i => (𝒜 i)) (fun i => (𝓜 i)) (fun i => (𝓝 i)) f) : IsLinearEquiv f := by
: (f : (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)) := by
sorry sorry
-- f ∈ (⨁ i, 𝓜 i) ≃ₗ[(⨁ i, 𝒜 i)] (⨁ i, 𝓝 i)
-- LinearEquivClass f (⨁ i, 𝒜 i) (⨁ i, 𝓜 i) (⨁ i, 𝓝 i)
-- (⊕ i, 𝒜 i) (⨁ i, 𝓜 i) (⊕ i, 𝓝 i) -- #print IsLinearEquiv
#check graded_isomorphism #check graded_isomorphism
@ -284,6 +282,8 @@ theorem Hilbert_polynomial_d_0_reduced