Direct sums of operators

TheoremComposition of direct sum operators is componentwise#✓fully proved

Composing direct sums is componentwise.

theorem prodMap_comp {E'' F'' : Type*}
    [NormedAddCommGroup E''] [NormedSpace 𝕜 E'']
    [NormedAddCommGroup F''] [NormedSpace 𝕜 F'']
    (T : E' →L[𝕜] E'') (S : F' →L[𝕜] F'') (T' : E →L[𝕜] E') (S' : F →L[𝕜] F') :
    (T.prodMap S) ∘L (T'.prodMap S') = (T ∘L T').prodMap (S ∘L S')

Used by 1

Used byInvertibility of a direct sum operator

TheoremDirect sum of identity operators is the identity#✓fully proved

The identity direct sum is the identity.

theorem prodMap_one : (1 : E →L[𝕜] E).prodMap (1 : F →L[𝕜] F) = 1

Used by 1

Used byInvertibility of a direct sum operator

TheoremDirect sum of zero operators is zero#✓fully proved

The zero direct sum is zero.

theorem prodMap_zero : (0 : E →L[𝕜] E').prodMap (0 : F →L[𝕜] F') = 0

TheoremScalar multiplication of a direct sum operator#✓fully proved

Scaling a direct sum scales both summands by the same factor.

theorem prodMap_smul (c : 𝕜) (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    (c • T).prodMap (c • S) = c • (T.prodMap S)

TheoremOperator norm of a direct sum is the maximum of the norms#✓fully proved

The operator norm of a direct sum is the maximum of the operator norms.

theorem norm_prodMap (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    ‖T.prodMap S‖ = max ‖T‖ ‖S‖

TheoremKernel of a direct sum operator#✓fully proved

The kernel of a direct sum is the product of the kernels.

theorem ker_prodMap (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    (T.prodMap S).ker = T.ker.prod S.ker

TheoremRange of a direct sum operator#✓fully proved

The range of a direct sum is the product of the ranges.

theorem range_prodMap (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    (T.prodMap S).range = T.range.prod S.range

TheoremInvertibility of a direct sum operator#✓fully proved

A direct sum is a unit iff both summands are units.

theorem isUnit_prodMap_iff (T : E →L[𝕜] E) (S : F →L[𝕜] F) :
    IsUnit (T.prodMap S) ↔ IsUnit T ∧ IsUnit S

Uses 2 · Used by 2

Proof usesComposition of direct sum operators is componentwise · Direct sum of identity operators is the identity

Used byResolvent set of a direct sum operator · Spectrum of a direct sum operator is the union of spectra

TheoremSpectrum of a direct sum operator is the union of spectra#✓fully proved

The spectrum of a direct sum is the union of the spectra.

theorem spectrum_prodMap (T : E →L[𝕜] E) (S : F →L[𝕜] F) :
    spectrum 𝕜 (T.prodMap S) = spectrum 𝕜 T ∪ spectrum 𝕜 S

Uses 1

Proof usesInvertibility of a direct sum operator

TheoremResolvent set of a direct sum operator#✓fully proved

The resolvent set of a direct sum is the intersection of the resolvent sets.

theorem resolventSet_prodMap (T : E →L[𝕜] E) (S : F →L[𝕜] F) :
    resolventSet 𝕜 (T.prodMap S) = resolventSet 𝕜 T ∩ resolventSet 𝕜 S

Uses 1

Proof usesInvertibility of a direct sum operator

TheoremCompactness of a direct sum operator#✓fully proved

A direct sum is compact iff both summands are compact.

theorem isCompactOperator_prodMap_iff (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    IsCompactOperator (T.prodMap S) ↔ IsCompactOperator T ∧ IsCompactOperator S

TheoremFredholmness of a direct sum operator#✓fully proved

A direct sum is Fredholm iff both summands are Fredholm.

theorem isFredholm_prodMap_iff [CompleteSpace 𝕜] (T : E →L[𝕜] E') (S : F →L[𝕜] F') :
    (T.prodMap S).IsFredholm ↔ T.IsFredholm ∧ S.IsFredholm

TheoremFredholm index of a direct sum is additive#✓fully proved

The Fredholm index of a direct sum is the sum of the Fredholm indices.

theorem index_prodMap [CompleteSpace 𝕜] (T : E →L[𝕜] E') (S : F →L[𝕜] F')
    (hT : T.IsFredholm) (hS : S.IsFredholm) :
    (T.prodMap S).index = T.index + S.index

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.