subtype_comp_codRestrict — Mathlib

English

Restriction of the codomain of a StarAlgHom to a subalgebra containing its range gives a new StarAlgHom.

Русский

Ограничение кодомодуля StarAlgHom до подалгебры, содержащей его образ, образует новый StarAlgHom.

LaTeX

$$$ f : A \\to_⋆ B \\;\\Rightarrow\\; f \\downarrow_S : A \\to⋆_ R S $$$

Lean4

@[simp]
theorem subtype_comp_codRestrict (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) (hf : ∀ x : A, f x ∈ S) :
    S.subtype.comp (f.codRestrict S hf) = f :=
  StarAlgHom.ext <| coe_codRestrict _ S hf

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