SemisimpleKernelProjection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The canonical fixed-space projection preserves invariant filtrations

For a semisimple operator, its kernel and range are complementary. The projection to the kernel preserves every invariant subspace, including the lower central series when the operator is A - 1.

theorem OAI.PolycyclicRecognition.semisimple_kernel_range_isCompl line 20
theorem OAI.PolycyclicRecognition.semisimple_sub_one line 54
def OAI.PolycyclicRecognition.semisimpleKernelProjection line 59
theorem OAI.PolycyclicRecognition.semisimpleKernelProjection_mem line 62
theorem OAI.PolycyclicRecognition.semisimpleKernelProjection_preserves line 66
theorem OAI.PolycyclicRecognition.semisimpleKernelProjection_commute line 86
theorem OAI.PolycyclicRecognition.semisimple_add_kernelProjection_bijective line 111
theorem OAI.PolycyclicRecognition.semisimple_sub_projection_mem_of_apply_mem line 135
Source documentation
A vector whose image lies in an invariant subspace differs from its fixed component by a vector in that subspace.
```
theorem semisimple_sub_projection_mem_of_apply_mem
    (B : Module.End ℝ L) (hB : B.IsSemisimple)
    (U : Submodule ℝ L) (hU : ∀ x ∈ U, B x ∈ U) {x : L} (hx : B x ∈ U) :
    x - semisimpleKernelProjection B hB x ∈ U := by
…
```
Mentions: OAI.PolycyclicRecognition.semisimpleKernelProjection