inclusion — Mathlib

English

For any S ≤ T, the inclusion map S → T is a nonunital star subalgebra homomorphism.

Русский

Для любых S ≤ T вложение S в T является негунитарным звездным подпалгебро-гомоморфизмом.

LaTeX

$$$\\text{inclusion}_h: S \\hookrightarrow T \\quad \\text{is a nonunital star subalgebra homomorphism}$$$

Lean4

/-- The map `S → T` when `S` is a non-unital star subalgebra contained in the non-unital star
algebra `T`.

This is the non-unital star subalgebra version of `Submodule.inclusion`, or
`NonUnitalSubalgebra.inclusion` -/
def inclusion {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) : S →⋆ₙₐ[R] T
    where
  toNonUnitalAlgHom := NonUnitalSubalgebra.inclusion h
  map_star' _ := rfl

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