Products of Fredholm operators #
This file proves that the Cartesian product of two Fredholm operators is Fredholm and that its index is the sum of the two indices. This is elementary bookkeeping needed for the block decompositions and finite-dimensional reductions in the Fredholm substrate of the analytic Heegaard Floer roadmap.
The proof identifies the kernel and range of the product operator with the products of the
individual kernels and ranges, and counts the cokernel with Submodule.finrank_quotient_prod.
Main declarations #
ContinuousLinearMap.IsFredholm.prodMap: a product of Fredholm operators is Fredholm.ContinuousLinearMap.index_prodMap: the Fredholm index is additive under products.
theorem
ContinuousLinearMap.IsFredholm.prodMap
{K : Type u_1}
{E₁ : Type u_2}
{E₂ : Type u_3}
{F₁ : Type u_4}
{F₂ : Type u_5}
[NontriviallyNormedField K]
[NormedAddCommGroup E₁]
[NormedSpace K E₁]
[NormedAddCommGroup E₂]
[NormedSpace K E₂]
[NormedAddCommGroup F₁]
[NormedSpace K F₁]
[NormedAddCommGroup F₂]
[NormedSpace K F₂]
{T : E₁ →L[K] F₁}
{S : E₂ →L[K] F₂}
(hT : T.IsFredholm)
(hS : S.IsFredholm)
:
(T.prodMap S).IsFredholm
The Cartesian product of two Fredholm operators is Fredholm.
@[simp]
theorem
ContinuousLinearMap.index_prodMap
{K : Type u_1}
{E₁ : Type u_2}
{E₂ : Type u_3}
{F₁ : Type u_4}
{F₂ : Type u_5}
[NontriviallyNormedField K]
[NormedAddCommGroup E₁]
[NormedSpace K E₁]
[NormedAddCommGroup E₂]
[NormedSpace K E₂]
[NormedAddCommGroup F₁]
[NormedSpace K F₁]
[NormedAddCommGroup F₂]
[NormedSpace K F₂]
(T : E₁ →L[K] F₁)
(S : E₂ →L[K] F₂)
(hT : T.IsFredholm)
(hS : S.IsFredholm)
:
The Fredholm index is additive under Cartesian products of Fredholm operators.