FaithfulRepresentation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Faithful representations are completely isometric

Injective star-algebra homomorphisms preserve C⋆-norms at each square matrix level. The isometric corner embedding then gives the same statement for every rectangular matrix size used in the perturbation estimates.

def OAI.KadisonKastler.starAlgHomToContinuousLinearMap line 24
Source documentation
A star homomorphism, viewed as a continuous linear map.
```
def starAlgHomToContinuousLinearMap (φ : A →⋆ₐ[ℂ] B) : A →L[ℂ] B :=
…
```
theorem OAI.KadisonKastler.starAlgHomToContinuousLinearMap_apply line 30
theorem OAI.KadisonKastler.injective_starAlgHom_norm line 34
Source documentation
The scalar isometry underlying a faithful representation.
```
theorem injective_starAlgHom_norm (φ : A →⋆ₐ[ℂ] B) (hφ : Function.Injective φ)
    (a : A) : ‖φ a‖ = ‖a‖ :=
…
```

theorem OAI.KadisonKastler.injective_starAlgHom_matrix line 42

Source documentation

Applying a faithful star homomorphism entrywise remains injective.

theorem injective_starAlgHom_matrix (φ : A →⋆ₐ[ℂ] B) (hφ : Function.Injective φ)
    {n : Type*} [Fintype n] :
    Function.Injective (CStarMatrix.mapₙₐ (n := n) φ.toNonUnitalStarAlgHom) := by
…

theorem OAI.KadisonKastler.injective_starAlgHom_matrix_norm line 50

Source documentation

Faithfulness preserves the norm of each square amplification.

theorem injective_starAlgHom_matrix_norm (φ : A →⋆ₐ[ℂ] B) (hφ : Function.Injective φ)
    {n : Type*} [Fintype n] (X : CStarMatrix n n A) :
    ‖CStarMatrix.mapₗ φ.toAlgHom.toLinearMap X‖ = ‖X‖ := by
…

theorem OAI.KadisonKastler.injective_starAlgHom_completelyIsometric line 57
Source documentation
Every faithful star representation preserves all rectangular matrix norms.
```
theorem injective_starAlgHom_completelyIsometric (φ : A →⋆ₐ[ℂ] B)
    (hφ : Function.Injective φ) : CompletelyIsometric φ.toAlgHom.toLinearMap := by
…
```
Mentions: OAI.KadisonKastler.CompletelyIsometric