toAlgebra — Mathlib

English

A Subalgebra S can be endowed with a canonical Algebra structure over R, using the inclusion of S into A.

Русский

Подалгебра S естественным образом наделяется структурой алгебра над R через включение S в A.

LaTeX

$$$S \text{ is given an } \mathsf{Alg}_R S \text{ structure}$ by inclusion into A$$

Lean4

instance (priority := 75) toAlgebra : Algebra R s
    where
  algebraMap :=
    { toFun r := ⟨algebraMap R A r, algebraMap_mem s r⟩
      map_one' := Subtype.ext <| by simp
      map_mul' _ _ := Subtype.ext <| by simp
      map_zero' := Subtype.ext <| by simp
      map_add' _ _ := Subtype.ext <| by simp }
  commutes' r x := Subtype.ext <| Algebra.commutes r (x : A)
  smul_def' r x := Subtype.ext <| (algebraMap_smul A r (x : A)).symm

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