QuotientUnitBall.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Closed star-homomorphism ranges and contractive lifts

The closed-range assertion uses the actual C-star quotient by the kernel. Clipping a preimage then gives an exact contraction lift, including at the boundary of the closed unit ball. No faithfulness assumption is needed.

def OAI.KadisonKastler.starHomClosedKernel line 25
def OAI.KadisonKastler.starHomKernelQuotient line 39
theorem OAI.KadisonKastler.starHomKernelQuotient_injective line 47
theorem OAI.KadisonKastler.starHomKernelQuotient_apply line 51
theorem OAI.KadisonKastler.isClosed_starAlgHom_range line 55
Source documentation
The image of a homomorphism of complete C-star algebras is norm closed.
```
theorem isClosed_starAlgHom_range (φ : A →⋆ₐ[ℂ] B) : IsClosed (Set.range φ) := by
…
```

theorem OAI.KadisonKastler.exists_contractive_starAlgHom_preimage line 69

Source documentation

Every contraction in a star-homomorphism range has a contraction preimage.

theorem exists_contractive_starAlgHom_preimage (φ : A →⋆ₐ[ℂ] B)
    {y : B} (hy : y ∈ Set.range φ) (hn : ‖y‖ ≤ 1) :
    ∃ x : A, ‖x‖ ≤ 1 ∧ φ x = y := by
…

theorem OAI.KadisonKastler.image_unitBall_starAlgHom line 80
Source documentation
Exact image equality for closed unit balls; in particular no radius enlargement is lost on restriction to a reducing subspace.
```
theorem image_unitBall_starAlgHom (φ : A →⋆ₐ[ℂ] B) :
    φ '' {x : A | ‖x‖ ≤ 1} = {y : B | y ∈ Set.range φ ∧ ‖y‖ ≤ 1} := by
…
```
theorem OAI.KadisonKastler.isClosed_image_unitBall_starAlgHom line 90