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] β
: Multiplicativen
-Freiman homomorphism onA
A →+[n] β
: Additiven
-Freiman homomorphism onA
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.
- toFun : α → β
The underlying function.
- map_sum_eq_map_sum' : ∀ {s_1 t : Multiset α}, (∀ ⦃x : α⦄, x ∈ s_1 → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → ↑Multiset.card s_1 = n → ↑Multiset.card t = n → Multiset.sum s_1 = Multiset.sum t → Multiset.sum (Multiset.map s.toFun s_1) = Multiset.sum (Multiset.map s.toFun t)
An additive
n
-Freiman homomorphism preserves sums ofn
elements.
An additive n
-Freiman homomorphism is a map which preserves sums of n
elements.
Instances For
- toFun : α → β
The underlying function.
- map_prod_eq_map_prod' : ∀ {s_1 t : Multiset α}, (∀ ⦃x : α⦄, x ∈ s_1 → x ∈ A) → (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → ↑Multiset.card s_1 = n → ↑Multiset.card t = n → Multiset.prod s_1 = Multiset.prod t → Multiset.prod (Multiset.map s.toFun s_1) = Multiset.prod (Multiset.map s.toFun t)
An
n
-Freiman homomorphism preserves products ofn
elements.
An n
-Freiman homomorphism on a set A
is a map which preserves products of n
elements.
Instances For
An additive n
-Freiman homomorphism is a map which preserves sums of n
elements.
Instances For
An n
-Freiman homomorphism on a set A
is a map which preserves products of n
elements.
Instances For
- 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 → Multiset.sum s = Multiset.sum t → Multiset.sum (Multiset.map (↑f) s) = Multiset.sum (Multiset.map (↑f) t)
An additive
n
-Freiman homomorphism preserves sums ofn
elements.
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
.
Instances
- 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 → Multiset.prod s = Multiset.prod t → Multiset.prod (Multiset.map (↑f) s) = Multiset.prod (Multiset.map (↑f) t)
An
n
-Freiman homomorphism preserves products ofn
elements.
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
.
Instances
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
.
Instances For
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
.
Instances For
Any type satisfying SMulHomClass
can be cast into MulActionHom
via
SMulHomClass.toMulActionHom
.
The identity map from an additive commutative monoid to itself.
Instances For
The identity map from a commutative monoid to itself.
Instances For
Composition of additive Freiman homomorphisms as an additive Freiman homomorphism.
Instances For
Composition of Freiman homomorphisms as a Freiman homomorphism.
Instances For
AddFreimanHom.const An b
is the Freiman homomorphism sending everything to b
.
Instances For
FreimanHom.const A n b
is the Freiman homomorphism sending everything to b
.
Instances For
0
is the Freiman homomorphism sending everything to 0
.
1
is the Freiman homomorphism sending everything to 1
.
f + g
is the Freiman homomorphism sending x
to f x + g x
.
f * g
is the Freiman homomorphism sends x
to f x * g x
.
If f
is a Freiman homomorphism to an additive commutative group, then -f
is the
Freiman homomorphism sending x
to -f x
.
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
Instances #
α →+[n] β
is an AddCommMonoid
.
A →*[n] β
is a CommMonoid
.
If β
is an additive commutative group, then A →*[n] β
is an additive commutative
group too.
Hom hierarchy #
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.
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.
An AddMonoidHom
is naturally an AddFreimanHom
Instances For
A MonoidHom
is naturally a FreimanHom
.
Instances For
α →+[n] β
is naturally included in α →+[m] β
for any m ≤ n
Instances For
α →*[n] β
is naturally included in A →*[m] β
for any m ≤ n
.
Instances For
An additive n
-Freiman homomorphism is
also an additive m
-Freiman homomorphism for any m ≤ n
.
An n
-Freiman homomorphism is also a m
-Freiman homomorphism for any m ≤ n
.