Version 1 source-bound exposition export. Original text SHA-256: 2f6cca4a5381109326012a1fa5e3b8329d73a9406986558fbfb1c939eadb7725. Link targets are adapted for this edition; the registered Card identity is unchanged.

# The Hilbert space of a minimal-ideal compact model

## Statement

Let $A$ be a complex C*-algebra with compatible order, and let $\pi:A\to\mathcal B(H)$ be a faithful representation with every value compact, on a complete complex Hilbert space. For a minimal nonzero closed $\ast$-ideal $i$ of $A$, this abbreviation names the chosen cyclic Hilbert subspace $H_i\subseteq H$.

## Definition

The [minimal-ideal model construction](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=146&end=158#L146) chooses a pair $(p,x)\in A\times H$ with the following properties: $p$ is a minimal projection, the closed ideal generated by $p$ is the displayed ideal $i$, $x\ne0$, $\pi(p)x=x$, and the same cyclic restriction $\sigma_{p,x}:I_p\to\mathcal B(H_i)$ is an [exact compact-operator model](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/CompactModel.lean.html?from=compact-model-space&start=29&end=33#L29): it is injective, every value is compact, and every compact operator on this same $H_i$ is $\sigma_{p,x}(a)$ for some $a\in I_p$. Faithfulness and compact-valuedness alone do not include the last condition. These properties are guaranteed for the chosen pair; they are not additional assumptions.

Write $I_p$ for the closed ideal generated by $p$. The [chosen model subspace](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=162&end=166#L162) is
$$
H_i=\overline{\{\pi(a)x:a\in I_p\}}\ \subseteq H
$$
for that same pair $(p,x)$, with its inherited norm and complex inner product. The [closedness and Hilbert-space results](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=175&end=178#L175) ensure that $H_i$ is complete and nonzero.

## Assumptions

The algebra carries a partial order and compatible order. The input ideal is minimal among nonzero closed $\ast$-ideals. The representation $\pi$ is injective and every value $\pi(a)$ is compact. There is no additional choice of Hilbert structure, no countability assumption and no global nonzero-algebra hypothesis.

## Conclusion

The resulting space depends on the ideal and the chosen representation $\pi$. The [compact-model isomorphism](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=271&end=279#L271) uses this same Hilbert space; different ideals need not give the same space.

## Main citations

- [Exact complete definition](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=170&end=172#L170).
- [MinimalClosedStarIdeal: the indexing type](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/OrthogonalElementary.lean.html?from=compact-model-space&start=101&end=102#L101).
- [compactModelWitness: one generator/vector pair and its full specification](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=146&end=158#L146).
- [IsCompactOperatorModel: the three conditions on one action](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/CompactModel.lean.html?from=compact-model-space&start=29&end=33#L29).
- [compactModelSubspace: the exact cyclic subspace](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=162&end=166#L162).
- [isClosed_compactModelSubspace and the completeness/nontriviality instances](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Analysis/CStarAlgebra/Ideal/MinimalIdealFamilyModel.lean.html?from=compact-model-space&start=175&end=178#L175).

## Lean source signature (exact)

The following is the complete defining right-hand side, copied from the fixed source.

```lean
abbrev CompactModelSpace (i : MinimalClosedStarIdeal A)
    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) : Type v :=
  i.compactModelSubspace pi hpi
```

| In the source | Mathematical meaning |
|---|---|
| `i : MinimalClosedStarIdeal A` | A minimal nonzero closed $\ast$-ideal. |
| `pi` and `hpi` | The fixed representation and its faithful compact-valued condition, used to choose the projection and cyclic vector. |
| `: Type v` | The resulting space $H_i$ is a subspace of the given Hilbert space $H$. |
| `i.compactModelSubspace pi hpi` | The closed cyclic subspace associated with the chosen pair $(p,x)$, with norm and inner product inherited from $H$. |

### Source context (separate exact excerpt)

Source lines 128–129:

```lean
variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
```

Source lines 140–140:

```lean
namespace MinimalClosedStarIdeal
```