A linear complement identity

theorem MagnitudeConjecture.linearMap_sub_comp_apply_eq {R : Type u₁} {J : Type u₂} {B : Type u₃} {K : Type u₄} [Ring R] [AddCommGroup J] [Module R J] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] (g : J →ₗ[R] K) (i : B →ₗ[R] J) (p : J →ₗ[R] B) (h : g.ker = i.range) (z : J) : g ((LinearMap.id - i ∘ₗ p) z) = g z

Subtracting a component annihilated by a linear map does not change the image.

theorem MagnitudeConjecture.linearMap_projection_sub_comp_apply_eq_zero {R : Type u₁} {J : Type u₂} {B : Type u₃} [Ring R] [AddCommGroup J] [Module R J] [AddCommGroup B] [Module R B] (i : B →ₗ[R] J) (p : J →ₗ[R] B) (h : p ∘ₗ i = LinearMap.id) (z : J) : p ((LinearMap.id - i ∘ₗ p) z) = 0

The complementary projection id - i p has zero p-coordinate when p i = id.

theorem MagnitudeConjecture.linearMap_ker_le_ker_sub_comp {R : Type u₁} {J : Type u₂} {B : Type u₃} {K : Type u₄} [Ring R] [AddCommGroup J] [Module R J] [AddCommGroup B] [Module R B] [AddCommGroup K] [Module R K] (g : J →ₗ[R] K) (i : B →ₗ[R] J) (p : J →ₗ[R] B) (hker : g.ker = i.range) (hret : p ∘ₗ i = LinearMap.id) : g.ker ≤ (LinearMap.id - i ∘ₗ p).ker

If the kernel of g is the range of a split inclusion i, then the complementary projection id - i p kills the kernel of g.