# mathlibdocumentation

algebra.hom.freiman

# Freiman homomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we define Freiman homomorphisms. A n-Freiman homomorphism on A is a function f : α → β such that f (x₁) * ... * f (xₙ) = f (y₁) * ... * f (yₙ) for all x₁, ..., xₙ, y₁, ..., yₙ ∈ A such that x₁ * ... * xₙ = y₁ * ... * yₙ. In particular, any mul_hom is a Freiman homomorphism.

They are of interest in additive combinatorics.

## Main declaration #

• freiman_hom: Freiman homomorphism.
• add_freiman_hom: Additive Freiman homomorphism.

## Notation #

• A →*[n] β: Multiplicative n-Freiman homomorphism on A
• A →+[n] β: Additive n-Freiman homomorphism on A

## 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 add_monoid/monoid instead of the add_monoid/monoid itself.

## References #

Yufei Zhao, 18.225: Graph Theory and Additive Combinatorics

## TODO #

monoid_hom.to_freiman_hom could be relaxed to mul_hom.to_freiman_hom by proving (s.map f).prod = (t.map f).prod directly by induction instead of going through f s.prod.

Define n-Freiman isomorphisms.

Affine maps induce Freiman homs. Concretely, provide the add_freiman_hom_class (α →ₐ[𝕜] β) A β n instance.

structure add_freiman_hom {α : Type u_2} (A : set α) (β : Type u_7) (n : ) :
Type (max u_2 u_7)

An additive n-Freiman homomorphism is a map which preserves sums of n elements.

Instances for add_freiman_hom
structure freiman_hom {α : Type u_2} (A : set α) (β : Type u_7) [comm_monoid α] [comm_monoid β] (n : ) :
Type (max u_2 u_7)

A n-Freiman homomorphism on a set A is a map which preserves products of n elements.

Instances for freiman_hom
@[class]
structure add_freiman_hom_class {α : Type u_2} (F : Type u_7) (A : out_param (set α)) (β : out_param (Type u_8)) (n : ) [ α (λ (_x : α), β)] :
Prop

add_freiman_hom_class F s β n states that F is a type of n-ary sums-preserving morphisms. You should extend this class when you extend add_freiman_hom.

Instances of this typeclass
@[class]
structure freiman_hom_class {α : Type u_2} (F : Type u_7) (A : out_param (set α)) (β : out_param (Type u_8)) [comm_monoid α] [comm_monoid β] (n : ) [ α (λ (_x : α), β)] :
Prop

freiman_hom_class F A β n states that F is a type of n-ary products-preserving morphisms. You should extend this class when you extend freiman_hom.

Instances of this typeclass
theorem map_prod_eq_map_prod {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] [comm_monoid α] [comm_monoid β] {A : set α} {n : } [ β n] (f : F) {s t : multiset α} (hsA : ⦃x : α⦄, x s x A) (htA : ⦃x : α⦄, x t x A) (hs : = n) (ht : = n) (h : s.prod = t.prod) :
s).prod = t).prod
theorem map_sum_eq_map_sum {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] {A : set α} {n : } [ n] (f : F) {s t : multiset α} (hsA : ⦃x : α⦄, x s x A) (htA : ⦃x : α⦄, x t x A) (hs : = n) (ht : = n) (h : s.sum = t.sum) :
s).sum = t).sum
theorem map_add_map_eq_map_add_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] {A : set α} {a b c d : α} [ 2] (f : F) (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 map_mul_map_eq_map_mul_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] [comm_monoid α] [comm_monoid β] {A : set α} {a b c d : α} [ β 2] (f : F) (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
@[protected, instance]
def add_freiman_hom.fun_like {α : Type u_2} {β : Type u_3} {A : set α} {n : } :
fun_like (A →+[n] β) α (λ (_x : α), β)
Equations
@[protected, instance]
def freiman_hom.fun_like {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
fun_like (A →*[n] β) α (λ (_x : α), β)
Equations
@[protected, instance]
def freiman_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
freiman_hom_class (A →*[n] β) A β n
@[protected, instance]
def add_freiman_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} {A : set α} {n : } :
@[protected, instance]
def freiman_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
has_coe_to_fun (A →*[n] β) (λ (_x : A →*[n] β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[protected, instance]
def add_freiman_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} {A : set α} {n : } :
has_coe_to_fun (A →+[n] β) (λ (_x : A →+[n] β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem add_freiman_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f : A →+[n] β) :
@[simp]
theorem freiman_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : A →*[n] β) :
@[ext]
theorem add_freiman_hom.ext {α : Type u_2} {β : Type u_3} {A : set α} {n : } ⦃f g : A →+[n] β⦄ (h : (x : α), f x = g x) :
f = g
@[ext]
theorem freiman_hom.ext {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } ⦃f g : A →*[n] β⦄ (h : (x : α), f x = g x) :
f = g
@[simp]
theorem add_freiman_hom.coe_mk {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f : α β) (h : (s t : multiset α), ( ⦃x : α⦄, x s x A) ( ⦃x : α⦄, x t x A) s.sum = t.sum s).sum = t).sum) :
@[simp]
theorem freiman_hom.coe_mk {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : α β) (h : (s t : multiset α), ( ⦃x : α⦄, x s x A) ( ⦃x : α⦄, x t x A) s.prod = t.prod s).prod = t).prod) :
@[simp]
theorem add_freiman_hom.mk_coe {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f : A →+[n] β) (h : {s t : multiset α}, ( ⦃x : α⦄, x s x A) ( ⦃x : α⦄, x t x A) s.sum = t.sum s).sum = t).sum) :
@[simp]
theorem freiman_hom.mk_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : A →*[n] β) (h : {s t : multiset α}, ( ⦃x : α⦄, x s x A) ( ⦃x : α⦄, x t x A) s.prod = t.prod s).prod = t).prod) :
@[simp]
theorem freiman_hom.id_apply {α : Type u_2} [comm_monoid α] (A : set α) (n : ) (x : α) :
n) x = x
@[protected]
def freiman_hom.id {α : Type u_2} [comm_monoid α] (A : set α) (n : ) :
A →*[n] α

The identity map from a commutative monoid to itself.

Equations
@[protected]
def add_freiman_hom.id {α : Type u_2} (A : set α) (n : ) :
A →+[n] α

The identity map from an additive commutative monoid to itself.

Equations
@[simp]
theorem add_freiman_hom.id_apply {α : Type u_2} (A : set α) (n : ) (x : α) :
n) x = x
@[protected]
def freiman_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) (hAB : A B) :
A →*[n] γ

Composition of Freiman homomorphisms as a Freiman homomorphism.

Equations
@[protected]
def add_freiman_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) (hAB : A B) :
A →+[n] γ

Equations
@[simp]
theorem freiman_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) {hfg : A B} :
(f.comp g hfg) = f g
@[simp]
theorem add_freiman_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : A B} :
(f.comp g hfg) = f g
theorem freiman_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →*[n] γ) (g : A →*[n] β) {hfg : A B} (x : α) :
(f.comp g hfg) x = f (g x)
theorem add_freiman_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : A B} (x : α) :
(f.comp g hfg) x = f (g x)
theorem freiman_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [comm_monoid α] [comm_monoid β] [comm_monoid γ] [comm_monoid δ] {A : set α} {B : set β} {C : set γ} {n : } (f : A →*[n] β) (g : B →*[n] γ) (h : C →*[n] δ) {hf : A B} {hhg : B C} {hgf : A B} {hh : set.maps_to (g.comp f hgf) A C} :
(h.comp g hhg).comp f hf = h.comp (g.comp f hgf) hh
theorem add_freiman_hom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} {A : set α} {B : set β} {C : set γ} {n : } (f : A →+[n] β) (g : B →+[n] γ) (h : C →+[n] δ) {hf : A B} {hhg : B C} {hgf : A B} {hh : set.maps_to (g.comp f hgf) A C} :
(h.comp g hhg).comp f hf = h.comp (g.comp f hgf) hh
theorem add_freiman_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } {g₁ g₂ : B →+[n] γ} {f : A →+[n] β} (hf : function.surjective f) {hg₁ hg₂ : A B} :
g₁.comp f hg₁ = g₂.comp f hg₂ g₁ = g₂
theorem freiman_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } {g₁ g₂ : B →*[n] γ} {f : A →*[n] β} (hf : function.surjective f) {hg₁ hg₂ : A B} :
g₁.comp f hg₁ = g₂.comp f hg₂ g₁ = g₂
theorem freiman_hom.cancel_right_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } {g₁ g₂ : B →*[n] γ} {f : A →*[n] β} (hf : A B) {hf' : A B} :
set.eq_on (g₁.comp f hf') (g₂.comp f hf') A g₂ B
theorem add_freiman_hom.cancel_right_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } {g₁ g₂ : B →+[n] γ} {f : A →+[n] β} (hf : A B) {hf' : A B} :
set.eq_on (g₁.comp f hf') (g₂.comp f hf') A g₂ B
theorem add_freiman_hom.cancel_left_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } {g : B →+[n] γ} {f₁ f₂ : A →+[n] β} (hg : B) {hf₁ : A B} {hf₂ : A B} :
set.eq_on (g.comp f₁ hf₁) (g.comp f₂ hf₂) A f₂ A
theorem freiman_hom.cancel_left_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } {g : B →*[n] γ} {f₁ f₂ : A →*[n] β} (hg : B) {hf₁ : A B} {hf₂ : A B} :
set.eq_on (g.comp f₁ hf₁) (g.comp f₂ hf₂) A f₂ A
@[simp]
theorem add_freiman_hom.comp_id {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f : A →+[n] β) {hf : A A} :
f.comp n) hf = f
@[simp]
theorem freiman_hom.comp_id {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : A →*[n] β) {hf : A A} :
f.comp n) hf = f
@[simp]
theorem add_freiman_hom.id_comp {α : Type u_2} {β : Type u_3} {A : set α} {B : set β} {n : } (f : A →+[n] β) {hf : A B} :
n).comp f hf = f
@[simp]
theorem freiman_hom.id_comp {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {B : set β} {n : } (f : A →*[n] β) {hf : A B} :
n).comp f hf = f
def freiman_hom.const {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (A : set α) (n : ) (b : β) :
A →*[n] β

freiman_hom.const A n b is the Freiman homomorphism sending everything to b.

Equations
def add_freiman_hom.const {α : Type u_2} {β : Type u_3} (A : set α) (n : ) (b : β) :
A →+[n] β

add_freiman_hom.const n b is the Freiman homomorphism sending everything to b.

Equations
@[simp]
theorem freiman_hom.const_apply {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} (n : ) (b : β) (x : α) :
b) x = b
@[simp]
theorem add_freiman_hom.const_apply {α : Type u_2} {β : Type u_3} {A : set α} (n : ) (b : β) (x : α) :
b) x = b
@[simp]
theorem freiman_hom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} (n : ) (c : γ) (f : A →*[n] β) {hf : A B} :
c).comp f hf = c
@[simp]
theorem add_freiman_hom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} (n : ) (c : γ) (f : A →+[n] β) {hf : A B} :
c).comp f hf =
@[protected, instance]
def freiman_hom.has_one {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
has_one (A →*[n] β)

1 is the Freiman homomorphism sending everything to 1.

Equations
@[protected, instance]
def add_freiman_hom.has_zero {α : Type u_2} {β : Type u_3} {A : set α} {n : } :

0 is the Freiman homomorphism sending everything to 0.

Equations
@[simp]
theorem freiman_hom.one_apply {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (x : α) :
1 x = 1
@[simp]
theorem add_freiman_hom.zero_apply {α : Type u_2} {β : Type u_3} {A : set α} {n : } (x : α) :
0 x = 0
@[simp]
theorem add_freiman_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } (f : A →+[n] β) {hf : A B} :
0.comp f hf = 0
@[simp]
theorem freiman_hom.one_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } (f : A →*[n] β) {hf : A B} :
1.comp f hf = 1
@[protected, instance]
def add_freiman_hom.inhabited {α : Type u_2} {β : Type u_3} {A : set α} {n : } :
Equations
@[protected, instance]
def freiman_hom.inhabited {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
Equations
@[protected, instance]
def freiman_hom.has_mul {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
has_mul (A →*[n] β)

f * g is the Freiman homomorphism sends x to f x * g x.

Equations
@[protected, instance]
def add_freiman_hom.has_add {α : Type u_2} {β : Type u_3} {A : set α} {n : } :

f + g is the Freiman homomorphism sending x to f x + g x.

Equations
@[simp]
theorem freiman_hom.mul_apply {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f g : A →*[n] β) (x : α) :
(f * g) x = f x * g x
@[simp]
theorem add_freiman_hom.add_apply {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f g : A →+[n] β) (x : α) :
(f + g) x = f x + g x
theorem freiman_hom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [comm_monoid α] [comm_monoid β] [comm_monoid γ] {A : set α} {B : set β} {n : } (g₁ g₂ : B →*[n] γ) (f : A →*[n] β) {hg hg₁ hg₂ : A B} :
(g₁ * g₂).comp f hg = g₁.comp f hg₁ * g₂.comp f hg₂
theorem add_freiman_hom.add_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} {A : set α} {B : set β} {n : } (g₁ g₂ : B →+[n] γ) (f : A →+[n] β) {hg hg₁ hg₂ : A B} :
(g₁ + g₂).comp f hg = g₁.comp f hg₁ + g₂.comp f hg₂
@[protected, instance]
def freiman_hom.has_inv {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : } :

If f is a Freiman homomorphism to a commutative group, then f⁻¹ is the Freiman homomorphism sending x to (f x)⁻¹.

Equations
@[protected, instance]
def add_freiman_hom.has_neg {α : Type u_2} {G : Type u_6} {A : set α} {n : } :

If f is a Freiman homomorphism to an additive commutative group, then -f is the Freiman homomorphism sending x to -f x.

Equations
@[simp]
theorem add_freiman_hom.neg_apply {α : Type u_2} {G : Type u_6} {A : set α} {n : } (f : A →+[n] G) (x : α) :
(-f) x = -f x
@[simp]
theorem freiman_hom.inv_apply {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : } (f : A →*[n] G) (x : α) :
@[simp]
theorem add_freiman_hom.neg_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} {A : set α} {B : set β} {n : } (f : B →+[n] G) (g : A →+[n] β) {hf hf' : A B} :
(-f).comp g hf = -f.comp g hf'
@[simp]
theorem freiman_hom.inv_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [comm_monoid α] [comm_monoid β] [comm_group G] {A : set α} {B : set β} {n : } (f : B →*[n] G) (g : A →*[n] β) {hf hf' : A B} :
f⁻¹.comp g hf = (f.comp g hf')⁻¹
@[protected, instance]
def freiman_hom.has_div {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : } :

If f and g are Freiman homomorphisms to a commutative group, then f / g is the Freiman homomorphism sending x to f x / g x.

Equations
@[protected, instance]
def add_freiman_hom.has_sub {α : Type u_2} {G : Type u_6} {A : set α} {n : } :

If f and g are additive Freiman homomorphisms to an additive commutative group, then f - g is the additive Freiman homomorphism sending x to f x - g x

Equations
@[simp]
theorem freiman_hom.div_apply {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : } (f g : A →*[n] G) (x : α) :
(f / g) x = f x / g x
@[simp]
theorem add_freiman_hom.sub_apply {α : Type u_2} {G : Type u_6} {A : set α} {n : } (f g : A →+[n] G) (x : α) :
(f - g) x = f x - g x
@[simp]
theorem freiman_hom.div_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [comm_monoid α] [comm_monoid β] [comm_group G] {A : set α} {B : set β} {n : } (f₁ f₂ : B →*[n] G) (g : A →*[n] β) {hf hf₁ hf₂ : A B} :
(f₁ / f₂).comp g hf = f₁.comp g hf₁ / f₂.comp g hf₂
@[simp]
theorem add_freiman_hom.sub_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} {A : set α} {B : set β} {n : } (f₁ f₂ : B →+[n] G) (g : A →+[n] β) {hf hf₁ hf₂ : A B} :
(f₁ - f₂).comp g hf = f₁.comp g hf₁ - f₂.comp g hf₂

### Instances #

@[protected, instance]
def add_freiman_hom.add_comm_monoid {α : Type u_2} {β : Type u_3} {A : set α} {n : } :

α →+[n] β is an add_comm_monoid.

Equations
@[protected, instance]
def freiman_hom.comm_monoid {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :

A →*[n] β is a comm_monoid.

Equations
@[protected, instance]
def add_freiman_hom.add_comm_group {α : Type u_2} {A : set α} {n : } {β : Type u_1}  :

If β is an additive commutative group, then A →*[n] β is an additive commutative group too.

Equations
@[protected, instance]
def freiman_hom.comm_group {α : Type u_2} [comm_monoid α] {A : set α} {n : } {β : Type u_1} [comm_group β] :

If β is a commutative group, then A →*[n] β is a commutative group too.

Equations

### Hom hierarchy #

@[protected, instance]
def monoid_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {n : } :

A monoid homomorphism is naturally a freiman_hom on its entire domain.

We can't leave the domain A : set α of the freiman_hom a free variable, since it wouldn't be inferrable.

@[protected, instance]
def add_monoid_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} {n : } :
β n

An additive monoid homomorphism is naturally an add_freiman_hom on its entire domain.

We can't leave the domain A : set α of the freiman_hom a free variable, since it wouldn't be inferrable.

def monoid_hom.to_freiman_hom {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] (A : set α) (n : ) (f : α →* β) :
A →*[n] β

A monoid_hom is naturally a freiman_hom.

Equations
def add_monoid_hom.to_add_freiman_hom {α : Type u_2} {β : Type u_3} (A : set α) (n : ) (f : α →+ β) :
A →+[n] β

An add_monoid_hom is naturally an add_freiman_hom

Equations
@[simp]
theorem add_monoid_hom.to_freiman_hom_coe {α : Type u_2} {β : Type u_3} {A : set α} {n : } (f : α →+ β) :
= f
@[simp]
theorem monoid_hom.to_freiman_hom_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : α →* β) :
f) = f
theorem add_monoid_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} {A : set α} {n : } :
theorem monoid_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } :
theorem map_sum_eq_map_sum_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] {A : set α} {m n : } [ n] (f : F) {s t : multiset α} (hsA : (x : α), x s x A) (htA : (x : α), x t x A) (hs : = m) (ht : = m) (hst : s.sum = t.sum) (h : m n) :
s).sum = t).sum
theorem map_prod_eq_map_prod_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] [comm_monoid α] {A : set α} {m n : } [ β n] (f : F) {s t : multiset α} (hsA : (x : α), x s x A) (htA : (x : α), x t x A) (hs : = m) (ht : = m) (hst : s.prod = t.prod) (h : m n) :
s).prod = t).prod
def add_freiman_hom.to_add_freiman_hom {α : Type u_2} {β : Type u_3} {A : set α} {m n : } (h : m n) (f : A →+[n] β) :
A →+[m] β

α →+[n] β is naturally included in α →+[m] β for any m ≤ n

Equations
def freiman_hom.to_freiman_hom {α : Type u_2} {β : Type u_3} [comm_monoid α] {A : set α} {m n : } (h : m n) (f : A →*[n] β) :
A →*[m] β

α →*[n] β is naturally included in A →*[m] β for any m ≤ n.

Equations
theorem add_freiman_hom.add_freiman_hom_class_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] {A : set α} {m n : } [ n] (h : m n) :
m

An additive n-Freiman homomorphism is also an additive m-Freiman homomorphism for any m ≤ n.

theorem freiman_hom.freiman_hom_class_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [ α (λ (_x : α), β)] [comm_monoid α] {A : set α} {m n : } [ β n] (h : m n) :
β m

A n-Freiman homomorphism is also a m-Freiman homomorphism for any m ≤ n.

@[simp]
theorem freiman_hom.to_freiman_hom_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] {A : set α} {m n : } (h : m n) (f : A →*[n] β) :
@[simp]
theorem add_freiman_hom.to_add_freiman_hom_coe {α : Type u_2} {β : Type u_3} {A : set α} {m n : } (h : m n) (f : A →+[n] β) :
theorem freiman_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} [comm_monoid α] {A : set α} {m n : } (h : m n) :
theorem add_freiman_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} {A : set α} {m n : } (h : m n) :