coe_codRestrict — Mathlib

English

The underlying algebra homomorphism of the codRestrict construction is the same as restricting the underlying algebra homomorphism to p.

Русский

Базовая алгебра-гомоморфизм-конструкция codRestrict совпадает с ограничением исходного гомоморфизма на подполью p.

LaTeX

$$$\text{toAlgHom}(f\ codRestrict p h) = (\text{toAlgHom } f)\ codRestrict p h$$$

Lean4

@[norm_cast]
theorem coe_codRestrict (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) :
    (f.codRestrict p h : A →ₐ[R] p) = (f : A →ₐ[R] B).codRestrict p h :=
  rfl

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