OAI/Analysis/KadisonKastler/TomiyamaDenseProjections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.closed_projection_span_eq_top_of_surjective line 16

   Source documentation

   A surjective star homomorphism preserves norm-density of projection spans.

   theorem closed_projection_span_eq_top_of_surjective
       (φ : A →⋆ₐ[ℂ] B) (hφ : Function.Surjective φ)
       (hdense : (Submodule.span ℂ {e : A | IsStarProjection e}).topologicalClosure = ⊤) :
       (Submodule.span ℂ {e : B | IsStarProjection e}).topologicalClosure = ⊤ := by
   …

2. theorem OAI.KadisonKastler.tomiyama_map_mul_of_dense_projections line 38

   Source documentation

   The algebraic projection identities extend to a target whose projections have norm-dense linear span.

   theorem tomiyama_map_mul_of_dense_projections
       (hdense : (Submodule.span ℂ {e : B | IsStarProjection e}).topologicalClosure = ⊤)
       (φ : B →⋆ₐ[ℂ] A) (P : A →L[ℂ] B)
       (hP : ∀ x, ‖P x‖ ≤ ‖x‖) (hfix : ∀ b, P (φ b) = b) :
       (∀ b x, P (φ b * x) = b * P x) ∧ (∀ x b, P (x * φ b) = P x * b) := by
   …