starLift_range_le — Mathlib

English

Using the integer-scalar closure, the same range equality holds with Subring closure.

Русский

С использованием целочисленного замыкания выполняется то же равенство образа.

LaTeX

$$$\mathrm{range}(\mathrm{unitization}(s)) = \mathrm{subalgebraOfSubring}(\mathrm{Subring.closure}(s))$$$

Lean4

theorem starLift_range_le {f : A →⋆ₙₐ[R] C} {S : StarSubalgebra R C} :
    (starLift f).range ≤ S ↔ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rintro - ⟨x, rfl⟩
    exact @h (f x) ⟨x, by simp⟩
  · rintro - ⟨x, rfl⟩
    induction x with
    | _ r a => simpa using add_mem (algebraMap_mem S r) (h ⟨a, rfl⟩)

Похожие утверждения