From ab065896c9de4aab1d0034d7ee5086b74d50f3bf Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 6 Sep 2024 14:45:23 +0000 Subject: [PATCH 01/11] feat(Algebra/BigOperators): add lemmas for product of MulHom over nonempty list --- Mathlib/Algebra/BigOperators/Group/List.lean | 21 ++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean index 8f96d4c7f7dbb1..bf6980cd573d96 100644 --- a/Mathlib/Algebra/BigOperators/Group/List.lean +++ b/Mathlib/Algebra/BigOperators/Group/List.lean @@ -137,24 +137,29 @@ theorem rel_prod {R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (· * (Forall₂ R ⇒ R) prod prod := rel_foldl hf h +@[to_additive] +theorem prod_hom_nonempty {l : List M} {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F) + (hl : l ≠ []) : (l.map f).prod = f l.prod := + match l, hl with | x :: xs, hl => by induction xs generalizing x <;> aesop + @[to_additive] theorem prod_hom (l : List M) {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) : (l.map f).prod = f l.prod := by simp only [prod, foldl_map, ← map_one f] exact l.foldl_hom f (· * ·) (· * f ·) 1 (fun x y => (map_mul f x y).symm) +@[to_additive] +theorem prod_hom₂_nonempty {l : List ι} (f : M → N → P) + (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) (hl : l ≠ []) : + (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by + match l, hl with | x :: xs, hl => induction xs generalizing x <;> aesop + @[to_additive] theorem prod_hom₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) : (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by - simp only [prod, foldl_map] - -- Porting note: next 3 lines used to be - -- convert l.foldl_hom₂ (fun a b => f a b) _ _ _ _ _ fun a b i => _ - -- · exact hf'.symm - -- · exact hf _ _ _ _ - rw [← l.foldl_hom₂ (fun a b => f a b), hf'] - intros - exact hf _ _ _ _ + rw [prod, prod, prod, foldl_map, foldl_map, foldl_map, + ← l.foldl_hom₂ f _ _ (fun x y => x * f (f₁ y) (f₂ y)) _ _ (by simp [hf]), hf'] @[to_additive (attr := simp)] theorem prod_map_mul {α : Type*} [CommMonoid α] {l : List ι} {f g : ι → α} : From 0b56c05d8670a88c4489c58344905d863ac888c5 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 6 Sep 2024 14:55:38 +0000 Subject: [PATCH 02/11] wip stuff --- .../Algebra/BigOperators/Group/Multiset.lean | 11 ++ .../Combinatorics/Additive/FreimanHom.lean | 113 ++++++++++++++++-- 2 files changed, 117 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset.lean b/Mathlib/Algebra/BigOperators/Group/Multiset.lean index 0d5d2fc6e95eae..0ee8838bbecc0d 100644 --- a/Mathlib/Algebra/BigOperators/Group/Multiset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Multiset.lean @@ -128,6 +128,12 @@ theorem prod_hom (s : Multiset α) {F : Type*} [FunLike F α β] (s.map f).prod = f s.prod := Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe] +@[to_additive] +theorem prod_hom_ne_zero {s : Multiset α} (hs : s ≠ 0) {F : Type*} [FunLike F α β] + [MulHomClass F α β] (f : F) : + (s.map f).prod = f s.prod := by + induction s using Quot.inductionOn; aesop (add simp List.prod_hom_nonempty) + @[to_additive] theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F α β] [MonoidHomClass F α β] (f : F) @@ -194,6 +200,11 @@ theorem prod_dvd_prod_of_le (h : s ≤ t) : s.prod ∣ t.prod := by lemma _root_.map_multiset_prod [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f s.prod = (s.map f).prod := (s.prod_hom f).symm +@[to_additive] +lemma _root_.map_multiset_prod_ne_zero [FunLike F α β] [MulHomClass F α β] (f : F) + {s : Multiset α} (hs : s ≠ 0): + f s.prod = (s.map f).prod := (s.prod_hom_ne_zero hs f).symm + @[to_additive] protected lemma _root_.MonoidHom.map_multiset_prod (f : α →* β) (s : Multiset α) : f s.prod = (s.map f).prod := (s.prod_hom f).symm diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index e3069dafec32ab..7ae75aa8d14724 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -18,13 +18,17 @@ An `n`-Freiman homomorphism from `A` to `B` is a function `f : α → β` such t `f x₁ * ... * f xₙ = f y₁ * ... * f yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A` such that `x₁ * ... * xₙ = y₁ * ... * yₙ`. In particular, any `MulHom` is a Freiman homomorphism. +Note a `0`- or `1`-Freiman homomorphism is simply a map, thus a `2`-Freiman homomorphism is the +first interesting case (and the most common). As `n` increases further, the property of being +an `n`-Freiman homomorphism between abelian groups becomes increasingly stronger. + An `n`-Freiman isomorphism from `A` to `B` is a function `f : α → β` bijective between `A` and `B` such that `f x₁ * ... * f xₙ = f y₁ * ... * f yₙ ↔ x₁ * ... * xₙ = y₁ * ... * yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A`. In particular, any `MulEquiv` is a Freiman isomorphism. They are of interest in additive combinatorics. -## Main declaration +## Main declarations * `IsMulFreimanHom`: Predicate for a function to be a multiplicative Freiman homomorphism. * `IsAddFreimanHom`: Predicate for a function to be an additive Freiman homomorphism. @@ -102,6 +106,46 @@ lemma IsMulFreimanIso.isMulFreimanHom (hf : IsMulFreimanIso n A B f) : IsMulFrei mapsTo := hf.bijOn.mapsTo map_prod_eq_map_prod _s _t hsA htA hs ht := (hf.map_prod_eq_map_prod hsA htA hs ht).2 +/-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality. -/ +@[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} + {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} + (hs : s.card = n) (ht : t.card = n) : + ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i in s, f i = ∏ i in t, f i := by + simpa using hf.map_prod_eq_map_prod hsA htA hs ht + +/-- +If the inverse of a Freiman homomorphism is itself a Freiman homomorphism, then it is a Freiman +isomorphism. +-/ +@[to_additive] +lemma IsMulFreimanHom.toIsMulFreimanIso {g : β → α} (h : InvOn g f A B) + (hf : IsMulFreimanHom n A B f) (hg : IsMulFreimanHom n B A g) : + IsMulFreimanIso n A B f where + bijOn := h.bijOn hf.mapsTo hg.mapsTo + map_prod_eq_map_prod s t hsA htA hs ht := by + constructor + case mp => + intro h' + have hsB : ∀ ⦃x : β⦄, x ∈ map f s → x ∈ B := by + simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] + intro x hx + exact hf.mapsTo (hsA hx) + have htB : ∀ ⦃x : β⦄, x ∈ map f t → x ∈ B := by + simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] + intro x hx + exact hf.mapsTo (htA hx) + have := hg.map_prod_eq_map_prod hsB htB (by simp [hs]) (by simp [ht]) h' + rwa [map_map, map_map, map_congr rfl ?g1, map_id, map_congr rfl ?g2, map_id] at this + case g1 => + intro x hx + exact h.1 (hsA hx) + case g2 => + intro x hx + exact h.1 (htA hx) + case mpr => + intro h' + exact hf.map_prod_eq_map_prod hsA htA hs ht h' + @[to_additive] lemma IsMulFreimanHom.mul_eq_mul (hf : IsMulFreimanHom 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) : @@ -171,6 +215,28 @@ lemma isMulFreimanHom_const {b : β} (hb : b ∈ B) : IsMulFreimanHom n A B fun mapsTo _ _ := hb map_prod_eq_map_prod s t _ _ hs ht _ := by simp only [map_const', hs, prod_replicate, ht] +@[to_additive (attr := simp)] +lemma isMulFreimanHom_zero_iff : IsMulFreimanHom 0 A B f ↔ MapsTo f A B := + ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop⟩⟩ + +@[to_additive (attr := simp)] +lemma isMulFreimanIso_zero_iff : IsMulFreimanIso 0 A B f ↔ BijOn f A B := + ⟨fun h => h.bijOn, fun h => ⟨h, by aesop⟩⟩ + +@[to_additive (attr := simp) isAddFreimanHom_one_iff] +lemma isMulFreimanHom_one_iff : IsMulFreimanHom 1 A B f ↔ MapsTo f A B := + ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop (add simp card_eq_one)⟩⟩ + +@[to_additive (attr := simp) isAddFreimanIso_one_iff] +lemma isMulFreimanIso_one_iff : IsMulFreimanIso 1 A B f ↔ BijOn f A B := + ⟨fun h => h.bijOn, fun h => ⟨h, by aesop (add simp [card_eq_one, BijOn])⟩⟩ + +@[to_additive (attr := simp)] +lemma isMulFreimanHom_empty : IsMulFreimanHom n (∅ : Set α) B f where + mapsTo := mapsTo_empty f B + map_prod_eq_map_prod s t hs ht := by + simp [eq_zero_of_forall_not_mem hs, eq_zero_of_forall_not_mem ht] + @[to_additive (attr := simp)] lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f where bijOn := bijOn_empty _ @@ -185,10 +251,31 @@ lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] -@[to_additive] lemma MonoidHomClass.isMulFreimanHom [FunLike F α β] [MonoidHomClass F α β] (f : F) - (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f where - mapsTo := hfAB - map_prod_eq_map_prod s t _ _ _ _ h := by rw [← map_multiset_prod, h, map_multiset_prod] +theorem List.length_eq_succ {α : Type*} {n} {l : List α} : + l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by cases l <;> aesop + +lemma coe_cons {α : Type*} {h : α} {t : List α} : + (h :: t : Multiset α) = h ::ₘ t := by simp only [cons_coe] + +theorem card_eq_succ {α : Type*} {s : Multiset α} : + card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by + constructor + case mp => + induction s using Quot.inductionOn + case h s => + simp only [quot_mk_to_coe'', coe_card, List.length_eq_succ, forall_exists_index, and_imp] + rintro a s rfl rfl + exact ⟨a, s, rfl, rfl⟩ + case mpr => + rintro ⟨_, _, rfl, rfl⟩ + simp + +@[to_additive] lemma MulHomClass.isMulFreimanHom [FunLike F α β] [MulHomClass F α β] (f : F) + (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f := + match n with + | 0 => by simpa + | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => + by rw [← map_multiset_prod_ne_zero _ (by aesop), h, map_multiset_prod_ne_zero _ (by aesop)] @[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where @@ -284,11 +371,21 @@ lemma IsMulFreimanHom.inv (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A B end DivisionCommMonoid section Prod + +section + +variable {α β₁ β₂ : Type*} [CommMonoid α] [CommMonoid β₁] [CommMonoid β₂] + {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ} + +end + +section + variable {α₁ α₂ β₁ β₂ : Type*} [CommMonoid α₁] [CommMonoid α₂] [CommMonoid β₁] [CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} @[to_additive] -lemma IsMulFreimanHom.prod (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : +lemma IsMulFreimanHom.prodMap (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where mapsTo := h₁.mapsTo.prodMap h₂.mapsTo map_prod_eq_map_prod s t hsA htA hs ht h := by @@ -301,7 +398,7 @@ lemma IsMulFreimanHom.prod (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsM (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa) h.2⟩ @[to_additive] -lemma IsMulFreimanIso.prod (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : +lemma IsMulFreimanIso.prodMap (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where bijOn := h₁.bijOn.prodMap h₂.bijOn map_prod_eq_map_prod s t hsA htA hs ht := by @@ -313,6 +410,8 @@ lemma IsMulFreimanIso.prod (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsM h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa)] +end + end Prod namespace Fin From 5af0ffc333fb0200c494bc04e401fb0f3d524da7 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 6 Sep 2024 14:55:38 +0000 Subject: [PATCH 03/11] wip stuff --- .../Algebra/BigOperators/Group/Multiset.lean | 11 ++ .../Combinatorics/Additive/FreimanHom.lean | 130 +++++++++++++++--- 2 files changed, 124 insertions(+), 17 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset.lean b/Mathlib/Algebra/BigOperators/Group/Multiset.lean index 0d5d2fc6e95eae..0ee8838bbecc0d 100644 --- a/Mathlib/Algebra/BigOperators/Group/Multiset.lean +++ b/Mathlib/Algebra/BigOperators/Group/Multiset.lean @@ -128,6 +128,12 @@ theorem prod_hom (s : Multiset α) {F : Type*} [FunLike F α β] (s.map f).prod = f s.prod := Quotient.inductionOn s fun l => by simp only [l.prod_hom f, quot_mk_to_coe, map_coe, prod_coe] +@[to_additive] +theorem prod_hom_ne_zero {s : Multiset α} (hs : s ≠ 0) {F : Type*} [FunLike F α β] + [MulHomClass F α β] (f : F) : + (s.map f).prod = f s.prod := by + induction s using Quot.inductionOn; aesop (add simp List.prod_hom_nonempty) + @[to_additive] theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F α β] [MonoidHomClass F α β] (f : F) @@ -194,6 +200,11 @@ theorem prod_dvd_prod_of_le (h : s ≤ t) : s.prod ∣ t.prod := by lemma _root_.map_multiset_prod [FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Multiset α) : f s.prod = (s.map f).prod := (s.prod_hom f).symm +@[to_additive] +lemma _root_.map_multiset_prod_ne_zero [FunLike F α β] [MulHomClass F α β] (f : F) + {s : Multiset α} (hs : s ≠ 0): + f s.prod = (s.map f).prod := (s.prod_hom_ne_zero hs f).symm + @[to_additive] protected lemma _root_.MonoidHom.map_multiset_prod (f : α →* β) (s : Multiset α) : f s.prod = (s.map f).prod := (s.prod_hom f).symm diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index e3069dafec32ab..8af8748aa21863 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -18,13 +18,17 @@ An `n`-Freiman homomorphism from `A` to `B` is a function `f : α → β` such t `f x₁ * ... * f xₙ = f y₁ * ... * f yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A` such that `x₁ * ... * xₙ = y₁ * ... * yₙ`. In particular, any `MulHom` is a Freiman homomorphism. +Note a `0`- or `1`-Freiman homomorphism is simply a map, thus a `2`-Freiman homomorphism is the +first interesting case (and the most common). As `n` increases further, the property of being +an `n`-Freiman homomorphism between abelian groups becomes increasingly stronger. + An `n`-Freiman isomorphism from `A` to `B` is a function `f : α → β` bijective between `A` and `B` such that `f x₁ * ... * f xₙ = f y₁ * ... * f yₙ ↔ x₁ * ... * xₙ = y₁ * ... * yₙ` for all `x₁, ..., xₙ, y₁, ..., yₙ ∈ A`. In particular, any `MulEquiv` is a Freiman isomorphism. They are of interest in additive combinatorics. -## Main declaration +## Main declarations * `IsMulFreimanHom`: Predicate for a function to be a multiplicative Freiman homomorphism. * `IsAddFreimanHom`: Predicate for a function to be an additive Freiman homomorphism. @@ -102,6 +106,32 @@ lemma IsMulFreimanIso.isMulFreimanHom (hf : IsMulFreimanIso n A B f) : IsMulFrei mapsTo := hf.bijOn.mapsTo map_prod_eq_map_prod _s _t hsA htA hs ht := (hf.map_prod_eq_map_prod hsA htA hs ht).2 +/-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality. -/ +@[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} + {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} + (hs : s.card = n) (ht : t.card = n) : + ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i in s, f i = ∏ i in t, f i := by + simpa using hf.map_prod_eq_map_prod hsA htA hs ht + +/-- +If the inverse of a Freiman homomorphism is itself a Freiman homomorphism, then it is a Freiman +isomorphism. +-/ +@[to_additive] +lemma IsMulFreimanHom.toIsMulFreimanIso {g : β → α} (h : InvOn g f A B) + (hf : IsMulFreimanHom n A B f) (hg : IsMulFreimanHom n B A g) : + IsMulFreimanIso n A B f where + bijOn := h.bijOn hf.mapsTo hg.mapsTo + map_prod_eq_map_prod s t hsA htA hs ht := by + refine ⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩ + have : (map g (map f s)).prod = (map g (map f t)).prod := by + have := hf.mapsTo + refine hg.map_prod_eq_map_prod ?_ ?_ ?_ ?_ h' <;> aesop (add simp MapsTo) + rwa [map_map, map_congr rfl fun x hx => ?g1, map_id, + map_map, map_congr rfl fun x hx => ?g2, map_id] at this + case g1 => exact h.1 (hsA hx) + case g2 => exact h.1 (htA hx) + @[to_additive] lemma IsMulFreimanHom.mul_eq_mul (hf : IsMulFreimanHom 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) : @@ -171,6 +201,28 @@ lemma isMulFreimanHom_const {b : β} (hb : b ∈ B) : IsMulFreimanHom n A B fun mapsTo _ _ := hb map_prod_eq_map_prod s t _ _ hs ht _ := by simp only [map_const', hs, prod_replicate, ht] +@[to_additive (attr := simp)] +lemma isMulFreimanHom_zero_iff : IsMulFreimanHom 0 A B f ↔ MapsTo f A B := + ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop⟩⟩ + +@[to_additive (attr := simp)] +lemma isMulFreimanIso_zero_iff : IsMulFreimanIso 0 A B f ↔ BijOn f A B := + ⟨fun h => h.bijOn, fun h => ⟨h, by aesop⟩⟩ + +@[to_additive (attr := simp) isAddFreimanHom_one_iff] +lemma isMulFreimanHom_one_iff : IsMulFreimanHom 1 A B f ↔ MapsTo f A B := + ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop (add simp card_eq_one)⟩⟩ + +@[to_additive (attr := simp) isAddFreimanIso_one_iff] +lemma isMulFreimanIso_one_iff : IsMulFreimanIso 1 A B f ↔ BijOn f A B := + ⟨fun h => h.bijOn, fun h => ⟨h, by aesop (add simp [card_eq_one, BijOn])⟩⟩ + +@[to_additive (attr := simp)] +lemma isMulFreimanHom_empty : IsMulFreimanHom n (∅ : Set α) B f where + mapsTo := mapsTo_empty f B + map_prod_eq_map_prod s t hs ht := by + simp [eq_zero_of_forall_not_mem hs, eq_zero_of_forall_not_mem ht] + @[to_additive (attr := simp)] lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f where bijOn := bijOn_empty _ @@ -185,10 +237,31 @@ lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] -@[to_additive] lemma MonoidHomClass.isMulFreimanHom [FunLike F α β] [MonoidHomClass F α β] (f : F) - (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f where - mapsTo := hfAB - map_prod_eq_map_prod s t _ _ _ _ h := by rw [← map_multiset_prod, h, map_multiset_prod] +theorem List.length_eq_succ {α : Type*} {n} {l : List α} : + l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by cases l <;> aesop + +lemma coe_cons {α : Type*} {h : α} {t : List α} : + (h :: t : Multiset α) = h ::ₘ t := by simp only [cons_coe] + +theorem card_eq_succ {α : Type*} {s : Multiset α} : + card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by + constructor + case mp => + induction s using Quot.inductionOn + case h s => + simp only [quot_mk_to_coe'', coe_card, List.length_eq_succ, forall_exists_index, and_imp] + rintro a s rfl rfl + exact ⟨a, s, rfl, rfl⟩ + case mpr => + rintro ⟨_, _, rfl, rfl⟩ + simp + +@[to_additive] lemma MulHomClass.isMulFreimanHom [FunLike F α β] [MulHomClass F α β] (f : F) + (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f := + match n with + | 0 => by simpa + | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => + by rw [← map_multiset_prod_ne_zero _ (by aesop), h, map_multiset_prod_ne_zero _ (by aesop)] @[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where @@ -284,24 +357,45 @@ lemma IsMulFreimanHom.inv (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A B end DivisionCommMonoid section Prod + +@[to_additive] +lemma IsMulFreimanHom.fst [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : + IsMulFreimanHom n (A ×ˢ B) A Prod.fst := + MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) (by aesop (add simp MapsTo)) + +@[to_additive] +lemma IsMulFreimanHom.snd [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : + IsMulFreimanHom n (A ×ˢ B) B Prod.snd := + MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) (by aesop (add simp MapsTo)) + +section + +variable {α β₁ β₂ : Type*} [CommMonoid α] [CommMonoid β₁] [CommMonoid β₂] + {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ} + +@[to_additive] +lemma IsMulFreimanHom.prodLift (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : + IsMulFreimanHom n A (B₁ ×ˢ B₂) (fun x => (f₁ x, f₂ x)) where + mapsTo := fun x hx => mk_mem_prod (h₁.mapsTo hx) (h₂.mapsTo hx) + map_prod_eq_map_prod s t hsA htA hs ht h := by + simp only [Prod.ext_iff, fst_prod, map_map, Function.comp_apply, snd_prod] + rw [h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] + trivial + +end + +section + variable {α₁ α₂ β₁ β₂ : Type*} [CommMonoid α₁] [CommMonoid α₂] [CommMonoid β₁] [CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} @[to_additive] -lemma IsMulFreimanHom.prod (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : - IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where - mapsTo := h₁.mapsTo.prodMap h₂.mapsTo - map_prod_eq_map_prod s t hsA htA hs ht h := by - simp only [mem_prod, forall_and, Prod.forall] at hsA htA - simp only [Prod.ext_iff, fst_prod, snd_prod, map_map, Function.comp_apply, Prod.map_fst, - Prod.map_snd] at h ⊢ - rw [← Function.comp_def, ← map_map, ← map_map, ← Function.comp_def f₂, ← map_map, ← map_map] - exact ⟨h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa) - (by simpa) h.1, h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) - (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa) h.2⟩ +lemma IsMulFreimanHom.prodMap (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : + IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) := + (h₁.comp IsMulFreimanHom.fst).prodLift (h₂.comp IsMulFreimanHom.snd) @[to_additive] -lemma IsMulFreimanIso.prod (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : +lemma IsMulFreimanIso.prodMap (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where bijOn := h₁.bijOn.prodMap h₂.bijOn map_prod_eq_map_prod s t hsA htA hs ht := by @@ -313,6 +407,8 @@ lemma IsMulFreimanIso.prod (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsM h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa)] +end + end Prod namespace Fin From 313c13c3c0f0e27fb2d78cdf19ec745c9b54dda7 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Fri, 6 Sep 2024 16:29:38 +0000 Subject: [PATCH 04/11] wips --- .../Combinatorics/Additive/FreimanHom.lean | 20 ++++++------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index 8af8748aa21863..c283908f20c8e2 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -220,8 +220,7 @@ lemma isMulFreimanIso_one_iff : IsMulFreimanIso 1 A B f ↔ BijOn f A B := @[to_additive (attr := simp)] lemma isMulFreimanHom_empty : IsMulFreimanHom n (∅ : Set α) B f where mapsTo := mapsTo_empty f B - map_prod_eq_map_prod s t hs ht := by - simp [eq_zero_of_forall_not_mem hs, eq_zero_of_forall_not_mem ht] + map_prod_eq_map_prod s t := by aesop (add simp eq_zero_of_forall_not_mem) @[to_additive (attr := simp)] lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f where @@ -240,28 +239,21 @@ lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f theorem List.length_eq_succ {α : Type*} {n} {l : List α} : l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by cases l <;> aesop -lemma coe_cons {α : Type*} {h : α} {t : List α} : - (h :: t : Multiset α) = h ::ₘ t := by simp only [cons_coe] - theorem card_eq_succ {α : Type*} {s : Multiset α} : card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by - constructor - case mp => - induction s using Quot.inductionOn - case h s => + refine ⟨?_, by aesop⟩ + induction s using Quot.inductionOn with + | h s => simp only [quot_mk_to_coe'', coe_card, List.length_eq_succ, forall_exists_index, and_imp] rintro a s rfl rfl exact ⟨a, s, rfl, rfl⟩ - case mpr => - rintro ⟨_, _, rfl, rfl⟩ - simp @[to_additive] lemma MulHomClass.isMulFreimanHom [FunLike F α β] [MulHomClass F α β] (f : F) (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f := match n with | 0 => by simpa - | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => - by rw [← map_multiset_prod_ne_zero _ (by aesop), h, map_multiset_prod_ne_zero _ (by aesop)] + | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => by + rw [← map_multiset_prod_ne_zero _ (by aesop), h, map_multiset_prod_ne_zero _ (by aesop)] @[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where From a08bacbfdcacc2e545953aacd28ccfafd61e20e2 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 7 Sep 2024 17:52:12 +0000 Subject: [PATCH 05/11] more bits --- .../Combinatorics/Additive/FreimanHom.lean | 138 +++++++++--------- Mathlib/Data/Set/Function.lean | 40 +++++ 2 files changed, 106 insertions(+), 72 deletions(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index c283908f20c8e2..cf9aecb852d4a6 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -106,12 +106,33 @@ lemma IsMulFreimanIso.isMulFreimanHom (hf : IsMulFreimanIso n A B f) : IsMulFrei mapsTo := hf.bijOn.mapsTo map_prod_eq_map_prod _s _t hsA htA hs ht := (hf.map_prod_eq_map_prod hsA htA hs ht).2 -/-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality. -/ -@[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} - {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} - (hs : s.card = n) (ht : t.card = n) : - ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i in s, f i = ∏ i in t, f i := by - simpa using hf.map_prod_eq_map_prod hsA htA hs ht +lemma IsMulFreimanHom.congr (hf₁ : IsMulFreimanHom n A B f₁) (h : EqOn f₁ f₂ A) : + IsMulFreimanHom n A B f₂ where + mapsTo := hf₁.mapsTo.congr h + map_prod_eq_map_prod s t hsA htA hs ht h' := by + rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm, + hf₁.map_prod_eq_map_prod hsA htA hs ht h'] + +lemma IsMulFreimanIso.congr (hf₁ : IsMulFreimanIso n A B f₁) (h : EqOn f₁ f₂ A) : + IsMulFreimanIso n A B f₂ where + bijOn := hf₁.bijOn.congr h + map_prod_eq_map_prod s t hsA htA hs ht := by + rw [map_congr rfl fun x hx => h.symm (hsA hx), map_congr rfl fun x hx => h.symm (htA hx), + hf₁.map_prod_eq_map_prod hsA htA hs ht] + +/-- +Given a Freiman isomorphism `f` from `A` to `B`, if `g` maps `B` into `A`, and is a right inverse +to `f` on `B`, then `g` is a Freiman isomorphism from `B` to `A`. +-/ +@[to_additive] +lemma IsMulFreimanIso.symm {g : β → α} (hg₁ : MapsTo g B A) (hg₂ : RightInvOn g f B) + (hf : IsMulFreimanIso n A B f) : + IsMulFreimanIso n B A g where + bijOn := hf.bijOn.symm ⟨hg₂, InjOn.rightInvOn_of_leftInvOn hf.bijOn.injOn hg₂ hf.bijOn.mapsTo hg₁⟩ + map_prod_eq_map_prod := fun s t hsB htB hs ht => by + rw [←hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id, + map_map, map_congr rfl, map_id] + all_goals aesop /-- If the inverse of a Freiman homomorphism is itself a Freiman homomorphism, then it is a Freiman @@ -132,6 +153,18 @@ lemma IsMulFreimanHom.toIsMulFreimanIso {g : β → α} (h : InvOn g f A B) case g1 => exact h.1 (hsA hx) case g2 => exact h.1 (htA hx) +@[to_additive] +lemma IsMulFreimanIso.isMulFreimanIso_invFunOn (hf : IsMulFreimanIso n A B f) : + IsMulFreimanIso n B A (f.invFunOn A) := + hf.symm hf.bijOn.surjOn.mapsTo_invFunOn hf.bijOn.surjOn.rightInvOn_invFunOn + +/-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality. -/ +@[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} + {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} + (hs : s.card = n) (ht : t.card = n) : + ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i in s, f i = ∏ i in t, f i := by + simpa using hf.map_prod_eq_map_prod hsA htA hs ht + @[to_additive] lemma IsMulFreimanHom.mul_eq_mul (hf : IsMulFreimanHom 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) (h : a * b = c * d) : @@ -267,31 +300,19 @@ section CancelCommMonoid variable [CommMonoid α] [CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {m n : ℕ} @[to_additive] -lemma IsMulFreimanHom.mono (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) : - IsMulFreimanHom m A B f where - mapsTo := hf.mapsTo - map_prod_eq_map_prod s t hsA htA hs ht h := by - obtain rfl | hm := m.eq_zero_or_pos - · rw [card_eq_zero] at hs ht - rw [hs, ht] - simp only [← hs, card_pos_iff_exists_mem] at hm - obtain ⟨a, ha⟩ := hm - suffices ((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod by - simp_rw [Multiset.map_add, prod_add] at this - exact mul_right_cancel this - replace ha := hsA ha - refine hf.map_prod_eq_map_prod (fun a ha ↦ ?_) (fun a ha ↦ ?_) ?_ ?_ ?_ - · rw [Multiset.mem_add] at ha - obtain ha | ha := ha - · exact hsA ha - · rwa [eq_of_mem_replicate ha] - · rw [Multiset.mem_add] at ha - obtain ha | ha := ha - · exact htA ha - · rwa [eq_of_mem_replicate ha] - · rw [_root_.map_add, card_replicate, hs, Nat.add_sub_cancel' hmn] - · rw [_root_.map_add, card_replicate, ht, Nat.add_sub_cancel' hmn] - · rw [prod_add, prod_add, h] +lemma isMulFreimanHom_antitone : Antitone (IsMulFreimanHom · A B f) := + antitone_nat_of_succ_le fun n hf => + { mapsTo := hf.mapsTo, + map_prod_eq_map_prod := fun s t hsA htA hs _ h => match n with + | 0 => by aesop + | n + 1 => + have ⟨a, ha⟩ : ∃ a, a ∈ s := card_pos_iff_exists_mem.1 (by simp [hs]) + by simpa [*] using hf.map_prod_eq_map_prod (s := a ::ₘ s) (t := a ::ₘ t) + (by simpa [hsA ha]) (by simpa [hsA ha]) } + +@[to_additive] +lemma IsMulFreimanHom.mono (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom m A B f := + isMulFreimanHom_antitone hmn hf end CancelCommMonoid @@ -300,30 +321,9 @@ variable [CancelCommMonoid α] [CancelCommMonoid β] {A : Set α} {B : Set β} { @[to_additive] lemma IsMulFreimanIso.mono {hmn : m ≤ n} (hf : IsMulFreimanIso n A B f) : - IsMulFreimanIso m A B f where - bijOn := hf.bijOn - map_prod_eq_map_prod s t hsA htA hs ht := by - obtain rfl | hm := m.eq_zero_or_pos - · rw [card_eq_zero] at hs ht - simp [hs, ht] - simp only [← hs, card_pos_iff_exists_mem] at hm - obtain ⟨a, ha⟩ := hm - suffices - ((s + replicate (n - m) a).map f).prod = ((t + replicate (n - m) a).map f).prod ↔ - (s + replicate (n - m) a).prod = (t + replicate (n - m) a).prod by - simpa only [Multiset.map_add, prod_add, mul_right_cancel_iff] using this - replace ha := hsA ha - refine hf.map_prod_eq_map_prod (fun a ha ↦ ?_) (fun a ha ↦ ?_) ?_ ?_ - · rw [Multiset.mem_add] at ha - obtain ha | ha := ha - · exact hsA ha - · rwa [eq_of_mem_replicate ha] - · rw [Multiset.mem_add] at ha - obtain ha | ha := ha - · exact htA ha - · rwa [eq_of_mem_replicate ha] - · rw [_root_.map_add, card_replicate, hs, Nat.add_sub_cancel' hmn] - · rw [_root_.map_add, card_replicate, ht, Nat.add_sub_cancel' hmn] + IsMulFreimanIso m A B f := + (hf.isMulFreimanHom.mono hmn).toIsMulFreimanIso hf.bijOn.invOn_invFunOn + (hf.isMulFreimanIso_invFunOn.isMulFreimanHom.mono hmn) end CancelCommMonoid @@ -353,12 +353,12 @@ section Prod @[to_additive] lemma IsMulFreimanHom.fst [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : IsMulFreimanHom n (A ×ˢ B) A Prod.fst := - MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) (by aesop (add simp MapsTo)) + MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) mapsTo_fst @[to_additive] lemma IsMulFreimanHom.snd [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : IsMulFreimanHom n (A ×ˢ B) B Prod.snd := - MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) (by aesop (add simp MapsTo)) + MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) mapsTo_snd section @@ -366,13 +366,12 @@ variable {α β₁ β₂ : Type*} [CommMonoid α] [CommMonoid β₁] [CommMonoid {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ} @[to_additive] -lemma IsMulFreimanHom.prodLift (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : +lemma IsMulFreimanHom.prodMk (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ ×ˢ B₂) (fun x => (f₁ x, f₂ x)) where mapsTo := fun x hx => mk_mem_prod (h₁.mapsTo hx) (h₂.mapsTo hx) map_prod_eq_map_prod s t hsA htA hs ht h := by - simp only [Prod.ext_iff, fst_prod, map_map, Function.comp_apply, snd_prod] - rw [h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] - trivial + simp [Prod.ext_iff, fst_prod, snd_prod, + h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] end @@ -384,20 +383,15 @@ variable {α₁ α₂ β₁ β₂ : Type*} [CommMonoid α₁] [CommMonoid α₂] @[to_additive] lemma IsMulFreimanHom.prodMap (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) := - (h₁.comp IsMulFreimanHom.fst).prodLift (h₂.comp IsMulFreimanHom.snd) + (h₁.comp .fst).prodMk (h₂.comp .snd) @[to_additive] lemma IsMulFreimanIso.prodMap (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : - IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) where - bijOn := h₁.bijOn.prodMap h₂.bijOn - map_prod_eq_map_prod s t hsA htA hs ht := by - simp only [mem_prod, forall_and, Prod.forall] at hsA htA - simp only [Prod.ext_iff, fst_prod, map_map, Function.comp_apply, Prod.map_fst, snd_prod, - Prod.map_snd] - rw [← Function.comp_def, ← map_map, ← map_map, ← Function.comp_def f₂, ← map_map, ← map_map, - h₁.map_prod_eq_map_prod (by simpa using hsA.1) (by simpa using htA.1) (by simpa) (by simpa), - h₂.map_prod_eq_map_prod (by simpa [@forall_swap α₁] using hsA.2) - (by simpa [@forall_swap α₁] using htA.2) (by simpa) (by simpa)] + IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) := + (h₁.isMulFreimanHom.prodMap h₂.isMulFreimanHom).toIsMulFreimanIso + (h₁.bijOn.invOn_invFunOn.prodMap h₂.bijOn.invOn_invFunOn) + (h₁.isMulFreimanIso_invFunOn.isMulFreimanHom.prodMap + h₂.isMulFreimanIso_invFunOn.isMulFreimanHom) end diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean index 56e1886f2c5393..a7e9a2a1696443 100644 --- a/Mathlib/Data/Set/Function.lean +++ b/Mathlib/Data/Set/Function.lean @@ -1673,6 +1673,44 @@ protected lemma InvOn.extendDomain (h : InvOn g₁ g₂ s t) : end Set namespace Set + +section Prod + +variable {α β₁ β₂ : Type*} {s : Set α} {t₁ : Set β₁} {t₂ : Set β₂} + {f₁ : α → β₁} {f₂ : α → β₂} {g₁ : β₁ → α} {g₂ : β₂ → α} + +lemma InjOn.left_prodMk (h₁ : s.InjOn f₁) : s.InjOn fun x ↦ (f₁ x, f₂ x) := + fun _ hx _ hy h => h₁ hx hy (Prod.ext_iff.1 h).1 + +lemma InjOn.right_prodMk (h₂ : s.InjOn f₂) : s.InjOn fun x ↦ (f₁ x, f₂ x) := + fun _ hx _ hy h => h₂ hx hy (Prod.ext_iff.1 h).2 + +lemma surjOn_fst (h : t₂.Nonempty) : (t₁ ×ˢ t₂).SurjOn Prod.fst t₁ := fun _ h => by simpa [h] +lemma surjOn_snd (h : t₁.Nonempty) : (t₁ ×ˢ t₂).SurjOn Prod.snd t₂ := fun _ h => by simpa [h] + +lemma surjOn_fst_iff : (t₁ ×ˢ t₂).SurjOn Prod.fst t₁ ↔ t₁ = ∅ ∨ t₂.Nonempty := + ⟨by by_contra!; aesop, Or.rec (· ▸ surjOn_empty _ _) surjOn_fst⟩ + +lemma surjOn_snd_iff : (t₁ ×ˢ t₂).SurjOn Prod.snd t₂ ↔ t₁.Nonempty ∨ t₂ = ∅ := + ⟨by by_contra!; aesop, Or.rec surjOn_snd (· ▸ surjOn_empty _ _)⟩ + +lemma mapsTo_fst : MapsTo Prod.fst (t₁ ×ˢ t₂) t₁ := fun _ hx => hx.1 +lemma mapsTo_snd : MapsTo Prod.snd (t₁ ×ˢ t₂) t₂ := fun _ hx => hx.2 + +lemma MapsTo.prodMk (h₁ : MapsTo f₁ s t₁) (h₂ : MapsTo f₂ s t₂) : + MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂) := + fun _ hx => ⟨h₁ hx, h₂ hx⟩ + +lemma LeftInvOn.left_prodMk (h₁ : LeftInvOn g₁ f₁ s) : + LeftInvOn (fun x ↦ g₁ x.1) (fun x ↦ (f₁ x, f₂ x)) s := h₁ + +lemma LeftInvOn.right_prodMk (h₂ : LeftInvOn g₂ f₂ s) : + LeftInvOn (fun x ↦ g₂ x.2) (fun x ↦ (f₁ x, f₂ x)) s := h₂ + +end Prod + +section ProdMap + variable {α₁ α₂ β₁ β₂ : Type*} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂} @@ -1707,6 +1745,8 @@ lemma InvOn.prodMap (h₁ : InvOn g₁ f₁ s₁ t₁) (h₂ : InvOn g₂ f₂ s InvOn (fun x ↦ (g₁ x.1, g₂ x.2)) (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) := ⟨h₁.1.prodMap h₂.1, h₁.2.prodMap h₂.2⟩ +end ProdMap + end Set namespace Equiv From 614d45349d3bfba978f4f0ad61d7a5f5f8151d4e Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 8 Sep 2024 19:29:27 +0000 Subject: [PATCH 06/11] fix --- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean index 30c00a8a001358..d0fb349997f4e2 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean @@ -446,7 +446,7 @@ lemma Fin.addRothNumber_eq_rothNumberNat (hkn : 2 * k ≤ n) : lemma Fin.addRothNumber_le_rothNumberNat (k n : ℕ) (hkn : k ≤ n) : addRothNumber (Iio k : Finset (Fin n.succ)) ≤ rothNumberNat k := by suffices h : Set.BijOn (Nat.cast : ℕ → Fin n.succ) (range k) (Iio k : Finset (Fin n.succ)) by - exact (AddMonoidHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h + exact (AddHomClass.isAddFreimanHom (Nat.castRingHom _) h.mapsTo).addRothNumber_mono h refine ⟨?_, (CharP.natCast_injOn_Iio _ n.succ).mono (by simp; omega), ?_⟩ · simpa using fun x ↦ natCast_strictMono hkn simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_iff_val_lt_val, From 8d467856a2aa5031b92cc302f518633e6f4b418a Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 8 Sep 2024 20:25:23 +0000 Subject: [PATCH 07/11] fix again --- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean index 9b660a299371d1..9e68e87cc8696f 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean @@ -171,7 +171,7 @@ nonrec theorem threeAPFree_sphere : ThreeAPFree (sphere n d k : Set (Fin n → { toFun := fun f => ((↑) : ℕ → ℝ) ∘ f map_zero' := funext fun _ => cast_zero map_add' := fun _ _ => funext fun _ => cast_add _ _ } - refine ThreeAPFree.of_image (AddMonoidHomClass.isAddFreimanHom f (Set.mapsTo_image _ _)) + refine ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _)) cast_injective.comp_left.injOn (Set.subset_univ _) ?_ refine (threeAPFree_sphere 0 (√↑k)).mono (Set.image_subset_iff.2 fun x => ?_) rw [Set.mem_preimage, mem_sphere_zero_iff_norm] From e05c21599718da9d967c17b2ded1fc9dc7543bd3 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 18 Apr 2026 02:46:07 +0100 Subject: [PATCH 08/11] =?UTF-8?q?fix:=20prod=5Fapply=20=E2=88=88=20syntax?= =?UTF-8?q?=20and=20MulHomClass.isMulFreimanHom=20ne=5Fzero=20proof?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Combinatorics/Additive/FreimanHom.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index aa2a3b58dbcf94..9923d459a8b57d 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -176,7 +176,7 @@ lemma IsMulFreimanIso.isMulFreimanIso_invFunOn (hf : IsMulFreimanIso n A B f) : @[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} (hs : s.card = n) (ht : t.card = n) : - ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i in s, f i = ∏ i in t, f i := by + ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i ∈ s, f i = ∏ i ∈ t, f i := by simpa using hf.map_prod_eq_map_prod hsA htA hs ht @@ -308,7 +308,8 @@ theorem card_eq_succ {α : Type*} {s : Multiset α} : match n with | 0 => by simpa | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => by - rw [← map_multiset_ne_zero_prod _ (by simp [hs]), h, map_multiset_ne_zero_prod _ (by simp [ht])] + rw [← map_multiset_ne_zero_prod _ (by rw [ne_eq, ← Multiset.card_eq_zero]; omega), + h, map_multiset_ne_zero_prod _ (by rw [ne_eq, ← Multiset.card_eq_zero]; omega)] @[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where From 81ae606dba8f1ffebb3500ca7814c489eae7e846 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 19 Apr 2026 03:30:04 +0100 Subject: [PATCH 09/11] replace deprecated Finset.toSet with coe in prod_apply --- Mathlib/Combinatorics/Additive/FreimanHom.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index 9923d459a8b57d..c5d31302c6c2f0 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -174,7 +174,7 @@ lemma IsMulFreimanIso.isMulFreimanIso_invFunOn (hf : IsMulFreimanIso n A B f) : /-- A version of the Freiman homomorphism condition expressed using `Finset`s, for practicality. -/ @[to_additive] lemma IsMulFreimanHom.prod_apply (hf : IsMulFreimanHom n A B f) {s t : Finset α} - {hsA : s.toSet ⊆ A} {htA : t.toSet ⊆ A} + {hsA : (s : Set α) ⊆ A} {htA : (t : Set α) ⊆ A} (hs : s.card = n) (ht : t.card = n) : ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i ∈ s, f i = ∏ i ∈ t, f i := by simpa using hf.map_prod_eq_map_prod hsA htA hs ht From d4f4face423e951afe2b317ad08b157739deb4fc Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 19 Apr 2026 13:56:27 +0100 Subject: [PATCH 10/11] update and shuffle --- .../Combinatorics/Additive/FreimanHom.lean | 28 ++++++------------- Mathlib/Data/List/Basic.lean | 4 +++ Mathlib/Data/Multiset/ZeroCons.lean | 5 ++++ Mathlib/Data/Set/Function.lean | 3 +- 4 files changed, 18 insertions(+), 22 deletions(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index c5d31302c6c2f0..3a8fea963e5a36 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -291,25 +291,13 @@ lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f rw [Pi.mul_def, prod_map_mul, prod_map_mul, h₁.map_prod_eq_map_prod hsA htA hs ht h, h₂.map_prod_eq_map_prod hsA htA hs ht h] -theorem List.length_eq_succ {α : Type*} {n} {l : List α} : - l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by cases l <;> aesop - -theorem card_eq_succ {α : Type*} {s : Multiset α} : - card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by - refine ⟨?_, by aesop⟩ - induction s using Quot.inductionOn with - | h s => - simp only [quot_mk_to_coe'', coe_card, List.length_eq_succ, forall_exists_index, and_imp] - rintro a s rfl rfl - exact ⟨a, s, rfl, rfl⟩ - @[to_additive] lemma MulHomClass.isMulFreimanHom [FunLike F α β] [MulHomClass F α β] (f : F) (hfAB : MapsTo f A B) : IsMulFreimanHom n A B f := match n with | 0 => by simpa | n + 1 => IsMulFreimanHom.mk hfAB fun s t hsA htA hs ht h => by - rw [← map_multiset_ne_zero_prod _ (by rw [ne_eq, ← Multiset.card_eq_zero]; omega), - h, map_multiset_ne_zero_prod _ (by rw [ne_eq, ← Multiset.card_eq_zero]; omega)] + rw [← map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero]), + h, map_multiset_ne_zero_prod _ (by grind [Multiset.card_eq_zero])] @[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where @@ -333,10 +321,10 @@ lemma isMulFreimanHom_antitone : Antitone (IsMulFreimanHom · A B f) := { mapsTo := hf.mapsTo, map_prod_eq_map_prod := fun s t hsA htA hs _ h => match n with | 0 => by aesop - | n + 1 => - have ⟨a, ha⟩ : ∃ a, a ∈ s := card_pos_iff_exists_mem.1 (by simp [hs]) - by simpa [*] using hf.map_prod_eq_map_prod (s := a ::ₘ s) (t := a ::ₘ t) - (by simpa [hsA ha]) (by simpa [hsA ha]) } + | n + 1 => by + have ⟨a, ha⟩ : ∃ a, a ∈ s := card_pos_iff_exists_mem.1 (by simp [hs]) + simpa [*] using hf.map_prod_eq_map_prod (s := a ::ₘ s) (t := a ::ₘ t) + (by simpa [hsA ha]) (by simpa [hsA ha]) } @[to_additive] lemma IsMulFreimanHom.mono (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom m A B f := @@ -379,12 +367,12 @@ section Prod @[to_additive] lemma IsMulFreimanHom.fst [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : IsMulFreimanHom n (A ×ˢ B) A Prod.fst := - MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) mapsTo_fst + MulHomClass.isMulFreimanHom (MonoidHom.fst _ _) mapsTo_fst_prod @[to_additive] lemma IsMulFreimanHom.snd [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} : IsMulFreimanHom n (A ×ˢ B) B Prod.snd := - MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) mapsTo_snd + MulHomClass.isMulFreimanHom (MonoidHom.snd _ _) mapsTo_snd_prod section diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 52d8710b6f7300..3c5b6f7e52c341 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -95,6 +95,10 @@ theorem exists_of_length_succ {n} : ∀ l : List α, l.length = n + 1 → ∃ h | [], H => absurd H.symm <| succ_ne_zero n | h :: t, _ => ⟨h, t, rfl⟩ +theorem length_eq_succ_iff {n} {l : List α} : + l.length = n + 1 ↔ ∃ h t, h :: t = l ∧ t.length = n := by + grind [cases List] + @[simp] lemma length_injective_iff : Injective (List.length : List α → ℕ) ↔ Subsingleton α := by constructor · intro h; refine ⟨fun x y => ?_⟩; (suffices [x] = [y] by simpa using this); apply h; rfl diff --git a/Mathlib/Data/Multiset/ZeroCons.lean b/Mathlib/Data/Multiset/ZeroCons.lean index 842bbada9a71ca..1828c1afa9b084 100644 --- a/Mathlib/Data/Multiset/ZeroCons.lean +++ b/Mathlib/Data/Multiset/ZeroCons.lean @@ -466,6 +466,11 @@ theorem card_eq_four {s : Multiset α} : card s = 4 ↔ ∃ x y z w, s = {x, y, Exists.imp fun _b => Exists.imp fun _c => Exists.imp fun _d => congr_arg _, fun ⟨_a, _b, _c, _d, e⟩ => e.symm ▸ rfl⟩ +theorem card_eq_succ {s : Multiset α} {n : ℕ} : + card s = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ card t = n := by + refine ⟨?_, by aesop⟩ + induction s using Multiset.induction generalizing n with aesop + /-! ### Map for partial functions -/ @[simp] diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean index a0e51c8c66a65f..c4076afed04e47 100644 --- a/Mathlib/Data/Set/Function.lean +++ b/Mathlib/Data/Set/Function.lean @@ -1261,8 +1261,7 @@ lemma surjOn_fst_iff : (t₁ ×ˢ t₂).SurjOn Prod.fst t₁ ↔ t₁ = ∅ ∨ lemma surjOn_snd_iff : (t₁ ×ˢ t₂).SurjOn Prod.snd t₂ ↔ t₁.Nonempty ∨ t₂ = ∅ := ⟨by by_contra!; aesop, Or.rec surjOn_snd (· ▸ surjOn_empty _ _)⟩ -lemma mapsTo_fst : MapsTo Prod.fst (t₁ ×ˢ t₂) t₁ := fun _ hx => hx.1 -lemma mapsTo_snd : MapsTo Prod.snd (t₁ ×ˢ t₂) t₂ := fun _ hx => hx.2 + lemma MapsTo.prodMk (h₁ : MapsTo f₁ s t₁) (h₂ : MapsTo f₂ s t₂) : MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂) := From 794d3a817539d903f9f0cc62b414b8c17ce36d37 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sun, 19 Apr 2026 14:07:46 +0100 Subject: [PATCH 11/11] tidy? --- Mathlib/Combinatorics/Additive/FreimanHom.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index 3a8fea963e5a36..60bcf194fbb822 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -144,7 +144,7 @@ lemma IsMulFreimanIso.symm {g : β → α} (hg₁ : MapsTo g B A) (hg₂ : Right IsMulFreimanIso n B A g where bijOn := hf.bijOn.symm ⟨hg₂, InjOn.rightInvOn_of_leftInvOn hf.bijOn.injOn hg₂ hf.bijOn.mapsTo hg₁⟩ map_prod_eq_map_prod := fun s t hsB htB hs ht => by - rw [←hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id, + rw [← hf.map_prod_eq_map_prod _ _ (by simp [hs]) (by simp [ht]), map_map, map_congr rfl, map_id, map_map, map_congr rfl, map_id] all_goals aesop @@ -161,9 +161,9 @@ lemma IsMulFreimanHom.toIsMulFreimanIso {g : β → α} (h : InvOn g f A B) refine ⟨fun h' => ?_, hf.map_prod_eq_map_prod hsA htA hs ht⟩ have : (map g (map f s)).prod = (map g (map f t)).prod := by have := hf.mapsTo - refine hg.map_prod_eq_map_prod ?_ ?_ ?_ ?_ h' <;> aesop (add simp MapsTo) - rwa [map_map, map_congr rfl fun x hx => ?g1, map_id, - map_map, map_congr rfl fun x hx => ?g2, map_id] at this + apply hg.map_prod_eq_map_prod <;> simp_all [MapsTo] + rwa [map_map, map_congr rfl fun x hx => ?g1, map_id, map_map, + map_congr rfl fun x hx => ?g2, map_id] at this case g1 => exact h.1 (hsA hx) case g2 => exact h.1 (htA hx)