The preimage ideal of the compact operators

Lean source signature (exact)

The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.

/-- The inverse image of the compact operators under a star representation,
as an algebraic two-sided ideal. -/
def compactPreimageIdeal [NonUnitalCStarAlgebra A]
    (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : TwoSidedIdeal A :=
  TwoSidedIdeal.mk' {a | rho a ∈ compactOperator (RingHom.id ℂ) H H}
    (by
      change rho 0 ∈ compactOperator (RingHom.id ℂ) H H
      rw [map_zero]
      exact Submodule.zero_mem _)
    (fun {x y} hx hy => by
      change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx
      change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy
      change rho (x + y) ∈ compactOperator (RingHom.id ℂ) H H
      rw [map_add]
      exact Submodule.add_mem _ hx hy)
    (fun {x} hx => by
      change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx
      change rho (-x) ∈ compactOperator (RingHom.id ℂ) H H
      rw [map_neg]
      exact Submodule.neg_mem _ hx)
    (fun {x y} hy => by
      change rho y ∈ compactOperator (RingHom.id ℂ) H H at hy
      change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H
      rw [map_mul]
      have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by
        change IsCompactOperator ⇑((rho x).comp (rho y))
        exact hy.clm_comp (rho x)
      exact hxy)
    (fun {x y} hx => by
      change rho x ∈ compactOperator (RingHom.id ℂ) H H at hx
      change rho (x * y) ∈ compactOperator (RingHom.id ℂ) H H
      rw [map_mul]
      have hxy : (rho x).comp (rho y) ∈ compactOperator (RingHom.id ℂ) H H := by
        change IsCompactOperator ⇑((rho x).comp (rho y))
        exact hx.comp_clm (rho y)
      exact hxy)