Explicitly Invoking Instance to Prove Basic Property

Stream: new members

[Gregory Wickham]

I want to prove

variable {A : Type*} [CStarAlgebra A]
variable (f : A →ₚ[ℂ] ℂ)
example (x : A) : f (star x) = conj (f x) := by sorry

And, because this is a basic property, I thought simp might have been able to handle it, but it doesn't.

The proof of the property is in Mathlib.Analysis.CStarAlgebra.PositiveLinearMap as

instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [OrderHomClass F A₁ A₂] :
    StarHomClass F A₁ A₂ where
  map_star f a := by

etc...

My full code with all imports and definitions of specific partial orders on the Complex numbers and on the CStarAlgebra is here:

import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
import Mathlib.Data.Complex.Basic
import Mathlib.Analysis.Complex.Order
import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

open ComplexConjugate
open scoped ComplexOrder
open scoped CStarAlgebra
scoped[ComplexOrder] attribute [instance] Complex.partialOrder
scoped[CStarAlgebra] attribute [instance] CStarAlgebra.spectralOrder

variable {A : Type*} [CStarAlgebra A]
variable (f : A →ₚ[ℂ] ℂ)
example (x : A) : f (star x) = conj (f x) := by sorry

How can I ensure lean can easily infer the fact that a positive linear functional is star-preserving?

[Aaron Liu]

How do we know that A is a star ordered ring

[Aaron Liu]

you probably need to make docs#CStarAlgebra.spectralOrderedRing a local instance

[Aaron Liu]

import Mathlib

open ComplexConjugate
open scoped ComplexOrder
open scoped CStarAlgebra
scoped[ComplexOrder] attribute [instance] Complex.partialOrder
scoped[CStarAlgebra] attribute [instance] CStarAlgebra.spectralOrder

variable {A : Type*} [CStarAlgebra A]
variable (f : A →ₚ[ℂ] ℂ)

example (x : A) : f (star x) = conj (f x) := by
  let := CStarAlgebra.spectralOrderedRing
  rw [map_star]
  simp

[Gregory Wickham]

Thank you! It seems that

example (x : A) : f (star x) = conj (f x) := by simp [map_star]

works. I guess lean could infer that f is an instance of StarHomClass