lift_range_le — Mathlib

English

If a nonunital subalgebra s of A does not contain 1, then its unitization is isomorphic (as R-algebras) to the algebra generated by s, i.e., to Algebra.adjoin R (s).

Русский

Если неединичная подалгебра s содержат 1, то её единизацию можно изобразить как изоморфие по R-алгебрам к Algebra.adjoin R (s).

LaTeX

$$$\text{Unitization } R s \cong_{R} \operatorname{Algebra.adjoin} R (s)$, при $1\notin s$$$

Lean4

theorem lift_range_le {f : A →ₙₐ[R] C} {S : Subalgebra R C} :
    (lift f).range ≤ S ↔ NonUnitalAlgHom.range f ≤ S.toNonUnitalSubalgebra :=
  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⟩)

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