From 7333c7ebfe9fe825bc1136727470f7f8c578f7d7 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 19 May 2026 11:49:10 +0200 Subject: [PATCH 01/27] =?UTF-8?q?1.=20add=20variant=20equivCongrLeft'=20of?= =?UTF-8?q?=20equivCongrLeft,=20and=20corresponding=20=E2=80=A6=5Fapply=20?= =?UTF-8?q?lemma=202.=20add=20=E2=80=A6=5Fof=20lemmas=20for=20both=20equiv?= =?UTF-8?q?CongrLeft=20and=20equivCongrLeft'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit re 1: Mathematically, I don't see why one version should be preferred over the other, but the existing equivCongrLeft is more difficult to work with when the equivalence h : ι ≃ κ is naturally given in the opposite direction. (I could not avoid explicit type casts through the equality h.symm.symm = h when defining sigmaFiberEquiv in terms of equivCongrLeft.) Very unsure about the name of equivCongrLeft'. The name equivCongrLeft was chosen in analogy with Equiv.piCongrLeft. Equiv.piCongrRight looks very different. --- Mathlib/Algebra/DirectSum/Basic.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 7bd5417d8977b6..30da5b50725092 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -306,11 +306,29 @@ variable {κ : Type*} def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv } +def equivCongrLeft' (h : κ ≃ ι) : (⨁ i, β i) ≃+ ⨁ i, β (h i) := + { DFinsupp.equivCongrLeft h.symm with map_add' := DFinsupp.comapDomain'_add _ h.left_inv } + @[simp] theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : equivCongrLeft h f k = f (h.symm k) := by exact DFinsupp.comapDomain'_apply _ h.right_inv _ _ +@[simp] +theorem equivCongrLeft'_apply (h : κ ≃ ι) (f : ⨁ i, β i) (k : κ) : + equivCongrLeft' h f k = f (h k) := by + exact DFinsupp.comapDomain'_apply _ h.left_inv _ _ + +@[simp] +theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) : + equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := by + exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _ + +@[simp] +theorem equivCongrLeft'_of [DecidableEq ι] [DecidableEq κ] (h : κ ≃ ι) (k : κ) (m : β (h k)) : + equivCongrLeft' h (of β (h k) m) = of (fun k ↦ β (h k)) k m := by + exact DFinsupp.comapDomain'_single _ h.left_inv' _ _ + end CongrLeft section Option From 8da74c517545047e767eb4ea1b519c6a12e4be35 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 19 May 2026 12:43:11 +0200 Subject: [PATCH 02/27] =?UTF-8?q?Add=20=E2=80=A6of=20lemma=20for=20sigmaCu?= =?UTF-8?q?rry,=20i.e.=20sigmaCurry=5Fof.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/DirectSum/Basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 30da5b50725092..c966bf8633d1d2 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -357,6 +357,12 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) sigmaCurry f i j = f ⟨i, j⟩ := DFinsupp.sigmaCurry_apply (δ := δ) _ i j +@[simp] +theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i)(x : δ k.1 k.2) : + sigmaCurry (of (fun k ↦ δ k.1 k.2) k x) = + of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) := by + exact DFinsupp.sigmaCurry_single k x + /-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of `curry`. -/ def sigmaUncurry : (⨁ (i) (j), δ i j) →+ ⨁ i : Σ _i, _, δ i.1 i.2 where From ed508da6b5d5365a75eb788e96167b15f72a865d Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 20 May 2026 10:11:00 +0200 Subject: [PATCH 03/27] =?UTF-8?q?Add=20sigmaFiberAddEquiv:=20the=20equival?= =?UTF-8?q?ence=20between=20a=20direct=20sum=20indexed=20by=20a=20type=20?= =?UTF-8?q?=CE=B9=E2=82=81=20and=20the=20=20double=20sum=20indexed=20by=20?= =?UTF-8?q?a=20type=20=CE=B9=E2=82=82=20and=20the=20fibres=20of=20a=20map?= =?UTF-8?q?=20f=20:=20=CE=B9=E2=82=81=20=E2=86=92=20=CE=B9=E2=82=82.=20=20?= =?UTF-8?q?Add=20two=20=E2=80=A6=5Fapply=20lemmas=20and=20an=20=E2=80=A6?= =?UTF-8?q?=5Fof=20lemma.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Unsure about the naming of the two different …_apply lemmas; called them …_apply and …_apply' for now. The second (…_apply') cannot be a simp lemma as it would prevent the first (…_apply) from firing. --- Mathlib/Algebra/DirectSum/Basic.lean | 38 ++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index c966bf8633d1d2..285a07c3c67839 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -381,6 +381,44 @@ def sigmaCurryEquiv : (⨁ i : Σ _i, _, δ i.1 i.2) ≃+ ⨁ (i) (j), δ i j := end Sigma +section SigmaFiber + +variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) +variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] + +/-- The equivalence between a direct sum indexed by a type `ι₁` and the + double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ +def sigmaFiberAddEquiv [DecidableEq ι₂] : + (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := + (equivCongrLeft' (Equiv.sigmaFiberEquiv f)).trans + (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) + +theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : + sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft' (Equiv.sigmaFiberEquiv f) x) := by + simp only [DirectSum.sigmaFiberAddEquiv,AddEquiv.trans_apply] + rfl + +@[simp] +theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : + sigmaFiberAddEquiv f x j i'= x i' := by + rw [DirectSum.sigmaFiberAddEquiv_apply'] + rfl + +@[simp] +theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : + sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := by + let h := Equiv.sigmaFiberEquiv f + let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ + calc sigmaFiberAddEquiv f (of β (h k) x) + _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β (h k)) k x) := by + simp only [sigmaFiberAddEquiv_apply',h,equivCongrLeft'_of] + _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by + rfl + _ = of _ k.1 (of _ k.2 x) := by + simp only [sigmaCurry_of] + +end SigmaFiber + /-- The canonical embedding from `⨁ i, A i` to `M` where `A` is a collection of `AddSubmonoid M` indexed by `ι`. From 438facb6efc4381d6c4df347c27cfb8bfd87d112 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 20 May 2026 12:49:10 +0200 Subject: [PATCH 04/27] add DocString for DirectSum.equivCongrLeft' --- Mathlib/Algebra/DirectSum/Basic.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 285a07c3c67839..d80142d80eb80e 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -302,11 +302,14 @@ section CongrLeft variable {κ : Type*} -/-- Reindexing terms of a direct sum. -/ +/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence + `h : ι ≃ κ`. -/ def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv } -def equivCongrLeft' (h : κ ≃ ι) : (⨁ i, β i) ≃+ ⨁ i, β (h i) := +/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence + `h : κ ≃ ι`. -/ +def equivCongrLeft' (h : κ ≃ ι) : (⨁ i, β i) ≃+ ⨁ k, β (h k) := { DFinsupp.equivCongrLeft h.symm with map_add' := DFinsupp.comapDomain'_add _ h.left_inv } @[simp] From 6805b5caea02efd5864659055a017f5e0937033c Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Mon, 22 Jun 2026 16:44:27 +0200 Subject: [PATCH 05/27] Apply suggestion from @themathqueen Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index d80142d80eb80e..2e571f5875d371 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -310,7 +310,7 @@ def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := /-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence `h : κ ≃ ι`. -/ def equivCongrLeft' (h : κ ≃ ι) : (⨁ i, β i) ≃+ ⨁ k, β (h k) := - { DFinsupp.equivCongrLeft h.symm with map_add' := DFinsupp.comapDomain'_add _ h.left_inv } + equivCongrLeft h.symm @[simp] theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : From e28e218969cb5d9e78534e711f3b41632cdb7e09 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 23 Jun 2026 11:22:00 +0200 Subject: [PATCH 06/27] remove equivCongrLeft' again --- Mathlib/Algebra/DirectSum/Basic.lean | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 2e571f5875d371..d11135722d1b95 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -307,31 +307,16 @@ variable {κ : Type*} def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv } -/-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence - `h : κ ≃ ι`. -/ -def equivCongrLeft' (h : κ ≃ ι) : (⨁ i, β i) ≃+ ⨁ k, β (h k) := - equivCongrLeft h.symm - @[simp] theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : equivCongrLeft h f k = f (h.symm k) := by exact DFinsupp.comapDomain'_apply _ h.right_inv _ _ -@[simp] -theorem equivCongrLeft'_apply (h : κ ≃ ι) (f : ⨁ i, β i) (k : κ) : - equivCongrLeft' h f k = f (h k) := by - exact DFinsupp.comapDomain'_apply _ h.left_inv _ _ - @[simp] theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) : equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := by exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _ -@[simp] -theorem equivCongrLeft'_of [DecidableEq ι] [DecidableEq κ] (h : κ ≃ ι) (k : κ) (m : β (h k)) : - equivCongrLeft' h (of β (h k) m) = of (fun k ↦ β (h k)) k m := by - exact DFinsupp.comapDomain'_single _ h.left_inv' _ _ - end CongrLeft section Option @@ -393,11 +378,11 @@ variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ def sigmaFiberAddEquiv [DecidableEq ι₂] : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := - (equivCongrLeft' (Equiv.sigmaFiberEquiv f)).trans + (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : - sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft' (Equiv.sigmaFiberEquiv f) x) := by + sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := by simp only [DirectSum.sigmaFiberAddEquiv,AddEquiv.trans_apply] rfl @@ -413,12 +398,11 @@ theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : let h := Equiv.sigmaFiberEquiv f let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ calc sigmaFiberAddEquiv f (of β (h k) x) - _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β (h k)) k x) := by - simp only [sigmaFiberAddEquiv_apply',h,equivCongrLeft'_of] _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by - rfl + rw [sigmaFiberAddEquiv_apply'] + exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) _ = of _ k.1 (of _ k.2 x) := by - simp only [sigmaCurry_of] + rw [sigmaCurry_of] end SigmaFiber From 42403fac8f6fa84a8860934140ee4dba07de7843 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 23 Jun 2026 11:44:22 +0200 Subject: [PATCH 07/27] remove doubled dedidability assumption --- Mathlib/Algebra/DirectSum/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index d11135722d1b95..ed095067d026c7 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -376,8 +376,7 @@ variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] /-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ -def sigmaFiberAddEquiv [DecidableEq ι₂] : - (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := +def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) From d5f3612f523c9e224bf4f582c7e4eac07d7dfa6c Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 12:11:09 +0200 Subject: [PATCH 08/27] adapt spacing Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index ed095067d026c7..431de0f31a8c8f 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -393,7 +393,7 @@ theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ @[simp] theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : - sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := by + sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := by let h := Equiv.sigmaFiberEquiv f let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ calc sigmaFiberAddEquiv f (of β (h k) x) From c5c3aece91cf28f261a892f263bae3f4994b964c Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 12:11:28 +0200 Subject: [PATCH 09/27] adapt spacing Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 431de0f31a8c8f..b2843deafb32bc 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -303,7 +303,7 @@ section CongrLeft variable {κ : Type*} /-- Reindexing terms of a direct sum: change indexing type from `ι` to `κ` along an equivalence - `h : ι ≃ κ`. -/ +`h : ι ≃ κ`. -/ def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := { DFinsupp.equivCongrLeft h with map_add' := DFinsupp.comapDomain'_add _ h.right_inv } From ba5a211a9a1b9b244dc3bd1a458dbf8181ca3058 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 23 Jun 2026 18:09:07 +0200 Subject: [PATCH 10/27] remove 'by exact' --- Mathlib/Algebra/DirectSum/Basic.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index b2843deafb32bc..c8176718e7b70c 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -309,13 +309,13 @@ def equivCongrLeft (h : ι ≃ κ) : (⨁ i, β i) ≃+ ⨁ k, β (h.symm k) := @[simp] theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : - equivCongrLeft h f k = f (h.symm k) := by - exact DFinsupp.comapDomain'_apply _ h.right_inv _ _ + equivCongrLeft h f k = f (h.symm k) := + DFinsupp.comapDomain'_apply _ h.right_inv _ _ @[simp] theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) : - equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := by - exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _ + equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := + DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _ end CongrLeft @@ -348,8 +348,8 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) @[simp] theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i)(x : δ k.1 k.2) : sigmaCurry (of (fun k ↦ δ k.1 k.2) k x) = - of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) := by - exact DFinsupp.sigmaCurry_single k x + of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) := + DFinsupp.sigmaCurry_single k x /-- The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of `curry`. -/ From 4ae1133fc8bb48bcf7cb61e18dfa34357cb684e8 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 21:29:28 +0200 Subject: [PATCH 11/27] indent calc block Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index c8176718e7b70c..04b02ad7b8c53e 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -397,10 +397,10 @@ theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : let h := Equiv.sigmaFiberEquiv f let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ calc sigmaFiberAddEquiv f (of β (h k) x) - _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by + _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by rw [sigmaFiberAddEquiv_apply'] exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) - _ = of _ k.1 (of _ k.2 x) := by + _ = of _ k.1 (of _ k.2 x) := by rw [sigmaCurry_of] end SigmaFiber From 064fcd47ed854c59c4a09a459ef74d83918f8787 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 21:30:32 +0200 Subject: [PATCH 12/27] remove unnecessary explicit cast Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 04b02ad7b8c53e..c1f4567bda37f9 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -315,7 +315,7 @@ theorem equivCongrLeft_apply (h : ι ≃ κ) (f : ⨁ i, β i) (k : κ) : @[simp] theorem equivCongrLeft_of [DecidableEq ι] [DecidableEq κ] (h : ι ≃ κ) (k : κ) (x : β (h.symm k)) : equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := - DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _ + DFinsupp.comapDomain'_single h.symm h.right_inv _ _ end CongrLeft From 5f6c2f0710350f48c78cd6c63f36c6c7b6dcd7c7 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 21:31:39 +0200 Subject: [PATCH 13/27] shorten proof to rfl Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index c1f4567bda37f9..15c356187cd517 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -381,9 +381,7 @@ def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : - sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := by - simp only [DirectSum.sigmaFiberAddEquiv,AddEquiv.trans_apply] - rfl + sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := rfl @[simp] theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : From a5ea5563e59ae74df9cfdb8b0a0a5685fe774e6d Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 23 Jun 2026 21:31:53 +0200 Subject: [PATCH 14/27] shorten proof to rfl Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 15c356187cd517..26076a43476a7d 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -385,9 +385,7 @@ theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : @[simp] theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : - sigmaFiberAddEquiv f x j i'= x i' := by - rw [DirectSum.sigmaFiberAddEquiv_apply'] - rfl + sigmaFiberAddEquiv f x j i'= x i' := rfl @[simp] theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : From 0d58d24d28412c9cd6a1ae3cf391532f27a1f52d Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 23 Jun 2026 21:36:28 +0200 Subject: [PATCH 15/27] add missing space --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 26076a43476a7d..84486dae042842 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -385,7 +385,7 @@ theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : @[simp] theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : - sigmaFiberAddEquiv f x j i'= x i' := rfl + sigmaFiberAddEquiv f x j i' = x i' := rfl @[simp] theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : From e48c29cc547c2b19f25737c128b01dcbff58ca9e Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 23 Jun 2026 21:41:33 +0200 Subject: [PATCH 16/27] simplify last step of calc proof --- Mathlib/Algebra/DirectSum/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 84486dae042842..8cdfa65dd7adec 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -396,8 +396,7 @@ theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by rw [sigmaFiberAddEquiv_apply'] exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) - _ = of _ k.1 (of _ k.2 x) := by - rw [sigmaCurry_of] + _ = of _ k.1 (of _ k.2 x) := sigmaCurry_of _ _ end SigmaFiber From f6c69a14c4cd1ed6df993b3e02a776a94e89f934 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Wed, 24 Jun 2026 09:49:56 +0200 Subject: [PATCH 17/27] adapt spacing Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 8cdfa65dd7adec..de8c6af732a064 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -346,7 +346,7 @@ theorem sigmaCurry_apply (f : ⨁ i : Σ _i, _, δ i.1 i.2) (i : ι) (j : α i) DFinsupp.sigmaCurry_apply (δ := δ) _ i j @[simp] -theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i)(x : δ k.1 k.2) : +theorem sigmaCurry_of [∀ i : ι, DecidableEq (α i)] (k : (i : ι) × α i) (x : δ k.1 k.2) : sigmaCurry (of (fun k ↦ δ k.1 k.2) k x) = of (fun i' ↦ ⨁ (j' : α i'), δ i' j') k.1 (of (fun j' ↦ δ k.1 j') k.2 x) := DFinsupp.sigmaCurry_single k x From 25fbafa2dded41937fc93a99787adf9e466084ac Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 24 Jun 2026 09:55:06 +0200 Subject: [PATCH 18/27] replace explicit use of sigmaCurry_of with simp call --- Mathlib/Algebra/DirectSum/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index de8c6af732a064..7b9e5a64ae0028 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -8,7 +8,6 @@ module public import Mathlib.Algebra.Group.Submonoid.Operations public import Mathlib.Data.DFinsupp.Sigma public import Mathlib.Data.DFinsupp.Submonoid - /-! # Direct sum @@ -396,7 +395,7 @@ theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by rw [sigmaFiberAddEquiv_apply'] exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) - _ = of _ k.1 (of _ k.2 x) := sigmaCurry_of _ _ + _ = of _ k.1 (of _ k.2 x) := by simp end SigmaFiber From d3ae57eb41cda2cc27c0d2e718ad7665f467d6d5 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 24 Jun 2026 12:22:17 +0200 Subject: [PATCH 19/27] reintroduce line break deleted by accidenent --- Mathlib/Algebra/DirectSum/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 7b9e5a64ae0028..922b0d9e6a2461 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Group.Submonoid.Operations public import Mathlib.Data.DFinsupp.Sigma public import Mathlib.Data.DFinsupp.Submonoid + /-! # Direct sum From 9808ab6c6b6c314acb258ce601bff4c490764766 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 24 Jun 2026 12:26:42 +0200 Subject: [PATCH 20/27] adjust spacing of doc string in line with other review suggestions --- Mathlib/Algebra/DirectSum/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 922b0d9e6a2461..fd53e063f6b7b3 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -374,8 +374,8 @@ section SigmaFiber variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] -/-- The equivalence between a direct sum indexed by a type `ι₁` and the - double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ +/-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type + `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) From 112d49991159cc7844c87a8acf5c5228f22cf89f Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Wed, 24 Jun 2026 12:28:49 +0200 Subject: [PATCH 21/27] further adjust docstring spacing --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index fd53e063f6b7b3..cb285de44138fd 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -375,7 +375,7 @@ variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] /-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type - `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ +`ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) From 13ec498e06372f4d4424b0d9b57d5296547c48c5 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Sat, 27 Jun 2026 20:00:53 +0200 Subject: [PATCH 22/27] adapt spacing Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index cb285de44138fd..425dbe4df2219b 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -385,7 +385,7 @@ theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : @[simp] theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : - sigmaFiberAddEquiv f x j i' = x i' := rfl + sigmaFiberAddEquiv f x j i' = x i' := rfl @[simp] theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : From 4d5c061601f4a3c7a37b2dbca233ce4af77ef17b Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Sat, 27 Jun 2026 20:04:08 +0200 Subject: [PATCH 23/27] =?UTF-8?q?rename=20=E2=80=A6apply'=20->=20=E2=80=A6?= =?UTF-8?q?apply;=20=E2=80=A6apply=20->=20=E2=80=A6apply=5Fapply?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/DirectSum/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 425dbe4df2219b..1d66b682b95d17 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -380,11 +380,11 @@ def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i))) -theorem sigmaFiberAddEquiv_apply' (x : ⨁ i, β i) : +theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) : sigmaFiberAddEquiv f x = sigmaCurry (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm x) := rfl @[simp] -theorem sigmaFiberAddEquiv_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : +theorem sigmaFiberAddEquiv_apply_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : ι₁ // f i = j}) : sigmaFiberAddEquiv f x j i' = x i' := rfl @[simp] @@ -394,7 +394,7 @@ theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ calc sigmaFiberAddEquiv f (of β (h k) x) _ = sigmaCurry (of (fun k : (j' : ι₂) × {i // f i = j'} ↦ β k.2) k x) := by - rw [sigmaFiberAddEquiv_apply'] + rw [sigmaFiberAddEquiv_apply] exact congrArg sigmaCurry (equivCongrLeft_of (h := h.symm) _ _) _ = of _ k.1 (of _ k.2 x) := by simp From 69a178710e6e718c5db3af839420f5e19c3bc2e3 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Sun, 28 Jun 2026 23:32:24 +0200 Subject: [PATCH 24/27] =?UTF-8?q?shorten=20'=E2=88=80=20i=20:=20=CE=B9?= =?UTF-8?q?=E2=82=81'=20to=20'=E2=88=80=20i'?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 1d66b682b95d17..79a1226a603ce0 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -372,7 +372,7 @@ end Sigma section SigmaFiber variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) -variable {β : ι₁ → Type w} [∀ i : ι₁, AddCommMonoid (β i)] +variable {β : ι₁ → Type w} [∀ i, AddCommMonoid (β i)] /-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ From 6b1bc34af95cb1dd5db0b1059a6e4a780040eafb Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Sun, 28 Jun 2026 23:34:29 +0200 Subject: [PATCH 25/27] don't need initial "by" in pure calc proof Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 79a1226a603ce0..9874ca7117259e 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -389,7 +389,7 @@ theorem sigmaFiberAddEquiv_apply_apply (x : ⨁ i, β i) (j : ι₂) (i' : { i : @[simp] theorem sigmaFiberAddEquiv_of [DecidableEq ι₁] (i : ι₁) (x : β i) : - sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := by + sigmaFiberAddEquiv f (of _ i x) = of _ (f i) (of _ ⟨i, rfl⟩ x) := let h := Equiv.sigmaFiberEquiv f let k : (j : ι₂) × {i₁ : ι₁ // f i₁ = j} := ⟨f i, ⟨i, rfl⟩⟩ calc sigmaFiberAddEquiv f (of β (h k) x) From cdfcc16a2151dd9edad711f7b0814bc6e90ec1c5 Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Mon, 29 Jun 2026 15:31:19 +0200 Subject: [PATCH 26/27] change \forall to \Pi --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 9874ca7117259e..7ca0675a12e894 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -372,7 +372,7 @@ end Sigma section SigmaFiber variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) -variable {β : ι₁ → Type w} [∀ i, AddCommMonoid (β i)] +variable {β : ι₁ → Type w} [Π i, AddCommMonoid (β i)] /-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type `ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ From fb1a532e681bd6c0f44375d519c4deb2215f828f Mon Sep 17 00:00:00 2001 From: TentativeConvert Date: Tue, 14 Jul 2026 15:20:52 +0200 Subject: [PATCH 27/27] improve readability of docstring following a suggestion by Jon Eugster --- Mathlib/Algebra/DirectSum/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean index 7ca0675a12e894..25a7ca4e92fa0f 100644 --- a/Mathlib/Algebra/DirectSum/Basic.lean +++ b/Mathlib/Algebra/DirectSum/Basic.lean @@ -375,7 +375,7 @@ variable {ι₁ ι₂ : Type v} [DecidableEq ι₂] (f : ι₁ → ι₂) variable {β : ι₁ → Type w} [Π i, AddCommMonoid (β i)] /-- The equivalence between a direct sum indexed by a type `ι₁` and the double sum indexed by a type -`ι₂` and the fibres of a map `f : ι₁ → ι₂`. -/ +`ι₂` together with the fibres of a map `f : ι₁ → ι₂`. -/ def sigmaFiberAddEquiv : (⨁ i, β i) ≃+ ⨁ (j : ι₂) (i : { i : ι₁ // f i = j}), β ↑i := (equivCongrLeft (Equiv.sigmaFiberEquiv f).symm).trans (sigmaCurryEquiv (δ := fun j ↦ (fun (i : { i : ι₁ // f i = j}) ↦ β i)))