diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean index d17244da0a84c2..35fe0a35b2589e 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean @@ -176,7 +176,7 @@ nonrec theorem threeAPFree_sphere : ThreeAPFree (sphere n d k : Set (Fin n → { toFun := fun f => toLp 2 (((↑) : ℕ → ℝ) ∘ f) map_zero' := PiLp.ext fun _ => cast_zero map_add' := fun _ _ => PiLp.ext fun _ => cast_add _ _ } - refine ThreeAPFree.of_image (AddMonoidHomClass.isAddFreimanHom f (Set.mapsTo_image _ _)) + refine ThreeAPFree.of_image (AddHomClass.isAddFreimanHom f (Set.mapsTo_image _ _)) ((toLp_injective 2).comp_injOn 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] diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean index 534177a2aa83fa..0de18c194e9c72 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Defs.lean @@ -452,7 +452,7 @@ open Fin.CommRing in -- TODO: should this be refactored to avoid needing the coe 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; lia), ?_⟩ · simpa using fun x ↦ natCast_strictMono hkn simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_def, diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean index 676b5d5ef1d6aa..60bcf194fbb822 100644 --- a/Mathlib/Combinatorics/Additive/FreimanHom.lean +++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean @@ -134,6 +134,52 @@ lemma IsMulFreimanIso.congr (hf₁ : IsMulFreimanIso n A B f₁) (h : EqOn f₁ 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 +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 + 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) + +@[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 : 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 + + @[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) : @@ -245,10 +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] -@[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] +@[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 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 @@ -259,7 +308,7 @@ lemma isMulFreimanIso_empty : IsMulFreimanIso n (∅ : Set α) (∅ : Set β) f @[to_additive] lemma IsMulFreimanHom.subtypeVal {S : Type*} [SetLike S α] [SubmonoidClass S α] {s : S} : IsMulFreimanHom n (univ : Set s) univ Subtype.val := - MonoidHomClass.isMulFreimanHom (SubmonoidClass.subtype s) (mapsTo_univ ..) + MulHomClass.isMulFreimanHom (SubmonoidClass.subtype s) (mapsTo_univ ..) end CommMonoid @@ -267,31 +316,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 [card_add, card_replicate, hs, Nat.add_sub_cancel' hmn] - · rw [card_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 => 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 := + isMulFreimanHom_antitone hmn hf end CancelCommMonoid @@ -300,30 +337,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 [card_add, card_replicate, hs, Nat.add_sub_cancel' hmn] - · rw [card_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 @@ -347,34 +363,51 @@ 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 _ _) 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_prod + +section + +variable {α β₁ β₂ : Type*} [CommMonoid α] [CommMonoid β₁] [CommMonoid β₂] + {A : Set α} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} {n : ℕ} + +@[to_additive] +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 [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 + +section + variable {α₁ α₂ β₁ β₂ : Type*} [CommMonoid α₁] [CommMonoid α₂] [CommMonoid β₁] [CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} -@[to_additive prodMap] +@[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₂) 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_comm α₁] using hsA.2) - (by simpa [@forall_comm α₁] using htA.2) (by simpa) (by simpa) h.2⟩ - -@[to_additive prodMap] + IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂) := + (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_comm α₁] using hsA.2) - (by simpa [@forall_comm α₁] 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 end Prod 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 8dc96468812a72..c4076afed04e47 100644 --- a/Mathlib/Data/Set/Function.lean +++ b/Mathlib/Data/Set/Function.lean @@ -1240,6 +1240,43 @@ 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.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₂ : β₂ → α₂} @@ -1274,6 +1311,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