mathlib documentation

algebra.hom.freiman

Freiman homomorphisms #

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 #

Notation #

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) [add_comm_monoid α] [add_comm_monoid β] (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)) [add_comm_monoid α] [add_comm_monoid β] (n : ) [fun_like F α (λ (_x : α), β)] :
Type

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
Instances of other typeclasses for add_freiman_hom_class
  • add_freiman_hom_class.has_sizeof_inst
@[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 : ) [fun_like F α (λ (_x : α), β)] :
Type

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
Instances of other typeclasses for freiman_hom_class
  • freiman_hom_class.has_sizeof_inst
theorem map_prod_eq_map_prod {F : Type u_1} {α : Type u_2} {β : Type u_3} [fun_like F α (λ (_x : α), β)] [comm_monoid α] [comm_monoid β] {A : set α} {n : } [freiman_hom_class F A β n] (f : F) {s t : multiset α} (hsA : ∀ ⦃x : α⦄, x sx A) (htA : ∀ ⦃x : α⦄, x tx A) (hs : multiset.card s = n) (ht : multiset.card t = n) (h : s.prod = t.prod) :
theorem map_sum_eq_map_sum {F : Type u_1} {α : Type u_2} {β : Type u_3} [fun_like F α (λ (_x : α), β)] [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } [add_freiman_hom_class F A β n] (f : F) {s t : multiset α} (hsA : ∀ ⦃x : α⦄, x sx A) (htA : ∀ ⦃x : α⦄, x tx A) (hs : multiset.card s = n) (ht : multiset.card t = n) (h : s.sum = t.sum) :
theorem map_add_map_eq_map_add_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [fun_like F α (λ (_x : α), β)] [add_comm_monoid α] [add_comm_monoid β] {A : set α} {a b c d : α} [add_freiman_hom_class F A β 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} [fun_like F α (λ (_x : α), β)] [comm_monoid α] [comm_monoid β] {A : set α} {a b c d : α} [freiman_hom_class F A β 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} [add_comm_monoid α] [add_comm_monoid β] {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
Equations
@[protected, instance]
def add_freiman_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } :
Equations
@[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} [add_comm_monoid α] [add_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
@[simp]
theorem add_freiman_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {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} [add_comm_monoid α] [add_comm_monoid β] {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} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } (f : α → β) (h : ∀ (s t : multiset α), (∀ ⦃x : α⦄, x sx A)(∀ ⦃x : α⦄, x tx A)multiset.card s = nmultiset.card t = ns.sum = t.sum(multiset.map f s).sum = (multiset.map f 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 sx A)(∀ ⦃x : α⦄, x tx A)multiset.card s = nmultiset.card t = ns.prod = t.prod(multiset.map f s).prod = (multiset.map f t).prod) :
@[simp]
theorem add_freiman_hom.mk_coe {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } (f : A →+[n] β) (h : ∀ {s t : multiset α}, (∀ ⦃x : α⦄, x sx A)(∀ ⦃x : α⦄, x tx A)multiset.card s = nmultiset.card t = ns.sum = t.sum(multiset.map f s).sum = (multiset.map f 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 sx A)(∀ ⦃x : α⦄, x tx A)multiset.card s = nmultiset.card t = ns.prod = t.prod(multiset.map f s).prod = (multiset.map f t).prod) :
@[simp]
theorem freiman_hom.id_apply {α : Type u_2} [comm_monoid α] (A : set α) (n : ) (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} [add_comm_monoid α] (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} [add_comm_monoid α] (A : set α) (n : ) (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 : set.maps_to g 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) (hAB : set.maps_to g A B) :
A →+[n] γ

Composition of additive Freiman homomorphisms as an additive Freiman homomorphism.

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 : set.maps_to g A B} :
(f.comp g hfg) = f g
@[simp]
theorem add_freiman_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : set.maps_to g 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 : set.maps_to g 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } (f : B →+[n] γ) (g : A →+[n] β) {hfg : set.maps_to g 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 : set.maps_to f A B} {hhg : set.maps_to g B C} {hgf : set.maps_to f 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [add_comm_monoid δ] {A : set α} {B : set β} {C : set γ} {n : } (f : A →+[n] β) (g : B →+[n] γ) (h : C →+[n] δ) {hf : set.maps_to f A B} {hhg : set.maps_to g B C} {hgf : set.maps_to f 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } {g₁ g₂ : B →+[n] γ} {f : A →+[n] β} (hf : function.surjective f) {hg₁ hg₂ : set.maps_to f 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₂ : set.maps_to f 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 : set.surj_on f A B) {hf' : set.maps_to f A B} :
set.eq_on (g₁.comp f hf') (g₂.comp f hf') A set.eq_on g₁ g₂ B
theorem add_freiman_hom.cancel_right_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } {g₁ g₂ : B →+[n] γ} {f : A →+[n] β} (hf : set.surj_on f A B) {hf' : set.maps_to f A B} :
set.eq_on (g₁.comp f hf') (g₂.comp f hf') A set.eq_on g₁ g₂ B
theorem add_freiman_hom.cancel_left_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } {g : B →+[n] γ} {f₁ f₂ : A →+[n] β} (hg : set.inj_on g B) {hf₁ : set.maps_to f₁ A B} {hf₂ : set.maps_to f₂ A B} :
set.eq_on (g.comp f₁ hf₁) (g.comp f₂ hf₂) A set.eq_on f₁ 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 : set.inj_on g B) {hf₁ : set.maps_to f₁ A B} {hf₂ : set.maps_to f₂ A B} :
set.eq_on (g.comp f₁ hf₁) (g.comp f₂ hf₂) A set.eq_on f₁ f₂ A
@[simp]
theorem add_freiman_hom.comp_id {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } (f : A →+[n] β) {hf : set.maps_to (add_freiman_hom.id A n) A A} :
@[simp]
theorem freiman_hom.comp_id {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : A →*[n] β) {hf : set.maps_to (freiman_hom.id A n) A A} :
f.comp (freiman_hom.id A n) hf = f
@[simp]
theorem add_freiman_hom.id_comp {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {B : set β} {n : } (f : A →+[n] β) {hf : set.maps_to f A B} :
@[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 : set.maps_to f A B} :
(freiman_hom.id 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} [add_comm_monoid α] [add_comm_monoid β] (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 : α) :
@[simp]
theorem add_freiman_hom.const_apply {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} (n : ) (b : β) (x : α) :
@[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 : set.maps_to f A B} :
@[simp]
theorem add_freiman_hom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} (n : ) (c : γ) (f : A →+[n] β) {hf : set.maps_to f A B} :
@[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} [add_comm_monoid α] [add_comm_monoid β] {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} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } (x : α) :
0 x = 0
@[simp]
theorem add_freiman_hom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } (f : A →+[n] β) {hf : set.maps_to f 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 : set.maps_to f A B} :
1.comp f hf = 1
@[protected, instance]
def add_freiman_hom.inhabited {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {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} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } :
has_add (A →+[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} [add_comm_monoid α] [add_comm_monoid β] {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₂ : set.maps_to f 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] {A : set α} {B : set β} {n : } (g₁ g₂ : B →+[n] γ) (f : A →+[n] β) {hg hg₁ hg₂ : set.maps_to f 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} [add_comm_monoid α] [add_comm_group G] {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} [add_comm_monoid α] [add_comm_group G] {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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_group G] {A : set α} {B : set β} {n : } (f : B →+[n] G) (g : A →+[n] β) {hf hf' : set.maps_to g 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' : set.maps_to g 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} [add_comm_monoid α] [add_comm_group G] {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} [add_comm_monoid α] [add_comm_group G] {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₂ : set.maps_to g 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} [add_comm_monoid α] [add_comm_monoid β] [add_comm_group G] {A : set α} {B : set β} {n : } (f₁ f₂ : B →+[n] G) (g : A →+[n] β) {hf hf₁ hf₂ : set.maps_to g 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} [add_comm_monoid α] [add_comm_monoid β] {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} [add_comm_monoid α] {A : set α} {n : } {β : Type u_1} [add_comm_group β] :

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.

Equations
@[protected, instance]
def add_monoid_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {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.

Equations
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} [add_comm_monoid α] [add_comm_monoid β] (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} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : } (f : α →+ β) :
@[simp]
theorem monoid_hom.to_freiman_hom_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : } (f : α →* β) :
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} [fun_like F α (λ (_x : α), β)] [add_comm_monoid α] [add_cancel_comm_monoid β] {A : set α} {m n : } [add_freiman_hom_class F A β n] (f : F) {s t : multiset α} (hsA : ∀ (x : α), x sx A) (htA : ∀ (x : α), x tx A) (hs : multiset.card s = m) (ht : multiset.card t = m) (hst : s.sum = t.sum) (h : m n) :
theorem map_prod_eq_map_prod_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [fun_like F α (λ (_x : α), β)] [comm_monoid α] [cancel_comm_monoid β] {A : set α} {m n : } [freiman_hom_class F A β n] (f : F) {s t : multiset α} (hsA : ∀ (x : α), x sx A) (htA : ∀ (x : α), x tx A) (hs : multiset.card s = m) (ht : multiset.card t = m) (hst : s.prod = t.prod) (h : m n) :
def add_freiman_hom.to_add_freiman_hom {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_cancel_comm_monoid β] {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 α] [cancel_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
def add_freiman_hom.add_freiman_hom_class_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [fun_like F α (λ (_x : α), β)] [add_comm_monoid α] [add_cancel_comm_monoid β] {A : set α} {m n : } [add_freiman_hom_class F A β n] (h : m n) :

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

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

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

Equations
@[simp]
theorem freiman_hom.to_freiman_hom_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [cancel_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} [add_comm_monoid α] [add_cancel_comm_monoid β] {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 α] [cancel_comm_monoid β] {A : set α} {m n : } (h : m n) :