From 041916ea03810490bdc80e041b570bea1ace1b46 Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 9 Jan 2024 17:38:14 +0000 Subject: [PATCH 1/3] initial --- Mathlib/Algebra/DirectSum/Decomposition.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Algebra/DirectSum/Decomposition.lean b/Mathlib/Algebra/DirectSum/Decomposition.lean index 8de190c040407..116c27334c781 100644 --- a/Mathlib/Algebra/DirectSum/Decomposition.lean +++ b/Mathlib/Algebra/DirectSum/Decomposition.lean @@ -143,6 +143,15 @@ theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j rw [decompose_of_mem _ hx, DirectSum.of_eq_of_ne _ _ _ _ hij, ZeroMemClass.coe_zero] #align direct_sum.decompose_of_mem_ne DirectSum.decompose_of_mem_ne +theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) : + i = j := by + classical + have eq2 : (of (fun i : ι ↦ ℳ i) i (⟨x, hxi⟩ : ℳ i)).support = + (of (fun i : ι ↦ ℳ i) j (⟨x, hxj⟩ : ℳ j)).support + · rw [← decompose_coe, ← decompose_coe] + rwa [support_of, support_of, Finset.singleton_inj] at eq2 <;> + exact fun r ↦ hx <| Subtype.ext_iff_val.mp r + /-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as an additive monoid to a direct sum of components. -/ -- Porting note: deleted [simps] and added the corresponding lemmas by hand From 37298fea114a01a290b98e4882059c96fc5bc26d Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Tue, 9 Jan 2024 17:42:06 +0000 Subject: [PATCH 2/3] rename --- Mathlib/Algebra/DirectSum/Decomposition.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Decomposition.lean b/Mathlib/Algebra/DirectSum/Decomposition.lean index 116c27334c781..c8859b97bba59 100644 --- a/Mathlib/Algebra/DirectSum/Decomposition.lean +++ b/Mathlib/Algebra/DirectSum/Decomposition.lean @@ -146,10 +146,10 @@ theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) : i = j := by classical - have eq2 : (of (fun i : ι ↦ ℳ i) i (⟨x, hxi⟩ : ℳ i)).support = + have eq : (of (fun i : ι ↦ ℳ i) i (⟨x, hxi⟩ : ℳ i)).support = (of (fun i : ι ↦ ℳ i) j (⟨x, hxj⟩ : ℳ j)).support · rw [← decompose_coe, ← decompose_coe] - rwa [support_of, support_of, Finset.singleton_inj] at eq2 <;> + rwa [support_of, support_of, Finset.singleton_inj] at eq <;> exact fun r ↦ hx <| Subtype.ext_iff_val.mp r /-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as From 8a9c9cba4cd5328ab93e0ae921d529dae701eaff Mon Sep 17 00:00:00 2001 From: Jujian Zhang Date: Wed, 10 Jan 2024 06:46:14 +0000 Subject: [PATCH 3/3] =?UTF-8?q?=E6=9B=B4=E6=96=B0=20Decomposition.lean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Junyan Xu --- Mathlib/Algebra/DirectSum/Decomposition.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Decomposition.lean b/Mathlib/Algebra/DirectSum/Decomposition.lean index c8859b97bba59..f47be7b117efd 100644 --- a/Mathlib/Algebra/DirectSum/Decomposition.lean +++ b/Mathlib/Algebra/DirectSum/Decomposition.lean @@ -145,12 +145,7 @@ theorem decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) : i = j := by - classical - have eq : (of (fun i : ι ↦ ℳ i) i (⟨x, hxi⟩ : ℳ i)).support = - (of (fun i : ι ↦ ℳ i) j (⟨x, hxj⟩ : ℳ j)).support - · rw [← decompose_coe, ← decompose_coe] - rwa [support_of, support_of, Finset.singleton_inj] at eq <;> - exact fun r ↦ hx <| Subtype.ext_iff_val.mp r + contrapose! hx; rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx] /-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as an additive monoid to a direct sum of components. -/