RankOneFactorCriterion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Rank-one tests for scalarity. A countable dense family suffices, including on a variable projection range. These are the tests used to prove that the central-decomposition fibers are factors.

theorem OAI.KadisonSimilarity.scalar_of_commutes_rankOne line 16

Source documentation

Commuting with all rank-one operators forces an operator to be scalar.

theorem scalar_of_commutes_rankOne (T : H →L[ℂ] H)
    (hT : ∀ v w : H, T * InnerProductSpace.rankOne ℂ v w =
      InnerProductSpace.rankOne ℂ v w * T) :
    ∃ c : ℂ, T = c • (1 : H →L[ℂ] H) := by
…

theorem OAI.KadisonSimilarity.scalar_of_commutes_dense_rankOne line 40

Source documentation

It suffices to test rank-one operators on a dense family of vectors.

theorem scalar_of_commutes_dense_rankOne {ι : Type*} (d : ι → H)
    (hd : DenseRange d) (T : H →L[ℂ] H)
    (hT : ∀ i j, T * InnerProductSpace.rankOne ℂ (d i) (d j) =
      InnerProductSpace.rankOne ℂ (d i) (d j) * T) :
    ∃ c : ℂ, T = c • (1 : H →L[ℂ] H) := by
…

theorem OAI.KadisonSimilarity.projectionFiber_denseRange line 58

Source documentation

Projecting a dense family gives a dense family in the actual range.

theorem projectionFiber_denseRange {ι : Type*} (d : ι → H) (hd : DenseRange d)
    (p : H →L[ℂ] H) (hp : IsStarProjection p) :
    DenseRange (fun i => projectionFiberRetraction p hp (d i)) := by
…

Mentions: OAI.KadisonSimilarity.projectionFiberRetraction

theorem OAI.KadisonSimilarity.scalar_of_commutes_projection_rankOne line 70

Source documentation

Countably many compressed rank-one commutation identities suffice for scalarity on the projection fiber.

theorem scalar_of_commutes_projection_rankOne {ι : Type*} (d : ι → H)
    (hd : DenseRange d) (p : H →L[ℂ] H) (hp : IsStarProjection p)
    (T : projectionFiber p hp →L[ℂ] projectionFiber p hp)
    (hT : ∀ i j,
      T * InnerProductSpace.rankOne ℂ
        (projectionFiberRetraction p hp (d i)) (projectionFiberRetraction p hp (d j)) =
      InnerProductSpace.rankOne ℂ
        (projectionFiberRetraction p hp (d i)) (projectionFiberRetraction p hp (d j)) * T) :
    ∃ c : ℂ, T = c • (1 : projectionFiber p hp →L[ℂ] projectionFiber p hp) :=
…

Mentions: OAI.KadisonSimilarity.projectionFiber, OAI.KadisonSimilarity.projectionFiberRetraction