Affine maps and affine subspaces over 𝔽₂

For maps between 𝔽₂-vector spaces, preserving sums of three points (Cslib.BitString.IsAffine) is the usual notion of affinity (Cslib.BitString.isAffine_iff_exists_affineMap): g is a Mathlib affine map over Bool with linear part x ↦ g x + g 0 (Cslib.BitString.IsAffine.linearMap, Cslib.BitString.IsAffine.toAffineMap). The image of an injective affine map from V is an affine subspace whose direction has the dimension of V (Cslib.BitString.IsAffine.finrank_direction_map_top).

Main definitions

• Cslib.BitString.IsAffine.linearMap: the linear part x ↦ g x + g 0 of an affine map over 𝔽₂.
• Cslib.BitString.IsAffine.toAffineMap: an affine map over 𝔽₂ as a Mathlib affine map.

Main results

• Cslib.BitString.isAffine_iff_exists_affineMap: a map between 𝔽₂-vector spaces is IsAffine if and only if it is a Mathlib affine map over Bool.
• Cslib.BitString.IsAffine.finrank_direction_map_top: the image of an injective affine map from V is an affine subspace whose direction has dimension finrank Bool V.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits, Definition 2.1

def Cslib.BitString.IsAffine.linearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : V →ₗ[Bool] W

The linear part x ↦ g x + g 0 of a map g that is affine over 𝔽₂.

@[simp]

theorem Cslib.BitString.IsAffine.linearMap_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (x : V) : hg.linearMap x = g x + g 0

The linear part of g sends x to g x + g 0.

theorem Cslib.BitString.IsAffine.linearMap_injective {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (hinj : Function.Injective g) : Function.Injective ⇑hg.linearMap

The linear part of an injective map that is affine over 𝔽₂ is injective.

def Cslib.BitString.IsAffine.toAffineMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : V →ᵃ[Bool] W

A map that is affine over 𝔽₂ (IsAffine) as a Mathlib affine map over Bool, with linear part x ↦ g x + g 0.

@[simp]

theorem Cslib.BitString.IsAffine.coe_toAffineMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : ⇑hg.toAffineMap = g

As a function, the Mathlib affine map of g is g itself.

theorem Cslib.BitString.isAffine_iff_exists_affineMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} : IsAffine g ↔ ∃ (f : V →ᵃ[Bool] W), ⇑f = g

A map between 𝔽₂-vector spaces is affine (IsAffine) if and only if it is a Mathlib affine map over Bool.

theorem Cslib.BitString.IsAffine.finrank_direction_map_top {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (hinj : Function.Injective g) : Module.finrank Bool ↥(AffineSubspace.map hg.toAffineMap ⊤).direction = Module.finrank Bool V

The image of an injective map from V that is affine over 𝔽₂ is an affine subspace whose direction has the dimension of V.