A linear map vanishing on $\ker f \cap \ker g$ factors as $u \circ f + v \circ g$

Proved

QLLL.LinearMap.exists_comp_add_comp

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebraquantum-lll

Let $\mathbb{K}$ be a field and let $V, M, N, H$ be vector spaces over $\mathbb{K}$ . Let $f : V \to M$ , $g : V \to N$ and $h : V \to H$ be linear maps with

\ker f \cap \ker g \ \subseteq\ \ker h.

Then there are linear maps $u : M \to H$ and $v : N \to H$ such that

h \ =\ u \circ f + v \circ g.

This factorization lemma is the key step in identifying the intersection of two tensor products of subspaces, QLLL.TensorProduct.range_mapIncl_eq_inf and QLLL.TensorProduct.range_mapIncl_inf_range_mapIncl.

Formalization Note No finite-dimensionality is assumed; the field hypothesis is essential. On the platform the name carries a QLLL. prefix so that it cannot clash with Mathlib if an equivalent lemma is added there later.

Preamble

import Mathlib

open TensorProduct LinearMap Function
variable {K V W : Type*} [Field K]
  [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
open _root_.LinearMap
variable {M N H : Type*}
  [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N]
  [AddCommGroup H] [Module K H]

Formal statement

theorem QLLL.LinearMap.exists_comp_add_comp (f : V →ₗ[K] M) (g : V →ₗ[K] N) (h : V →ₗ[K] H)
    (hker : ker f ⊓ ker g ≤ ker h) :
    ∃ (u : M →ₗ[K] H) (v : N →ₗ[K] H), h = u ∘ₗ f + v ∘ₗ g := by sorry

Source

Not in the paper; general linear algebra supporting the tensor-product computation of Lemma 11. Formalization companion to Ambainis, Kempe and Sattath, A Quantum Lovász Local Lemma, arXiv:0911.1696; see the blueprint https://sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint/

View graph

A linear map vanishing on ker⁡f∩ker⁡g\ker f \cap \ker gkerf∩kerg factors as u∘f+v∘gu \circ f + v \circ gu∘f+v∘g

A linear map vanishing on $\ker f \cap \ker g$ factors as $u \circ f + v \circ g$