Documentation

TauCeti.Analysis.Fredholm.Adjoint

Adjoints of Fredholm operators #

This file proves the closed-range theorem for adjoints on Hilbert spaces and applies it to Fredholm operators. If a continuous linear map has closed range, then its adjoint has range equal to the orthogonal complement of the original kernel. Consequently, taking adjoints preserves Fredholm operators and negates their index.

The proof restricts an operator with closed range to a continuous linear equivalence from the orthogonal complement of its kernel onto its range. The adjoint of this equivalence is surjective, which removes the closure from Mathlib's general identity T.orthogonal_ker : T.kerแ—ฎ = Tโ€ .range.topologicalClosure.

Main declarations #

The argument and index convention follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1.

source
noncomputable def ContinuousLinearMap.orthogonalKerEquivRange {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) :
โ†ฅ(โ†‘T).kerแ—ฎ โ‰ƒL[๐•œ] โ†ฅ(โ†‘T).range

The restriction of a closed-range operator to the orthogonal complement of its kernel is a continuous linear equivalence onto its range.

Equations
Instances For
    source
    @[simp]
    theorem ContinuousLinearMap.orthogonalKerEquivRange_apply {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (x : โ†ฅ(โ†‘T).kerแ—ฎ) :
    โ†‘((T.orthogonalKerEquivRange hT) x) = T โ†‘x

    The closed-range restriction equivalence acts by the original operator.

    source
    @[simp]
    theorem ContinuousLinearMap.orthogonalKerEquivRange_symm_apply {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (y : โ†ฅ(โ†‘T).range) :
    T โ†‘((T.orthogonalKerEquivRange hT).symm y) = โ†‘y

    Applying a closed-range operator to the inverse of its orthogonal-kernel restriction recovers the given range element.

    source
    theorem ContinuousLinearMap.range_adjoint_eq_orthogonal_ker_of_isClosed_range {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) :
    (โ†‘(adjoint T)).range = (โ†‘T).kerแ—ฎ

    A continuous linear map with closed range has adjoint range equal to the orthogonal complement of its kernel.

    source
    theorem ContinuousLinearMap.isClosed_range_adjoint_of_isClosed_range {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) :
    IsClosed โ†‘(โ†‘(adjoint T)).range

    If a continuous linear map between Hilbert spaces has closed range, then so does its adjoint.

    source
    @[simp]
    theorem ContinuousLinearMap.isClosed_range_adjoint_iff {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) :
    IsClosed โ†‘(โ†‘(adjoint T)).range โ†” IsClosed โ†‘(โ†‘T).range

    A continuous linear map between Hilbert spaces has closed range if and only if its adjoint does.

    source
    noncomputable def ContinuousLinearMap.cokerEquivKerAdjoint {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) :
    (F โงธ (โ†‘T).range) โ‰ƒL[๐•œ] โ†ฅ(โ†‘(adjoint T)).ker

    The cokernel of a closed-range operator is continuously linearly equivalent to the kernel of its adjoint.

    Equations
    Instances For
      source
      @[simp]
      theorem ContinuousLinearMap.coe_cokerEquivKerAdjoint_apply_mk {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (y : F) :
      โ†‘((T.cokerEquivKerAdjoint hT) (Submodule.Quotient.mk y)) = โ†‘((โ†‘T).rangeแ—ฎ.orthogonalProjectionOnto y)

      On quotient representatives, the cokernel--adjoint-kernel equivalence is orthogonal projection onto the orthogonal complement of the range.

      source
      @[simp]
      theorem ContinuousLinearMap.cokerEquivKerAdjoint_symm_apply {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (y : โ†ฅ(โ†‘(adjoint T)).ker) :
      (T.cokerEquivKerAdjoint hT).symm y = Submodule.Quotient.mk โ†‘y

      The inverse cokernel--adjoint-kernel equivalence sends a kernel vector to its quotient class.

      source
      noncomputable def ContinuousLinearMap.cokerAdjointEquivKer {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) :
      (E โงธ (โ†‘(adjoint T)).range) โ‰ƒL[๐•œ] โ†ฅ(โ†‘T).ker

      The cokernel of the adjoint of a closed-range operator is continuously linearly equivalent to the original kernel.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem ContinuousLinearMap.coe_cokerAdjointEquivKer_apply_mk {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (x : E) :
        โ†‘((T.cokerAdjointEquivKer hT) (Submodule.Quotient.mk x)) = โ†‘((โ†‘(adjoint T)).rangeแ—ฎ.orthogonalProjectionOnto x)

        On quotient representatives, the adjoint-cokernel--kernel equivalence is orthogonal projection onto the orthogonal complement of the adjoint range.

        source
        @[simp]
        theorem ContinuousLinearMap.cokerAdjointEquivKer_symm_apply {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : IsClosed โ†‘(โ†‘T).range) (x : โ†ฅ(โ†‘T).ker) :
        (T.cokerAdjointEquivKer hT).symm x = Submodule.Quotient.mk โ†‘x

        The inverse adjoint-cokernel--kernel equivalence sends a kernel vector to its quotient class.

        source
        theorem ContinuousLinearMap.IsFredholm.adjoint {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] {T : E โ†’L[๐•œ] F} (hT : T.IsFredholm) :
        (ContinuousLinearMap.adjoint T).IsFredholm

        The adjoint of a Fredholm operator between Hilbert spaces is Fredholm.

        source
        @[simp]
        theorem TauCeti.isFredholm_adjoint_iff {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) :
        (ContinuousLinearMap.adjoint T).IsFredholm โ†” T.IsFredholm

        A continuous linear map between Hilbert spaces is Fredholm if and only if its adjoint is Fredholm.

        source
        @[simp]
        theorem ContinuousLinearMap.index_adjoint {๐•œ : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike ๐•œ] [NormedAddCommGroup E] [InnerProductSpace ๐•œ E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace ๐•œ F] [CompleteSpace F] (T : E โ†’L[๐•œ] F) (hT : T.IsFredholm) :
        (adjoint T).index = -T.index

        Taking the adjoint of a Fredholm operator negates its index.