Freiman homomorphisms

In this file, we define Freiman homomorphisms and isomorphism.

An n-Freiman homomorphism from A to B is a function f : α → β such that f '' A ⊆ B and 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 declarations

• IsMulFreimanHom: Predicate for a function to be a multiplicative Freiman homomorphism.
• IsAddFreimanHom: Predicate for a function to be an additive Freiman homomorphism.
• IsMulFreimanIso: Predicate for a function to be a multiplicative Freiman isomorphism.
• IsAddFreimanIso: Predicate for a function to be an additive Freiman isomorphism.

Main results

• isMulFreimanHom_two: Characterisation of 2-Freiman homomorphisms.
• IsMulFreimanHom.mono: If m ≤ n and f is an n-Freiman homomorphism, then it is also an m-Freiman homomorphism.

Implementation notes

In the context of combinatorics, we are interested in Freiman homomorphisms over sets which are not necessarily closed under addition/multiplication. This means we must parametrize them with a set in an AddMonoid/Monoid instead of the AddMonoid/Monoid itself.

References

Yufei Zhao, 18.225: Graph Theory and Additive Combinatorics

TODO

• MonoidHomClass.isMulFreimanHom could be relaxed to MulHom.toFreimanHom by proving (s.map f).prod = (t.map f).prod directly by induction instead of going through f s.prod.
• Affine maps are Freiman homs.

structure IsAddFreimanHom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) (A : Set α) (B : Set β) (f : α → β) : Prop

An additive n-Freiman homomorphism from a set A to a set B is a map which preserves sums of n elements.

• mapsTo : Set.MapsTo f A B
• map_sum_eq_map_sum : ∀ ⦃s t : Multiset α⦄, (∀ ⦃x : α⦄, x ∈ s → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → Multiset.card s = n → Multiset.card t = n → s.sum = t.sum → (Multiset.map f s).sum = (Multiset.map f t).sum

  An additive n-Freiman homomorphism preserves sums of n elements.

structure IsMulFreimanHom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (n : ℕ) (A : Set α) (B : Set β) (f : α → β) : Prop

An n-Freiman homomorphism from a set A to a set B is a map which preserves products of n elements.

• mapsTo : Set.MapsTo f A B
• map_prod_eq_map_prod : ∀ ⦃s t : Multiset α⦄, (∀ ⦃x : α⦄, x ∈ s → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → Multiset.card s = n → Multiset.card t = n → s.prod = t.prod → (Multiset.map f s).prod = (Multiset.map f t).prod

  An n-Freiman homomorphism preserves products of n elements.

structure IsAddFreimanIso {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) (A : Set α) (B : Set β) (f : α → β) : Prop

An additive n-Freiman homomorphism from a set A to a set B is a bijective map which preserves sums of n elements.

• bijOn : Set.BijOn f A B
• map_sum_eq_map_sum : ∀ ⦃s t : Multiset α⦄, (∀ ⦃x : α⦄, x ∈ s → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → Multiset.card s = n → Multiset.card t = n → ((Multiset.map f s).sum = (Multiset.map f t).sum ↔ s.sum = t.sum)

  An additive n-Freiman homomorphism preserves sums of n elements.

structure IsMulFreimanIso {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (n : ℕ) (A : Set α) (B : Set β) (f : α → β) : Prop

An n-Freiman homomorphism from a set A to a set B is a map which preserves products of n elements.

• bijOn : Set.BijOn f A B
• map_prod_eq_map_prod : ∀ ⦃s t : Multiset α⦄, (∀ ⦃x : α⦄, x ∈ s → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → Multiset.card s = n → Multiset.card t = n → ((Multiset.map f s).prod = (Multiset.map f t).prod ↔ s.prod = t.prod)

  An n-Freiman homomorphism preserves products of n elements.

theorem IsMulFreimanIso.isMulFreimanHom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} {n : ℕ} (hf : IsMulFreimanIso n A B f) : IsMulFreimanHom n A B f

theorem IsAddFreimanIso.isAddFreimanHom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {n : ℕ} (hf : IsAddFreimanIso n A B f) : IsAddFreimanHom n A B f

theorem IsMulFreimanHom.congr {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f₁ f₂ : α → β} {n : ℕ} (hf₁ : IsMulFreimanHom n A B f₁) (h : Set.EqOn f₁ f₂ A) : IsMulFreimanHom n A B f₂

theorem IsMulFreimanIso.congr {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f₁ f₂ : α → β} {n : ℕ} (hf₁ : IsMulFreimanIso n A B f₁) (h : Set.EqOn f₁ f₂ A) : IsMulFreimanIso n A B f₂

theorem IsMulFreimanHom.mul_eq_mul {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} (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) : f a * f b = f c * f d

theorem IsAddFreimanHom.add_eq_add {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} (hf : IsAddFreimanHom 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) : f a + f b = f c + f d

theorem IsMulFreimanIso.mul_eq_mul {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} (hf : IsMulFreimanIso 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) : f a * f b = f c * f d ↔ a * b = c * d

theorem IsAddFreimanIso.add_eq_add {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} (hf : IsAddFreimanIso 2 A B f) {a b c d : α} (ha : a ∈ A) (hb : b ∈ A) (hc : c ∈ A) (hd : d ∈ A) : f a + f b = f c + f d ↔ a + b = c + d

theorem isMulFreimanHom_two {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d

Characterisation of 2-Freiman homomorphisms.

theorem isAddFreimanHom_two {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a + b = c + d → f a + f b = f c + f d

Characterisation of 2-Freiman homomorphisms.

theorem isMulFreimanIso_two {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanIso 2 A B f ↔ Set.BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a * f b = f c * f d ↔ a * b = c * d

Characterisation of 2-Freiman homs.

theorem isAddFreimanIso_two {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanIso 2 A B f ↔ Set.BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a + f b = f c + f d ↔ a + b = c + d

Characterisation of 2-Freiman isomorphisms.

theorem isMulFreimanHom_id {α : Type u_2} [CommMonoid α] {A₁ A₂ : Set α} {n : ℕ} (hA : A₁ ⊆ A₂) : IsMulFreimanHom n A₁ A₂ id

theorem isAddFreimanHom_id {α : Type u_2} [AddCommMonoid α] {A₁ A₂ : Set α} {n : ℕ} (hA : A₁ ⊆ A₂) : IsAddFreimanHom n A₁ A₂ id

theorem isMulFreimanIso_id {α : Type u_2} [CommMonoid α] {A : Set α} {n : ℕ} : IsMulFreimanIso n A A id

theorem isAddFreimanIso_id {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} : IsAddFreimanIso n A A id

theorem IsMulFreimanHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ} (hg : IsMulFreimanHom n B C g) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A C (g ∘ f)

theorem IsAddFreimanHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ} (hg : IsAddFreimanHom n B C g) (hf : IsAddFreimanHom n A B f) : IsAddFreimanHom n A C (g ∘ f)

theorem IsMulFreimanIso.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ} (hg : IsMulFreimanIso n B C g) (hf : IsMulFreimanIso n A B f) : IsMulFreimanIso n A C (g ∘ f)

theorem IsAddFreimanIso.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {C : Set γ} {f : α → β} {g : β → γ} {n : ℕ} (hg : IsAddFreimanIso n B C g) (hf : IsAddFreimanIso n A B f) : IsAddFreimanIso n A C (g ∘ f)

theorem IsMulFreimanHom.subset {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hA : A₁ ⊆ A₂) (hf : IsMulFreimanHom n A₂ B₂ f) (hf' : Set.MapsTo f A₁ B₁) : IsMulFreimanHom n A₁ B₁ f

theorem IsAddFreimanHom.subset {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hA : A₁ ⊆ A₂) (hf : IsAddFreimanHom n A₂ B₂ f) (hf' : Set.MapsTo f A₁ B₁) : IsAddFreimanHom n A₁ B₁ f

theorem IsMulFreimanHom.superset {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hB : B₁ ⊆ B₂) (hf : IsMulFreimanHom n A B₁ f) : IsMulFreimanHom n A B₂ f

theorem IsAddFreimanHom.superset {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hB : B₁ ⊆ B₂) (hf : IsAddFreimanHom n A B₁ f) : IsAddFreimanHom n A B₂ f

theorem IsMulFreimanIso.subset {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hA : A₁ ⊆ A₂) (hf : IsMulFreimanIso n A₂ B₂ f) (hf' : Set.BijOn f A₁ B₁) : IsMulFreimanIso n A₁ B₁ f

theorem IsAddFreimanIso.subset {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A₁ A₂ : Set α} {B₁ B₂ : Set β} {f : α → β} {n : ℕ} (hA : A₁ ⊆ A₂) (hf : IsAddFreimanIso n A₂ B₂ f) (hf' : Set.BijOn f A₁ B₁) : IsAddFreimanIso n A₁ B₁ f

theorem isMulFreimanHom_const {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} {b : β} (hb : b ∈ B) : IsMulFreimanHom n A B fun (x : α) => b

theorem isAddFreimanHom_const {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ} {b : β} (hb : b ∈ B) : IsAddFreimanHom n A B fun (x : α) => b

@[simp]

theorem isMulFreimanHom_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanHom 0 A B f ↔ Set.MapsTo f A B

@[simp]

theorem isAddFreimanHom_zero_iff {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanHom 0 A B f ↔ Set.MapsTo f A B

@[simp]

theorem isMulFreimanIso_zero_iff {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanIso 0 A B f ↔ Set.BijOn f A B

@[simp]

theorem isAddFreimanIso_zero_iff {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanIso 0 A B f ↔ Set.BijOn f A B

@[simp]

theorem isMulFreimanHom_one_iff {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanHom 1 A B f ↔ Set.MapsTo f A B

@[simp]

theorem isAddFreimanHom_one_iff {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanHom 1 A B f ↔ Set.MapsTo f A B

@[simp]

theorem isMulFreimanIso_one_iff {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsMulFreimanIso 1 A B f ↔ Set.BijOn f A B

@[simp]

theorem isAddFreimanIso_one_iff {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β} : IsAddFreimanIso 1 A B f ↔ Set.BijOn f A B

@[simp]

theorem isMulFreimanHom_empty {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {B : Set β} {f : α → β} {n : ℕ} : IsMulFreimanHom n ∅ B f

@[simp]

theorem isAddFreimanHom_empty {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {B : Set β} {f : α → β} {n : ℕ} : IsAddFreimanHom n ∅ B f

@[simp]

theorem isMulFreimanIso_empty {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {f : α → β} {n : ℕ} : IsMulFreimanIso n ∅ ∅ f

@[simp]

theorem isAddFreimanIso_empty {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {f : α → β} {n : ℕ} : IsAddFreimanIso n ∅ ∅ f

theorem IsMulFreimanHom.mul {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} {n : ℕ} (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ * B₂) (f₁ * f₂)

theorem IsAddFreimanHom.add {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B₁ B₂ : Set β} {f₁ f₂ : α → β} {n : ℕ} (h₁ : IsAddFreimanHom n A B₁ f₁) (h₂ : IsAddFreimanHom n A B₂ f₂) : IsAddFreimanHom n A (B₁ + B₂) (f₁ + f₂)

theorem MonoidHomClass.isMulFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} [FunLike F α β] [MonoidHomClass F α β] (f : F) (hfAB : Set.MapsTo (⇑f) A B) : IsMulFreimanHom n A B ⇑f

theorem AddMonoidHomClass.isAddFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ} [FunLike F α β] [AddMonoidHomClass F α β] (f : F) (hfAB : Set.MapsTo (⇑f) A B) : IsAddFreimanHom n A B ⇑f

theorem MulEquivClass.isMulFreimanIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} [EquivLike F α β] [MulEquivClass F α β] (f : F) (hfAB : Set.BijOn (⇑f) A B) : IsMulFreimanIso n A B ⇑f

theorem AddEquivClass.isAddFreimanIso {F : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ} [EquivLike F α β] [AddEquivClass F α β] (f : F) (hfAB : Set.BijOn (⇑f) A B) : IsAddFreimanIso n A B ⇑f

theorem IsMulFreimanHom.subtypeVal {α : Type u_2} [CommMonoid α] {n : ℕ} {S : Type u_5} [SetLike S α] [SubmonoidClass S α] {s : S} : IsMulFreimanHom n Set.univ Set.univ Subtype.val

theorem IsAddFreimanHom.subtypeVal {α : Type u_2} [AddCommMonoid α] {n : ℕ} {S : Type u_5} [SetLike S α] [AddSubmonoidClass S α] {s : S} : IsAddFreimanHom n Set.univ Set.univ Subtype.val

theorem IsMulFreimanHom.mono {α : Type u_2} {β : Type u_3} [CommMonoid α] [CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {m n : ℕ} (hmn : m ≤ n) (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom m A B f

theorem IsAddFreimanHom.mono {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {m n : ℕ} (hmn : m ≤ n) (hf : IsAddFreimanHom n A B f) : IsAddFreimanHom m A B f

theorem IsMulFreimanIso.mono {α : Type u_2} {β : Type u_3} [CancelCommMonoid α] [CancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {m n : ℕ} {hmn : m ≤ n} (hf : IsMulFreimanIso n A B f) : IsMulFreimanIso m A B f

theorem IsAddFreimanIso.mono {α : Type u_2} {β : Type u_3} [AddCancelCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {m n : ℕ} {hmn : m ≤ n} (hf : IsAddFreimanIso n A B f) : IsAddFreimanIso m A B f

theorem IsMulFreimanHom.inv {α : Type u_2} {β : Type u_3} [CommMonoid α] [DivisionCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {n : ℕ} (hf : IsMulFreimanHom n A B f) : IsMulFreimanHom n A B⁻¹ f⁻¹

theorem IsAddFreimanHom.neg {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [SubtractionCommMonoid β] {A : Set α} {B : Set β} {f : α → β} {n : ℕ} (hf : IsAddFreimanHom n A B f) : IsAddFreimanHom n A (-B) (-f)

theorem IsMulFreimanHom.div {α : Type u_2} [CommMonoid α] {A : Set α} {n : ℕ} {β : Type u_5} [DivisionCommMonoid β] {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : IsMulFreimanHom n A B₁ f₁) (h₂ : IsMulFreimanHom n A B₂ f₂) : IsMulFreimanHom n A (B₁ / B₂) (f₁ / f₂)

theorem IsAddFreimanHom.sub {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_5} [SubtractionCommMonoid β] {B₁ B₂ : Set β} {f₁ f₂ : α → β} (h₁ : IsAddFreimanHom n A B₁ f₁) (h₂ : IsAddFreimanHom n A B₂ f₂) : IsAddFreimanHom n A (B₁ - B₂) (f₁ - f₂)

theorem IsMulFreimanHom.prod {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [CommMonoid α₁] [CommMonoid α₂] [CommMonoid β₁] [CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} (h₁ : IsMulFreimanHom n A₁ B₁ f₁) (h₂ : IsMulFreimanHom n A₂ B₂ f₂) : IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

theorem IsAddFreimanHom.sum {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [AddCommMonoid α₁] [AddCommMonoid α₂] [AddCommMonoid β₁] [AddCommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} (h₁ : IsAddFreimanHom n A₁ B₁ f₁) (h₂ : IsAddFreimanHom n A₂ B₂ f₂) : IsAddFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

theorem IsMulFreimanIso.prod {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [CommMonoid α₁] [CommMonoid α₂] [CommMonoid β₁] [CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} (h₁ : IsMulFreimanIso n A₁ B₁ f₁) (h₂ : IsMulFreimanIso n A₂ B₂ f₂) : IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

theorem IsAddFreimanIso.sum {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [AddCommMonoid α₁] [AddCommMonoid α₂] [AddCommMonoid β₁] [AddCommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ} (h₁ : IsAddFreimanIso n A₁ B₁ f₁) (h₂ : IsAddFreimanIso n A₂ B₂ f₂) : IsAddFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)

theorem Fin.isAddFreimanIso_Iic {k m n : ℕ} (hm : m ≠ 0) (hkmn : m * k ≤ n) : IsAddFreimanIso m (Set.Iic ↑k) (Set.Iic k) Fin.val

No wrap-around principle.

The first k + 1 elements of Fin (n + 1) are m-Freiman isomorphic to the first k + 1 elements of ℕ assuming there is no wrap-around.

theorem Fin.isAddFreimanIso_Iio {k m n : ℕ} (hm : m ≠ 0) (hkmn : m * k ≤ n) : IsAddFreimanIso m (Set.Iio ↑k) (Set.Iio k) Fin.val

No wrap-around principle.

The first k elements of Fin (n + 1) are m-Freiman isomorphic to the first k elements of ℕ assuming there is no wrap-around.