English
The endomorphism space with the adjoint operation forms a Star-Ordered Ring, i.e., an ordered ring compatible with the star operation.
Русский
Пространство линейных отображений с сопряжением образует звездообразное упорядоченное кольцо, сохраняющее порядок под операцией звезды.
LaTeX
$$StarOrderedRing End(H) for complex 𝕜$$
Lean4
/-- Because this takes `ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint` as an argument,
and for the moment we only have this for `𝕜 := ℂ`, this is not registered as an instance. -/
theorem instStarOrderedRingRCLike [ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint] :
StarOrderedRing (H →L[𝕜] H) where
le_iff f
g := by
constructor
· intro h
rw [le_def] at h
obtain ⟨p, hp₁, -, hp₃⟩ := CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.spectrumRestricts
refine ⟨p ^ 2, ?_, by symm; rwa [add_comm, ← eq_sub_iff_add_eq]⟩
exact AddSubmonoid.subset_closure ⟨p, by simp only [hp₁.star_eq, sq]⟩
· rintro ⟨p, hp, rfl⟩
rw [le_def, add_sub_cancel_left]
induction hp using AddSubmonoid.closure_induction with
| mem _ hf =>
obtain ⟨f, rfl⟩ := hf
simpa using ContinuousLinearMap.IsPositive.adjoint_conj isPositive_one f
| zero => exact isPositive_zero
| add f g _ _ hf hg => exact hf.add hg
