Compact operators as an ideal family

The compact operators, gauged by the operator norm, form a symmetric operator ideal family: the smallest interesting one, sitting inside TauCeti.operatorNormFamily with the same gauge but a proper carrier.

Everything the ideal laws need is in Mathlib already — IsCompactOperator.add, .smul, .comp_clm, .clm_comp, isCompactOperator_zero and isClosed_setOfPred_isCompactOperator — except adjoint-invariance, which is Schauder's theorem; that is TauCeti.ContinuousLinearMap.isCompactOperator_adjoint, whose own docstring records that it was written to unblock exactly this family.

The gauge is ∞ off the ideal

OperatorIdealFamily carries an ℝ≥0∞-valued gauge that is ∞ exactly off the carrier, so the compact family's gauge is the operator norm on compact operators and ∞ elsewhere. Two of the four laws then need a case split that the operator-norm family does not:

• gauge_smul at c = 0, where the left side is gauge 0 = 0 and the right is 0 * ∞ = 0 — the ℝ≥0∞ convention is what makes this come out right;
• gauge_comp_le when A is not compact, where the bound is vacuous unless L or R is zero, and then L ∘L A ∘L R is zero and so compact.

Main definitions

• TauCeti.compactOperatorIdealFamily
• TauCeti.compactOperatorFamily: its symmetric (adjoint-invariant) refinement.
• TauCeti.instIsCompleteCompactOperatorIdealFamily: the ideal is complete, because the compact operators are closed for the operator norm and the gauge is the operator norm on them.

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: authored directly in ForTauCeti; it has had no prior home.
• Extraction class: authored in place for the Tau Ceti staging layer.
• Original authors / copyright: Jon Crall, Claude Opus 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

noncomputable def TauCeti.compactOperatorIdealFamily (𝕜 : Type u) [RCLike 𝕜] : OperatorIdealFamily 𝕜

The compact operators, gauged by the operator norm, as an operator ideal family. The gauge is ∞ off the compact operators, which is how OperatorIdealFamily records the carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.gauge_compactOperatorIdealFamily {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) : (compactOperatorIdealFamily 𝕜).gauge A = if IsCompactOperator ⇑A then ‖A‖ₑ else ⊤

The compact family's gauge, unfolded.

theorem TauCeti.mem_carrier_compactOperatorIdealFamily {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {A : E →L[𝕜] F} : A ∈ (compactOperatorIdealFamily 𝕜).carrier ↔ IsCompactOperator ⇑A

Membership in the compact ideal is compactness.

theorem TauCeti.gauge_compactOperatorIdealFamily_of_isCompactOperator {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {A : E →L[𝕜] F} (hA : IsCompactOperator ⇑A) : (compactOperatorIdealFamily 𝕜).gauge A = ‖A‖ₑ

On the ideal, the gauge is the operator norm; the compact family differs from operatorNormIdealFamily only in its carrier.

noncomputable def TauCeti.compactOperatorIdealFamilyElemEquiv {𝕜 : Type u} [RCLike 𝕜] {E : Type v} {F : Type w} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] : (compactOperatorIdealFamily 𝕜).Elem E F ≃ₗᵢ[𝕜] ↥(compactOperator (RingHom.id 𝕜) E F)

The ideal of the compact family, as a normed space, is isometric to Mathlib's submodule of compact operators. This is what carries completeness across: the gauge is the operator norm on members, so the two norms agree.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.instIsCompleteCompactOperatorIdealFamily {𝕜 : Type u} [RCLike 𝕜] : (compactOperatorIdealFamily 𝕜).IsComplete

The compact ideal is complete. The compact operators are closed for the operator norm, and on them the ideal norm is the operator norm, so the ideal inherits completeness from the ambient operator space.

noncomputable def TauCeti.compactOperatorFamily (𝕜 : Type u) [RCLike 𝕜] : SymmetricOperatorIdealFamily 𝕜

The compact operators as a symmetric ideal family.

Adjoint-invariance of the carrier is Schauder's theorem (ContinuousLinearMap.isCompactOperator_adjoint_iff); adjoint-invariance of the gauge is then the isometry of the adjoint, exactly as for the operator-norm family.

Equations

• TauCeti.compactOperatorFamily 𝕜 = { toOperatorIdealFamily := TauCeti.compactOperatorIdealFamily 𝕜, gauge_adjoint := ⋯ }

instance TauCeti.instIsCompleteCompactOperatorFamily {𝕜 : Type u} [RCLike 𝕜] : (compactOperatorFamily 𝕜).IsComplete

Completeness transfers to the symmetric view, which shares its underlying family. Restated rather than inherited for the reason recorded on operatorNormFamily: the base instance is at three independent universes and the symmetric family constrains the last two to be equal.

theorem TauCeti.gauge_compactOperatorFamily_of_isCompactOperator {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {A : E →L[𝕜] F} (hA : IsCompactOperator ⇑A) : (compactOperatorFamily 𝕜).gauge A = ‖A‖ₑ

The symmetric compact family has the same gauge as the plain one.

theorem TauCeti.mem_carrier_compactOperatorFamily {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {A : E →L[𝕜] F} : A ∈ (compactOperatorFamily 𝕜).carrier ↔ IsCompactOperator ⇑A

Membership in the symmetric compact family is compactness.