SpectralArcTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Faithful-coordinate transport of the spectral arc. Only the actual generated subalgebra must have a von Neumann range.

theorem OAI.KadisonSimilarity.starAlgHom_unit_zpow line 14

theorem OAI.KadisonSimilarity.dihedralSpectralArcInput_of_injective line 20

Source documentation

An arc in a faithful represented subalgebra is an arc in the source, with exactly the same trace moments.

theorem dihedralSpectralArcInput_of_injective
    (τA : A →ₗ[ℂ] ℂ) (τB : B →ₗ[ℂ] ℂ) (ρ : A →⋆ₐ[ℂ] B)
    (hρ : Function.Injective ρ) (hτ : ∀ a, τB (ρ a) = τA a)
    (C : StarSubalgebra ℂ A) (w d : Aˣ)
    (hinput : DihedralSpectralArcInput τB (C.map ρ)
      (Units.map ρ.toAlgHom.toMonoidHom w) (Units.map ρ.toAlgHom.toMonoidHom d)) :
    DihedralSpectralArcInput τA C w d := by
…

Mentions: OAI.KadisonSimilarity.DihedralSpectralArcInput