Freiman homomorphisms

In this file, we define Freiman homomorphisms. An 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 MulHom is a Freiman homomorphism.

They are of interest in additive combinatorics.

Main declaration

• FreimanHom: Freiman homomorphism.
• AddFreimanHom: 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 AddMonoid/Monoid instead of the AddMonoid/Monoid itself.

References

Yufei Zhao, 18.225: Graph Theory and Additive Combinatorics

TODO

MonoidHom.toFreimanHom 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.

Define n-Freiman isomorphisms.

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

structure AddFreimanHom {α : Type u_2} (A : Set α) (β : Type u_7) [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) : Type (max u_2 u_7)

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

• toFun : α → β

  The underlying function.

• 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.toFun s).sum = (Multiset.map self.toFun t).sum

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

theorem AddFreimanHom.map_sum_eq_map_sum' {α : Type u_2} {A : Set α} {β : Type u_7} [AddCommMonoid α] [AddCommMonoid β] {n : ℕ} (self : A →+[n] β) {s : Multiset α} {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 self.toFun s).sum = (Multiset.map self.toFun t).sum

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

structure FreimanHom {α : Type u_2} (A : Set α) (β : Type u_7) [CommMonoid α] [CommMonoid β] (n : ℕ) : Type (max u_2 u_7)

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

• toFun : α → β

  The underlying function.

• 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.toFun s).prod = (Multiset.map self.toFun t).prod

  An n-Freiman homomorphism preserves products of n elements.

theorem FreimanHom.map_prod_eq_map_prod' {α : Type u_2} {A : Set α} {β : Type u_7} [CommMonoid α] [CommMonoid β] {n : ℕ} (self : A →*[n] β) {s : Multiset α} {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 self.toFun s).prod = (Multiset.map self.toFun t).prod

An n-Freiman homomorphism preserves products of n elements.

def «AddFreimanHomLocal≺» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

def «FreimanHomLocal≺» : Lean.TrailingParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

class AddFreimanHomClass {α : Type u_2} (F : Type u_7) (A : outParam (Set α)) (β : outParam (Type u_8)) [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) [FunLike F α β] : Prop

AddFreimanHomClass F A β n states that F is a type of n-ary sums-preserving morphisms. You should extend this class when you extend AddFreimanHom.

• 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

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

theorem AddFreimanHomClass.map_sum_eq_map_sum' {α : Type u_2} {F : Type u_7} {A : outParam (Set α)} {β : outParam (Type u_8)} [AddCommMonoid α] [AddCommMonoid β] {n : ℕ} [FunLike F α β] [self : AddFreimanHomClass F A β n] (f : F) {s : Multiset α} {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

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

class FreimanHomClass {α : Type u_2} (F : Type u_7) (A : outParam (Set α)) (β : outParam (Type u_8)) [CommMonoid α] [CommMonoid β] (n : ℕ) [FunLike F α β] : Prop

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

• 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

  An n-Freiman homomorphism preserves products of n elements.

theorem FreimanHomClass.map_prod_eq_map_prod' {α : Type u_2} {F : Type u_7} {A : outParam (Set α)} {β : outParam (Type u_8)} [CommMonoid α] [CommMonoid β] {n : ℕ} [FunLike F α β] [self : FreimanHomClass F A β n] (f : F) {s : Multiset α} {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

An n-Freiman homomorphism preserves products of n elements.

def AddFreimanHomClass.toFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} [AddFreimanHomClass F A β n] (f : F) : A →+[n] β

Turn an element of a type F satisfying AddFreimanHomClass F A β n into an actual AddFreimanHom. This is declared as the default coercion from F to AddFreimanHom A β n.

Equations

• ↑f = { toFun := ⇑f, map_sum_eq_map_sum' := ⋯ }

def FreimanHomClass.toFreimanHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} [FreimanHomClass F A β n] (f : F) : A →*[n] β

Turn an element of a type F satisfying FreimanHomClass F A β n into an actual FreimanHom. This is declared as the default coercion from F to FreimanHom A β n.

Equations

• ↑f = { toFun := ⇑f, map_prod_eq_map_prod' := ⋯ }

instance instCoeTCFreimanHomOfFreimanHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} [FreimanHomClass F A β n] : CoeTC F (A →*[n] β)

Any type satisfying SMulHomClass can be cast into MulActionHom via SMulHomClass.toMulActionHom.

Equations

• instCoeTCFreimanHomOfFreimanHomClass = { coe := FreimanHomClass.toFreimanHom }

theorem map_sum_eq_map_sum {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} [AddFreimanHomClass F A β n] (f : F) {s : Multiset α} {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

theorem map_prod_eq_map_prod {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} [FreimanHomClass F A β n] (f : F) {s : Multiset α} {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

theorem map_add_map_eq_map_add_map {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {a : α} {b : α} {c : α} {d : α} [AddFreimanHomClass 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} [FunLike F α β] [CommMonoid α] [CommMonoid β] {A : Set α} {a : α} {b : α} {c : α} {d : α} [FreimanHomClass 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 AddFreimanHom.instFunLike.proof_1 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : A →+[n] β) (g : A →+[n] β) (h : f.toFun = g.toFun) : f = g

instance AddFreimanHom.instFunLike {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : FunLike (A →+[n] β) α β

Equations

• AddFreimanHom.instFunLike = { coe := AddFreimanHom.toFun, coe_injective' := ⋯ }

instance FreimanHom.instFunLike {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : FunLike (A →*[n] β) α β

Equations

• FreimanHom.instFunLike = { coe := FreimanHom.toFun, coe_injective' := ⋯ }

instance AddFreimanHom.addFreimanHomClass {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : AddFreimanHomClass (A →+[n] β) A β n

Equations

• ⋯ = ⋯

instance FreimanHom.freimanHomClass {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : FreimanHomClass (A →*[n] β) A β n

Equations

• ⋯ = ⋯

@[simp]

theorem AddFreimanHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : A →+[n] β) : f.toFun = ⇑f

@[simp]

theorem FreimanHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} (f : A →*[n] β) : f.toFun = ⇑f

theorem AddFreimanHom.ext {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} ⦃f : A →+[n] β⦄ ⦃g : A →+[n] β⦄ (h : ∀ (x : α), f x = g x) : f = g

theorem FreimanHom.ext {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} ⦃f : A →*[n] β⦄ ⦃g : A →*[n] β⦄ (h : ∀ (x : α), f x = g x) : f = g

@[simp]

theorem AddFreimanHom.coe_mk {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {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) : ⇑{ toFun := f, map_sum_eq_map_sum' := ⋯ } = f

@[simp]

theorem FreimanHom.coe_mk {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {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) : ⇑{ toFun := f, map_prod_eq_map_prod' := ⋯ } = f

@[simp]

theorem AddFreimanHom.mk_coe {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {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) : { toFun := ⇑f, map_sum_eq_map_sum' := h } = f

@[simp]

theorem FreimanHom.mk_coe {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {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) : { toFun := ⇑f, map_prod_eq_map_prod' := h } = f

theorem AddFreimanHom.id.proof_1 {α : Type u_1} [AddCommMonoid α] (A : Set α) (n : ℕ) : ∀ {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 (fun (x : α) => x) s).sum = (Multiset.map (fun (x : α) => x) t).sum

def AddFreimanHom.id {α : Type u_2} [AddCommMonoid α] (A : Set α) (n : ℕ) : A →+[n] α

The identity map from an additive commutative monoid to itself.

Equations

• AddFreimanHom.id A n = { toFun := fun (x : α) => x, map_sum_eq_map_sum' := ⋯ }

@[simp]

theorem AddFreimanHom.id_apply {α : Type u_2} [AddCommMonoid α] (A : Set α) (n : ℕ) (x : α) : (AddFreimanHom.id A n) x = x

@[simp]

theorem FreimanHom.id_apply {α : Type u_2} [CommMonoid α] (A : Set α) (n : ℕ) (x : α) : (FreimanHom.id A n) x = x

def FreimanHom.id {α : Type u_2} [CommMonoid α] (A : Set α) (n : ℕ) : A →*[n] α

The identity map from a commutative monoid to itself.

Equations

• FreimanHom.id A n = { toFun := fun (x : α) => x, map_prod_eq_map_prod' := ⋯ }

theorem AddFreimanHom.comp.proof_1 {α : Type u_1} {β : Type u_3} {γ : Type u_2} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →+[n] γ) (g : A →+[n] β) (hAB : Set.MapsTo (⇑g) A B) : ∀ {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 ∘ ⇑g) s).sum = (Multiset.map (⇑f ∘ ⇑g) t).sum

def AddFreimanHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →+[n] γ) (g : A →+[n] β) (hAB : Set.MapsTo (⇑g) A B) : A →+[n] γ

Composition of additive Freiman homomorphisms as an additive Freiman homomorphism.

Equations

• f.comp g hAB = { toFun := ⇑f ∘ ⇑g, map_sum_eq_map_sum' := ⋯ }

def FreimanHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →*[n] γ) (g : A →*[n] β) (hAB : Set.MapsTo (⇑g) A B) : A →*[n] γ

Composition of Freiman homomorphisms as a Freiman homomorphism.

Equations

• f.comp g hAB = { toFun := ⇑f ∘ ⇑g, map_prod_eq_map_prod' := ⋯ }

@[simp]

theorem AddFreimanHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →+[n] γ) (g : A →+[n] β) {hfg : Set.MapsTo (⇑g) A B} : ⇑(f.comp g hfg) = ⇑f ∘ ⇑g

@[simp]

theorem FreimanHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →*[n] γ) (g : A →*[n] β) {hfg : Set.MapsTo (⇑g) A B} : ⇑(f.comp g hfg) = ⇑f ∘ ⇑g

theorem AddFreimanHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →+[n] γ) (g : A →+[n] β) {hfg : Set.MapsTo (⇑g) A B} (x : α) : (f.comp g hfg) x = f (g x)

theorem FreimanHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : B →*[n] γ) (g : A →*[n] β) {hfg : Set.MapsTo (⇑g) A B} (x : α) : (f.comp g hfg) x = f (g x)

theorem AddFreimanHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [AddCommMonoid δ] {A : Set α} {B : Set β} {C : Set γ} {n : ℕ} (f : A →+[n] β) (g : B →+[n] γ) (h : C →+[n] δ) {hf : Set.MapsTo (⇑f) A B} {hhg : Set.MapsTo (⇑g) B C} {hgf : Set.MapsTo (⇑f) A B} {hh : Set.MapsTo (⇑(g.comp f hgf)) A C} : (h.comp g hhg).comp f hf = h.comp (g.comp f hgf) hh

theorem FreimanHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [CommMonoid α] [CommMonoid β] [CommMonoid γ] [CommMonoid δ] {A : Set α} {B : Set β} {C : Set γ} {n : ℕ} (f : A →*[n] β) (g : B →*[n] γ) (h : C →*[n] δ) {hf : Set.MapsTo (⇑f) A B} {hhg : Set.MapsTo (⇑g) B C} {hgf : Set.MapsTo (⇑f) A B} {hh : Set.MapsTo (⇑(g.comp f hgf)) A C} : (h.comp g hhg).comp f hf = h.comp (g.comp f hgf) hh

@[simp]

theorem AddFreimanHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g₁ : B →+[n] γ} {g₂ : B →+[n] γ} {f : A →+[n] β} (hf : Function.Surjective ⇑f) {hg₁ : Set.MapsTo (⇑f) A B} {hg₂ : Set.MapsTo (⇑f) A B} : g₁.comp f hg₁ = g₂.comp f hg₂ ↔ g₁ = g₂

@[simp]

theorem FreimanHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g₁ : B →*[n] γ} {g₂ : B →*[n] γ} {f : A →*[n] β} (hf : Function.Surjective ⇑f) {hg₁ : Set.MapsTo (⇑f) A B} {hg₂ : Set.MapsTo (⇑f) A B} : g₁.comp f hg₁ = g₂.comp f hg₂ ↔ g₁ = g₂

theorem AddFreimanHom.cancel_right_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g₁ : B →+[n] γ} {g₂ : B →+[n] γ} {f : A →+[n] β} (hf : Set.SurjOn (⇑f) A B) {hf' : Set.MapsTo (⇑f) A B} : Set.EqOn (⇑(g₁.comp f hf')) (⇑(g₂.comp f hf')) A ↔ Set.EqOn (⇑g₁) (⇑g₂) B

theorem FreimanHom.cancel_right_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g₁ : B →*[n] γ} {g₂ : B →*[n] γ} {f : A →*[n] β} (hf : Set.SurjOn (⇑f) A B) {hf' : Set.MapsTo (⇑f) A B} : Set.EqOn (⇑(g₁.comp f hf')) (⇑(g₂.comp f hf')) A ↔ Set.EqOn (⇑g₁) (⇑g₂) B

theorem AddFreimanHom.cancel_left_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g : B →+[n] γ} {f₁ : A →+[n] β} {f₂ : A →+[n] β} (hg : Set.InjOn (⇑g) B) {hf₁ : Set.MapsTo (⇑f₁) A B} {hf₂ : Set.MapsTo (⇑f₂) A B} : Set.EqOn (⇑(g.comp f₁ hf₁)) (⇑(g.comp f₂ hf₂)) A ↔ Set.EqOn (⇑f₁) (⇑f₂) A

theorem FreimanHom.cancel_left_on {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} {g : B →*[n] γ} {f₁ : A →*[n] β} {f₂ : A →*[n] β} (hg : Set.InjOn (⇑g) B) {hf₁ : Set.MapsTo (⇑f₁) A B} {hf₂ : Set.MapsTo (⇑f₂) A B} : Set.EqOn (⇑(g.comp f₁ hf₁)) (⇑(g.comp f₂ hf₂)) A ↔ Set.EqOn (⇑f₁) (⇑f₂) A

@[simp]

theorem AddFreimanHom.comp_id {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : A →+[n] β) {hf : Set.MapsTo (⇑(AddFreimanHom.id A n)) A A} : f.comp (AddFreimanHom.id A n) hf = f

@[simp]

theorem FreimanHom.comp_id {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} (f : A →*[n] β) {hf : Set.MapsTo (⇑(FreimanHom.id A n)) A A} : f.comp (FreimanHom.id A n) hf = f

@[simp]

theorem AddFreimanHom.id_comp {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {B : Set β} {n : ℕ} (f : A →+[n] β) {hf : Set.MapsTo (⇑f) A B} : (AddFreimanHom.id B n).comp f hf = f

@[simp]

theorem FreimanHom.id_comp {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {B : Set β} {n : ℕ} (f : A →*[n] β) {hf : Set.MapsTo (⇑f) A B} : (FreimanHom.id B n).comp f hf = f

theorem AddFreimanHom.const.proof_1 {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCommMonoid β] (A : Set α) (n : ℕ) (b : β) : ∀ {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 (fun (x : α) => b) s).sum = (Multiset.map (fun (x : α) => b) t).sum

def AddFreimanHom.const {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (A : Set α) (n : ℕ) (b : β) : A →+[n] β

AddFreimanHom.const An b is the Freiman homomorphism sending everything to b.

Equations

• AddFreimanHom.const A n b = { toFun := fun (x : α) => b, map_sum_eq_map_sum' := ⋯ }

def FreimanHom.const {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (A : Set α) (n : ℕ) (b : β) : A →*[n] β

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

Equations

• FreimanHom.const A n b = { toFun := fun (x : α) => b, map_prod_eq_map_prod' := ⋯ }

@[simp]

theorem AddFreimanHom.const_apply {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} (n : ℕ) (b : β) (x : α) : (AddFreimanHom.const A n b) x = b

@[simp]

theorem FreimanHom.const_apply {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} (n : ℕ) (b : β) (x : α) : (FreimanHom.const A n b) x = b

@[simp]

theorem AddFreimanHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} (n : ℕ) (c : γ) (f : A →+[n] β) {hf : Set.MapsTo (⇑f) A B} : (AddFreimanHom.const B n c).comp f hf = AddFreimanHom.const A n c

@[simp]

theorem FreimanHom.const_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} (n : ℕ) (c : γ) (f : A →*[n] β) {hf : Set.MapsTo (⇑f) A B} : (FreimanHom.const B n c).comp f hf = FreimanHom.const A n c

instance AddFreimanHom.instZero {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : Zero (A →+[n] β)

0 is the Freiman homomorphism sending everything to 0.

Equations

• AddFreimanHom.instZero = { zero := AddFreimanHom.const A n 0 }

instance FreimanHom.instOne {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : One (A →*[n] β)

1 is the Freiman homomorphism sending everything to 1.

Equations

• FreimanHom.instOne = { one := FreimanHom.const A n 1 }

@[simp]

theorem AddFreimanHom.zero_apply {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (x : α) : 0 x = 0

@[simp]

theorem FreimanHom.one_apply {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} (x : α) : 1 x = 1

@[simp]

theorem AddFreimanHom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : A →+[n] β) {hf : Set.MapsTo (⇑f) A B} : AddFreimanHom.comp 0 f hf = 0

@[simp]

theorem FreimanHom.one_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (f : A →*[n] β) {hf : Set.MapsTo (⇑f) A B} : FreimanHom.comp 1 f hf = 1

instance AddFreimanHom.instInhabited {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : Inhabited (A →+[n] β)

Equations

• AddFreimanHom.instInhabited = { default := 0 }

instance FreimanHom.instInhabited {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : Inhabited (A →*[n] β)

Equations

• FreimanHom.instInhabited = { default := 1 }

theorem AddFreimanHom.instAdd.proof_1 {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : A →+[n] β) (g : A →+[n] β) : ∀ {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 (fun (x : α) => f x + g x) s).sum = (Multiset.map (fun (x : α) => f x + g x) t).sum

instance AddFreimanHom.instAdd {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : Add (A →+[n] β)

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

Equations

• AddFreimanHom.instAdd = { add := fun (f g : A →+[n] β) => { toFun := fun (x : α) => f x + g x, map_sum_eq_map_sum' := ⋯ } }

instance FreimanHom.instMul {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : Mul (A →*[n] β)

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

Equations

• FreimanHom.instMul = { mul := fun (f g : A →*[n] β) => { toFun := fun (x : α) => f x * g x, map_prod_eq_map_prod' := ⋯ } }

@[simp]

theorem AddFreimanHom.add_apply {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : A →+[n] β) (g : A →+[n] β) (x : α) : (f + g) x = f x + g x

@[simp]

theorem FreimanHom.mul_apply {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} (f : A →*[n] β) (g : A →*[n] β) (x : α) : (f * g) x = f x * g x

theorem AddFreimanHom.add_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (g₁ : B →+[n] γ) (g₂ : B →+[n] γ) (f : A →+[n] β) {hg : Set.MapsTo (⇑f) A B} {hg₁ : Set.MapsTo (⇑f) A B} {hg₂ : Set.MapsTo (⇑f) A B} : (g₁ + g₂).comp f hg = g₁.comp f hg₁ + g₂.comp f hg₂

theorem FreimanHom.mul_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [CommMonoid α] [CommMonoid β] [CommMonoid γ] {A : Set α} {B : Set β} {n : ℕ} (g₁ : B →*[n] γ) (g₂ : B →*[n] γ) (f : A →*[n] β) {hg : Set.MapsTo (⇑f) A B} {hg₁ : Set.MapsTo (⇑f) A B} {hg₂ : Set.MapsTo (⇑f) A B} : (g₁ * g₂).comp f hg = g₁.comp f hg₁ * g₂.comp f hg₂

instance AddFreimanHom.instNeg {α : Type u_2} {G : Type u_6} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} : 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

• AddFreimanHom.instNeg = { neg := fun (f : A →+[n] G) => { toFun := fun (x : α) => -f x, map_sum_eq_map_sum' := ⋯ } }

theorem AddFreimanHom.instNeg.proof_1 {α : Type u_1} {G : Type u_2} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} (f : A →+[n] G) : ∀ {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 (fun (x : α) => -f x) s).sum = (Multiset.map (fun (x : α) => -f x) t).sum

instance FreimanHom.instInv {α : Type u_2} {G : Type u_6} [CommMonoid α] [CommGroup G] {A : Set α} {n : ℕ} : 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

• FreimanHom.instInv = { inv := fun (f : A →*[n] G) => { toFun := fun (x : α) => (f x)⁻¹, map_prod_eq_map_prod' := ⋯ } }

@[simp]

theorem AddFreimanHom.neg_apply {α : Type u_2} {G : Type u_6} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} (f : A →+[n] G) (x : α) : (-f) x = -f x

@[simp]

theorem FreimanHom.inv_apply {α : Type u_2} {G : Type u_6} [CommMonoid α] [CommGroup G] {A : Set α} {n : ℕ} (f : A →*[n] G) (x : α) : f⁻¹ x = (f x)⁻¹

@[simp]

theorem AddFreimanHom.neg_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [AddCommMonoid α] [AddCommMonoid β] [AddCommGroup G] {A : Set α} {B : Set β} {n : ℕ} (f : B →+[n] G) (g : A →+[n] β) {hf : Set.MapsTo (⇑g) A B} {hf' : Set.MapsTo (⇑g) A B} : (-f).comp g hf = -f.comp g hf'

@[simp]

theorem FreimanHom.inv_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [CommMonoid α] [CommMonoid β] [CommGroup G] {A : Set α} {B : Set β} {n : ℕ} (f : B →*[n] G) (g : A →*[n] β) {hf : Set.MapsTo (⇑g) A B} {hf' : Set.MapsTo (⇑g) A B} : f⁻¹.comp g hf = (f.comp g hf')⁻¹

instance AddFreimanHom.instSub {α : Type u_2} {G : Type u_6} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} : 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

• AddFreimanHom.instSub = { sub := fun (f g : A →+[n] G) => { toFun := fun (x : α) => f x - g x, map_sum_eq_map_sum' := ⋯ } }

theorem AddFreimanHom.instSub.proof_1 {α : Type u_1} {G : Type u_2} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} (f : A →+[n] G) (g : A →+[n] G) : ∀ {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 (fun (x : α) => f x - g x) s).sum = (Multiset.map (fun (x : α) => f x - g x) t).sum

instance FreimanHom.instDiv {α : Type u_2} {G : Type u_6} [CommMonoid α] [CommGroup G] {A : Set α} {n : ℕ} : 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

• FreimanHom.instDiv = { div := fun (f g : A →*[n] G) => { toFun := fun (x : α) => f x / g x, map_prod_eq_map_prod' := ⋯ } }

@[simp]

theorem AddFreimanHom.sub_apply {α : Type u_2} {G : Type u_6} [AddCommMonoid α] [AddCommGroup G] {A : Set α} {n : ℕ} (f : A →+[n] G) (g : A →+[n] G) (x : α) : (f - g) x = f x - g x

@[simp]

theorem FreimanHom.div_apply {α : Type u_2} {G : Type u_6} [CommMonoid α] [CommGroup G] {A : Set α} {n : ℕ} (f : A →*[n] G) (g : A →*[n] G) (x : α) : (f / g) x = f x / g x

@[simp]

theorem AddFreimanHom.sub_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [AddCommMonoid α] [AddCommMonoid β] [AddCommGroup G] {A : Set α} {B : Set β} {n : ℕ} (f₁ : B →+[n] G) (f₂ : B →+[n] G) (g : A →+[n] β) {hf : Set.MapsTo (⇑g) A B} {hf₁ : Set.MapsTo (⇑g) A B} {hf₂ : Set.MapsTo (⇑g) A B} : (f₁ - f₂).comp g hf = f₁.comp g hf₁ - f₂.comp g hf₂

@[simp]

theorem FreimanHom.div_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [CommMonoid α] [CommMonoid β] [CommGroup G] {A : Set α} {B : Set β} {n : ℕ} (f₁ : B →*[n] G) (f₂ : B →*[n] G) (g : A →*[n] β) {hf : Set.MapsTo (⇑g) A B} {hf₁ : Set.MapsTo (⇑g) A B} {hf₂ : Set.MapsTo (⇑g) A B} : (f₁ / f₂).comp g hf = f₁.comp g hf₁ / f₂.comp g hf₂

Instances

theorem AddFreimanHom.addCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : ∀ (n_1 : ℕ) (x : A →+[n] β), nsmulRec (n_1 + 1) x = nsmulRec (n_1 + 1) x

theorem AddFreimanHom.addCommMonoid.proof_3 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (a : A →+[n] β) : a + 0 = a

theorem AddFreimanHom.addCommMonoid.proof_6 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (a : A →+[n] β) (b : A →+[n] β) : a + b = b + a

theorem AddFreimanHom.addCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (a : A →+[n] β) : 0 + a = a

instance AddFreimanHom.addCommMonoid {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : AddCommMonoid (A →+[n] β)

α →+[n] β is an AddCommMonoid.

Equations

• AddFreimanHom.addCommMonoid = AddCommMonoid.mk ⋯

theorem AddFreimanHom.addCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : ∀ (x : A →+[n] β), nsmulRec 0 x = nsmulRec 0 x

theorem AddFreimanHom.addCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (a : A →+[n] β) (b : A →+[n] β) (c : A →+[n] β) : a + b + c = a + (b + c)

instance FreimanHom.commMonoid {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : CommMonoid (A →*[n] β)

A →*[n] β is a CommMonoid.

Equations

• FreimanHom.commMonoid = CommMonoid.mk ⋯

theorem AddFreimanHom.addCommGroup.proof_4 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] : ∀ (n_1 : ℕ) (a : A →+[n] β), zsmulRec (Int.negSucc n_1) a = zsmulRec (Int.negSucc n_1) a

theorem AddFreimanHom.addCommGroup.proof_5 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] : ∀ (a : A →+[n] β), -a + a = 0

theorem AddFreimanHom.addCommGroup.proof_3 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] : ∀ (n_1 : ℕ) (a : A →+[n] β), zsmulRec (Int.ofNat n_1.succ) a = zsmulRec (Int.ofNat n_1.succ) a

theorem AddFreimanHom.addCommGroup.proof_1 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] : ∀ (a b : A →+[n] β), a - b = a + -b

instance AddFreimanHom.addCommGroup {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_7} [AddCommGroup β] : AddCommGroup (A →+[n] β)

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

Equations

• AddFreimanHom.addCommGroup = let __src := AddFreimanHom.addCommMonoid; AddCommGroup.mk ⋯

theorem AddFreimanHom.addCommGroup.proof_2 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] : ∀ (a : A →+[n] β), zsmulRec 0 a = zsmulRec 0 a

theorem AddFreimanHom.addCommGroup.proof_6 {α : Type u_2} [AddCommMonoid α] {A : Set α} {n : ℕ} {β : Type u_1} [AddCommGroup β] (a : A →+[n] β) (b : A →+[n] β) : a + b = b + a

instance FreimanHom.commGroup {α : Type u_2} [CommMonoid α] {A : Set α} {n : ℕ} {β : Type u_7} [CommGroup β] : CommGroup (A →*[n] β)

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

Equations

• FreimanHom.commGroup = let __src := FreimanHom.commMonoid; CommGroup.mk ⋯

Hom hierarchy

instance AddMonoidHom.addFreimanHomClass {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {n : ℕ} : AddFreimanHomClass (α →+ β) Set.univ β n

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

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

Equations

• ⋯ = ⋯

instance MonoidHom.freimanHomClass {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {n : ℕ} : FreimanHomClass (α →* β) Set.univ β n

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

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

Equations

• ⋯ = ⋯

def AddMonoidHom.toAddFreimanHom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (A : Set α) (n : ℕ) (f : α →+ β) : A →+[n] β

An AddMonoidHom is naturally an AddFreimanHom

Equations

• AddMonoidHom.toAddFreimanHom A n f = { toFun := ⇑f, map_sum_eq_map_sum' := ⋯ }

theorem AddMonoidHom.toAddFreimanHom.proof_1 {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCommMonoid β] (A : Set α) (n : ℕ) (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

def MonoidHom.toFreimanHom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] (A : Set α) (n : ℕ) (f : α →* β) : A →*[n] β

A MonoidHom is naturally a FreimanHom.

Equations

• MonoidHom.toFreimanHom A n f = { toFun := ⇑f, map_prod_eq_map_prod' := ⋯ }

@[simp]

theorem AddMonoidHom.toAddFreimanHom_coe {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} (f : α →+ β) : ⇑(AddMonoidHom.toAddFreimanHom A n f) = ⇑f

@[simp]

theorem MonoidHom.toFreimanHom_coe {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} (f : α →* β) : ⇑(MonoidHom.toFreimanHom A n f) = ⇑f

theorem AddMonoidHom.toAddFreimanHom_injective {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {A : Set α} {n : ℕ} : Function.Injective (AddMonoidHom.toAddFreimanHom A n)

theorem MonoidHom.toFreimanHom_injective {α : Type u_2} {β : Type u_3} [CommMonoid α] [CommMonoid β] {A : Set α} {n : ℕ} : Function.Injective (MonoidHom.toFreimanHom A n)

theorem map_sum_eq_map_sum_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} [AddFreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ x ∈ s, x ∈ A) (htA : ∀ 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

theorem map_prod_eq_map_prod_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} [FreimanHomClass F A β n] (f : F) {s : Multiset α} {t : Multiset α} (hsA : ∀ x ∈ s, x ∈ A) (htA : ∀ 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

theorem AddFreimanHom.toAddFreimanHom.proof_1 {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) (f : A →+[n] β) : ∀ {s t : Multiset α}, (∀ ⦃x : α⦄, x ∈ s → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → Multiset.card s = m → Multiset.card t = m → s.sum = t.sum → (Multiset.map (⇑f) s).sum = (Multiset.map (⇑f) t).sum

def AddFreimanHom.toAddFreimanHom {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) (f : A →+[n] β) : A →+[m] β

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

Equations

• AddFreimanHom.toAddFreimanHom h f = { toFun := ⇑f, map_sum_eq_map_sum' := ⋯ }

def FreimanHom.toFreimanHom {α : Type u_2} {β : Type u_3} [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) (f : A →*[n] β) : A →*[m] β

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

Equations

• FreimanHom.toFreimanHom h f = { toFun := ⇑f, map_prod_eq_map_prod' := ⋯ }

theorem AddFreimanHom.addFreimanHomClass_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} [AddFreimanHomClass F A β n] (h : m ≤ n) : AddFreimanHomClass F A β m

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

theorem FreimanHom.FreimanHomClass_of_le {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} [FreimanHomClass F A β n] (h : m ≤ n) : FreimanHomClass F A β m

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

@[simp]

theorem AddFreimanHom.toAddFreimanHom_coe {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) (f : A →+[n] β) : ⇑(AddFreimanHom.toAddFreimanHom h f) = ⇑f

@[simp]

theorem FreimanHom.toFreimanHom_coe {α : Type u_2} {β : Type u_3} [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) (f : A →*[n] β) : ⇑(FreimanHom.toFreimanHom h f) = ⇑f

theorem AddFreimanHom.toAddFreimanHom_injective {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [AddCancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) : Function.Injective (AddFreimanHom.toAddFreimanHom h)

theorem FreimanHom.toFreimanHom_injective {α : Type u_2} {β : Type u_3} [CommMonoid α] [CancelCommMonoid β] {A : Set α} {m : ℕ} {n : ℕ} (h : m ≤ n) : Function.Injective (FreimanHom.toFreimanHom h)