English
For a unital C*-subalgebra S of A and a ∈ S, a is invertible in A iff a is invertible in S.
Русский
Для унитарной подалгебры S в A и элемента a ∈ S, a обратим в A тогда и только тогда, когда обратим в S.
LaTeX
$$$$\text{IsUnit}(a) \text{ in } A \iff \text{IsUnit}(a) \text{ in } S.$$$$
Lean4
/-- For a unital C⋆-subalgebra `S` of `A` and `x : S`, if `↑x : A` is invertible in `A`, then
`x` is invertible in `S`. -/
theorem coe_isUnit {a : S} : IsUnit (a : A) ↔ IsUnit a :=
by
refine ⟨fun ha ↦ ?_, IsUnit.map S.subtype⟩
have ha₁ := ha.star.mul ha
have ha₂ := ha.mul ha.star
have spec_eq {x : S} (hx : IsSelfAdjoint x) : spectrum ℂ x = spectrum ℂ (x : A) :=
Subalgebra.spectrum_eq_of_isPreconnected_compl S _ <| (hx.map S.subtype).isConnected_spectrum_compl.isPreconnected
rw [← StarMemClass.coe_star, ← MulMemClass.coe_mul, ← spectrum.zero_notMem_iff ℂ, ← spec_eq,
spectrum.zero_notMem_iff] at ha₁ ha₂
· have h₁ : ha₁.unit⁻¹ * star a * a = 1 := mul_assoc _ _ a ▸ ha₁.val_inv_mul
have h₂ : a * (star a * ha₂.unit⁻¹) = 1 := (mul_assoc a _ _).symm ▸ ha₂.mul_val_inv
exact ⟨⟨a, ha₁.unit⁻¹ * star a, left_inv_eq_right_inv h₁ h₂ ▸ h₂, h₁⟩, rfl⟩
· exact IsSelfAdjoint.mul_star_self a
· exact IsSelfAdjoint.star_mul_self a
