From f090ba3ce77cf5cf271bd87b91ea4ffa0490b4d6 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Sat, 30 Nov 2024 00:51:14 -0500 Subject: [PATCH 1/3] finSigmaFinEquiv and friends --- Mathlib/Algebra/BigOperators/Fin.lean | 11 +++++++++ Mathlib/Logic/Equiv/Basic.lean | 32 ++++++++++++++++++++++++++- 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean index f336a553c7f57..fe79239972270 100644 --- a/Mathlib/Algebra/BigOperators/Fin.lean +++ b/Mathlib/Algebra/BigOperators/Fin.lean @@ -388,6 +388,17 @@ theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] rintro x hx rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul] +/-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`. -/ +def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i) := + match m with + | 0 => @Equiv.equivOfIsEmpty _ _ _ (by simp; exact Fin.isEmpty') + | Nat.succ m => + calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm + _ ≃ _ := Equiv.sumSigmaDistrib _ + _ ≃ _ := finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma _) + _ ≃ _ := finSumFinEquiv + _ ≃ _ := finCongr (Fin.sum_univ_castSucc n).symm + namespace List section CommMonoid diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index 070edf6a55b4e..584ba9a530f75 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -215,6 +215,23 @@ theorem sigmaUnique_symm_apply {α} {β : α → Type*} [∀ a, Unique (β a)] ( (sigmaUnique α β).symm x = ⟨x, default⟩ := rfl +/-- Any `Unique` type is a left identity for type sigma up to equivalence. Compare with `uniqueProd` +which is non-dependent. -/ +def uniqueSigma {α} (β : α → Type*) [Unique α] : (i:α) × β i ≃ β default := + ⟨fun p ↦ (Unique.eq_default _).rec p.2, + fun b ↦ ⟨default, b⟩, + fun _ ↦ Sigma.ext (Unique.default_eq _) (eqRec_heq _ _), + fun _ ↦ rfl⟩ + +theorem uniqueSigma_apply {α} {β : α → Type*} [Unique α] (x : (a : α) × β a) : + uniqueSigma β x = (Unique.eq_default _).rec x.2 := + rfl + +@[simp] +theorem uniqueSigma_symm_apply {α} {β : α → Type*} [Unique α] (y : β default) : + (uniqueSigma β).symm y = ⟨default, y⟩ := + rfl + /-- `Empty` type is a right absorbing element for type product up to an equivalence. -/ def prodEmpty (α) : α × Empty ≃ Empty := equivEmpty _ @@ -919,7 +936,8 @@ theorem prodSumDistrib_symm_apply_right {α β γ} (a : α × γ) : (prodSumDistrib α β γ).symm (inr a) = (a.1, inr a.2) := rfl -/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. -/ +/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare +with `Equiv.sumSigmaDistrib` which is indexed by sums. -/ @[simps] def sigmaSumDistrib {ι} (α β : ι → Type*) : (Σ i, α i ⊕ β i) ≃ (Σ i, α i) ⊕ (Σ i, β i) := @@ -927,6 +945,18 @@ def sigmaSumDistrib {ι} (α β : ι → Type*) : Sum.elim (Sigma.map id fun _ => Sum.inl) (Sigma.map id fun _ => Sum.inr), fun p => by rcases p with ⟨i, a | b⟩ <;> rfl, fun p => by rcases p with (⟨i, a⟩ | ⟨i, b⟩) <;> rfl⟩ +/-- A type indexed by disjoint sums of types is equivalent to the sum of the sums. Compare with +`Equiv.sigmaSumDistrib` which has the sums as the output type. -/ +@[simps] +def sumSigmaDistrib {α β} (t : α ⊕ β → Type*) : + (Σ i, t i) ≃ (Σ i, t (.inl i)) ⊕ (Σ i, t (.inr i)) := + ⟨(match · with + | .mk (.inl x) y => .inl ⟨x, y⟩ + | .mk (.inr x) y => .inr ⟨x, y⟩), + Sum.elim (fun a ↦ ⟨.inl a.1, a.2⟩) (fun b ↦ ⟨.inr b.1, b.2⟩), + by rintro ⟨x|x,y⟩ <;> simp, + by rintro (⟨x,y⟩|⟨x,y⟩) <;> simp⟩ + /-- The product of an indexed sum of types (formally, a `Sigma`-type `Σ i, α i`) by a type `β` is equivalent to the sum of products `Σ i, (α i × β)`. -/ @[simps apply symm_apply] From a19b012ef3ef69797038fb6280b48708159e19e3 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Mon, 9 Dec 2024 12:30:48 -0500 Subject: [PATCH 2/3] Add 'finSigmaFinEquiv_apply' --- Mathlib/Algebra/BigOperators/Fin.lean | 39 +++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean index fe79239972270..05d96ed43bfa3 100644 --- a/Mathlib/Algebra/BigOperators/Fin.lean +++ b/Mathlib/Algebra/BigOperators/Fin.lean @@ -399,6 +399,45 @@ def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) _ ≃ _ := finSumFinEquiv _ ≃ _ := finCongr (Fin.sum_univ_castSucc n).symm +@[simp] +theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) : + (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2 := by + induction m + · exact k.fst.elim0 + rename_i m ih + rcases k with ⟨⟨iv,hi⟩,j⟩ + rw [finSigmaFinEquiv] + unfold finSumFinEquiv + simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans, + Equiv.trans_apply, finCongr_apply, Fin.coe_cast] + generalize_proofs + rename_i pf1 _ + by_cases him : iv < m + · have : (Sigma.mk (β := (fun a ↦ Fin (n (Sum.elim _ _ a)))) _ + (pf1.rec (motive := fun x _ ↦ Fin (n x)) j) = ⟨.inl (@Fin.mk m iv him), j⟩) := by + simp [Fin.addCases, him] + conv => + enter [1,1,3] + apply Equiv.sumCongr_apply + simpa [this] using ih _ + · replace him := Nat.eq_of_lt_succ_of_not_lt hi him + subst him + obtain ⟨w, this⟩ : ∃ (w : Eq _ (Fin (n ((Sum.inr 0).elim _ _)))), + (Sigma.mk (β := (fun a ↦ Fin (n _))) _ + (pf1.rec (motive := fun x _ ↦ Fin (n x)) j) = ⟨_, w.rec j⟩) := by + simp [Fin.addCases, Fin.natAdd] + conv => + enter [1,1,3] + apply Equiv.sumCongr_apply + simp [this] + congr + +/-- `finSigmaFinEquiv` on `Fin 1 × f` is just `f`-/ +theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : + (finSigmaFinEquiv ij : ℕ) = ij.2 := by + rw [finSigmaFinEquiv_apply, add_left_eq_self] + apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty') + namespace List section CommMonoid From 9fcfebfbc18acdbd5220478b49a1319657a91830 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Mon, 9 Dec 2024 14:07:30 -0500 Subject: [PATCH 3/3] golf --- Mathlib/Algebra/BigOperators/Fin.lean | 28 ++++++++++----------------- 1 file changed, 10 insertions(+), 18 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean index 05d96ed43bfa3..37a8d3d507e47 100644 --- a/Mathlib/Algebra/BigOperators/Fin.lean +++ b/Mathlib/Algebra/BigOperators/Fin.lean @@ -410,27 +410,19 @@ theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × unfold finSumFinEquiv simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans, Equiv.trans_apply, finCongr_apply, Fin.coe_cast] - generalize_proofs - rename_i pf1 _ + conv => + enter [1,1,3] + apply Equiv.sumCongr_apply by_cases him : iv < m - · have : (Sigma.mk (β := (fun a ↦ Fin (n (Sum.elim _ _ a)))) _ - (pf1.rec (motive := fun x _ ↦ Fin (n x)) j) = ⟨.inl (@Fin.mk m iv him), j⟩) := by - simp [Fin.addCases, him] - conv => - enter [1,1,3] - apply Equiv.sumCongr_apply - simpa [this] using ih _ + · conv in Sigma.mk _ _ => + equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him] + simpa using ih _ · replace him := Nat.eq_of_lt_succ_of_not_lt hi him subst him - obtain ⟨w, this⟩ : ∃ (w : Eq _ (Fin (n ((Sum.inr 0).elim _ _)))), - (Sigma.mk (β := (fun a ↦ Fin (n _))) _ - (pf1.rec (motive := fun x _ ↦ Fin (n x)) j) = ⟨_, w.rec j⟩) := by - simp [Fin.addCases, Fin.natAdd] - conv => - enter [1,1,3] - apply Equiv.sumCongr_apply - simp [this] - congr + conv in Sigma.mk _ _ => + equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd] + simp + rfl /-- `finSigmaFinEquiv` on `Fin 1 × f` is just `f`-/ theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) :