algebra.hom.freiman - mathlib3 docs

source

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)

to_fun : α → β
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 self.to_fun s).sum = (multiset.map self.to_fun t).sum

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

Instances for add_freiman_hom

source

structure freiman_hom {α : Type u_2} (A : set α) (β : Type u_7) [comm_monoid α] [comm_monoid β] (n : ℕ) :

Type (max u_2 u_7)

to_fun : α → β
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 self.to_fun s).prod = (multiset.map self.to_fun t).prod

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

Instances for freiman_hom

source

@[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 : α), β)] :

Prop

map_sum_eq_map_sum' : ∀ (f : F) {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

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

source

@[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 : α), β)] :

Prop

map_prod_eq_map_prod' : ∀ (f : F) {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

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

source

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 ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : ⇑multiset.card s = n) (ht : ⇑multiset.card t = n) (h : s.prod = t.prod) :

(multiset.map ⇑f s).prod = (multiset.map ⇑f t).prod

source

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 ∈ s → x ∈ A) (htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A) (hs : ⇑multiset.card s = n) (ht : ⇑multiset.card t = n) (h : s.sum = t.sum) :

(multiset.map ⇑f s).sum = (multiset.map ⇑f t).sum

source

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

source

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

source

@[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

add_freiman_hom.fun_like = {coe := add_freiman_hom.to_fun n, coe_injective' := _}

source

@[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

freiman_hom.fun_like = {coe := freiman_hom.to_fun n, coe_injective' := _}

source

@[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

source

@[protected, instance]

def add_freiman_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : ℕ} :

add_freiman_hom_class (A →+[n] β) A β n

source

@[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

freiman_hom.has_coe_to_fun = {coe := freiman_hom.to_fun n}

source

@[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

add_freiman_hom.has_coe_to_fun = {coe := add_freiman_hom.to_fun n}

source

@[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] β) :

f.to_fun = ⇑f

source

@[simp]

theorem freiman_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : ℕ} (f : A →*[n] β) :

f.to_fun = ⇑f

source

@[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

source

@[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

source

@[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 ∈ 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) :

⇑{to_fun := f, map_sum_eq_map_sum' := h} = f

source

@[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) → ⇑multiset.card s = n → ⇑multiset.card t = n → s.prod = t.prod → (multiset.map f s).prod = (multiset.map f t).prod) :

⇑{to_fun := f, map_prod_eq_map_prod' := h} = f

source

@[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 ∈ 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) :

{to_fun := ⇑f, map_sum_eq_map_sum' := h} = f

source

@[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) → ⇑multiset.card s = n → ⇑multiset.card t = n → s.prod = t.prod → (multiset.map ⇑f s).prod = (multiset.map ⇑f t).prod) :

{to_fun := ⇑f, map_prod_eq_map_prod' := h} = f

source

@[simp]

theorem freiman_hom.id_apply {α : Type u_2} [comm_monoid α] (A : set α) (n : ℕ) (x : α) :

⇑(freiman_hom.id A n) x = x

source

@[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

freiman_hom.id A n = {to_fun := λ (x : α), x, map_prod_eq_map_prod' := _}

source

@[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

add_freiman_hom.id A n = {to_fun := λ (x : α), x, map_sum_eq_map_sum' := _}

source

@[simp]

theorem add_freiman_hom.id_apply {α : Type u_2} [add_comm_monoid α] (A : set α) (n : ℕ) (x : α) :

⇑(add_freiman_hom.id A n) x = x

source

@[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

f.comp g hAB = {to_fun := ⇑f ∘ ⇑g, map_prod_eq_map_prod' := _}

source

@[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

f.comp g hAB = {to_fun := ⇑f ∘ ⇑g, map_sum_eq_map_sum' := _}

source

@[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

source

@[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

source

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)

source

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)

source

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

source

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

source

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₂

source

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₂

source

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

source

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

source

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

source

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

source

@[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} :

f.comp (add_freiman_hom.id A n) hf = f

source

@[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

source

@[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} :

(add_freiman_hom.id B n).comp f hf = f

source

@[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

source

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

freiman_hom.const A n b = {to_fun := λ (_x : α), b, map_prod_eq_map_prod' := _}

source

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

add_freiman_hom.const A n b = {to_fun := λ (_x : α), b, map_sum_eq_map_sum' := _}

source

@[simp]

theorem freiman_hom.const_apply {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} (n : ℕ) (b : β) (x : α) :

⇑(freiman_hom.const A n b) x = b

source

@[simp]

theorem add_freiman_hom.const_apply {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} (n : ℕ) (b : β) (x : α) :

⇑(add_freiman_hom.const A n b) x = b

source

@[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} :

(freiman_hom.const B n c).comp f hf = freiman_hom.const A n c

source

@[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} :

(add_freiman_hom.const B n c).comp f hf = add_freiman_hom.const A n c

source

@[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

freiman_hom.has_one = {one := freiman_hom.const A n 1}

source

@[protected, instance]

def add_freiman_hom.has_zero {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : ℕ} :

has_zero (A →+[n] β)

0 is the Freiman homomorphism sending everything to 0.

Equations

add_freiman_hom.has_zero = {zero := add_freiman_hom.const A n 0}

source

@[simp]

theorem freiman_hom.one_apply {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : ℕ} (x : α) :

⇑1 x = 1

source

@[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

source

@[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

source

@[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

source

@[protected, instance]

def add_freiman_hom.inhabited {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : ℕ} :

inhabited (A →+[n] β)

Equations

add_freiman_hom.inhabited = {default := 0}

source

@[protected, instance]

def freiman_hom.inhabited {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : ℕ} :

inhabited (A →*[n] β)

Equations

freiman_hom.inhabited = {default := 1}

source

@[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

freiman_hom.has_mul = {mul := λ (f g : A →*[n] β), {to_fun := λ (x : α), ⇑f x * ⇑g x, map_prod_eq_map_prod' := _}}

source

@[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

add_freiman_hom.has_add = {add := λ (f g : A →+[n] β), {to_fun := λ (x : α), ⇑f x + ⇑g x, map_sum_eq_map_sum' := _}}

source

@[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

source

@[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

source

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₂

source

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₂

source

@[protected, instance]

def freiman_hom.has_inv {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : ℕ} :

has_inv (A →*[n] G)

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

Equations

freiman_hom.has_inv = {inv := λ (f : A →*[n] G), {to_fun := λ (x : α), (⇑f x)⁻¹, map_prod_eq_map_prod' := _}}

source

@[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 : ℕ} :

has_neg (A →+[n] G)

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

Equations

add_freiman_hom.has_neg = {neg := λ (f : A →+[n] G), {to_fun := λ (x : α), -⇑f x, map_sum_eq_map_sum' := _}}

source

@[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

source

@[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 : α) :

⇑f⁻¹ x = (⇑f x)⁻¹

source

@[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'

source

@[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')⁻¹

source

@[protected, instance]

def freiman_hom.has_div {α : Type u_2} {G : Type u_6} [comm_monoid α] [comm_group G] {A : set α} {n : ℕ} :

has_div (A →*[n] G)

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

freiman_hom.has_div = {div := λ (f g : A →*[n] G), {to_fun := λ (x : α), ⇑f x / ⇑g x, map_prod_eq_map_prod' := _}}

source

@[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 : ℕ} :

has_sub (A →+[n] G)

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

add_freiman_hom.has_sub = {sub := λ (f g : A →+[n] G), {to_fun := λ (x : α), ⇑f x - ⇑g x, map_sum_eq_map_sum' := _}}

source

@[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

source

@[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

source

@[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₂

source

@[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₂

source

@[protected, instance]

def add_freiman_hom.add_comm_monoid {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : ℕ} :

add_comm_monoid (A →+[n] β)

α →+[n] β is an add_comm_monoid.

Equations

add_freiman_hom.add_comm_monoid = {add := has_add.add add_freiman_hom.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := λ (m : ℕ) (f : A →+[n] β), {to_fun := λ (x : α), m • ⇑f x, map_sum_eq_map_sum' := _}, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def freiman_hom.comm_monoid {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : ℕ} :

comm_monoid (A →*[n] β)

A →*[n] β is a comm_monoid.

Equations

freiman_hom.comm_monoid = {mul := has_mul.mul freiman_hom.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := λ (m : ℕ) (f : A →*[n] β), {to_fun := λ (x : α), ⇑f x ^ m, map_prod_eq_map_prod' := _}, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def add_freiman_hom.add_comm_group {α : Type u_2} [add_comm_monoid α] {A : set α} {n : ℕ} {β : Type u_1} [add_comm_group β] :

add_comm_group (A →+[n] β)

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

Equations

add_freiman_hom.add_comm_group = {add := add_comm_monoid.add add_freiman_hom.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero add_freiman_hom.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul add_freiman_hom.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg add_freiman_hom.has_neg, sub := has_sub.sub add_freiman_hom.has_sub, sub_eq_add_neg := _, zsmul := λ (n_1 : ℤ) (f : A →+[n] β), {to_fun := λ (x : α), n_1 • ⇑f x, map_sum_eq_map_sum' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected, instance]

def freiman_hom.comm_group {α : Type u_2} [comm_monoid α] {A : set α} {n : ℕ} {β : Type u_1} [comm_group β] :

comm_group (A →*[n] β)

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

Equations

freiman_hom.comm_group = {mul := comm_monoid.mul freiman_hom.comm_monoid, mul_assoc := _, one := comm_monoid.one freiman_hom.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow freiman_hom.comm_monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv freiman_hom.has_inv, div := has_div.div freiman_hom.has_div, div_eq_mul_inv := _, zpow := λ (n_1 : ℤ) (f : A →*[n] β), {to_fun := λ (x : α), ⇑f x ^ n_1, map_prod_eq_map_prod' := _}, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

@[protected, instance]

def monoid_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {n : ℕ} :

freiman_hom_class (α →* β) set.univ β 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.

source

@[protected, instance]

def add_monoid_hom.freiman_hom_class {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {n : ℕ} :

add_freiman_hom_class (α →+ β) set.univ β 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.

source

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

monoid_hom.to_freiman_hom A n f = {to_fun := ⇑f, map_prod_eq_map_prod' := _}

source

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

add_monoid_hom.to_add_freiman_hom A n f = {to_fun := ⇑f, map_sum_eq_map_sum' := _}

source

@[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 : α →+ β) :

⇑(add_monoid_hom.to_add_freiman_hom A n f) = ⇑f

source

@[simp]

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

⇑(monoid_hom.to_freiman_hom A n f) = ⇑f

source

theorem add_monoid_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {A : set α} {n : ℕ} :

function.injective (add_monoid_hom.to_add_freiman_hom A n)

source

theorem monoid_hom.to_freiman_hom_injective {α : Type u_2} {β : Type u_3} [comm_monoid α] [comm_monoid β] {A : set α} {n : ℕ} :

function.injective (monoid_hom.to_freiman_hom A n)

source

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 ∈ s → x ∈ A) (htA : ∀ (x : α), x ∈ t → x ∈ A) (hs : ⇑multiset.card s = m) (ht : ⇑multiset.card t = m) (hst : s.sum = t.sum) (h : m ≤ n) :

(multiset.map ⇑f s).sum = (multiset.map ⇑f t).sum

source

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 ∈ s → x ∈ A) (htA : ∀ (x : α), x ∈ t → x ∈ A) (hs : ⇑multiset.card s = m) (ht : ⇑multiset.card t = m) (hst : s.prod = t.prod) (h : m ≤ n) :

(multiset.map ⇑f s).prod = (multiset.map ⇑f t).prod

source

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

add_freiman_hom.to_add_freiman_hom h f = {to_fun := ⇑f, map_sum_eq_map_sum' := _}

source

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

freiman_hom.to_freiman_hom h f = {to_fun := ⇑f, map_prod_eq_map_prod' := _}

source

theorem 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) :

add_freiman_hom_class F A β m

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

source

theorem 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) :

freiman_hom_class F A β m

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

source

@[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] β) :

⇑(freiman_hom.to_freiman_hom h f) = ⇑f

source

@[simp]