subalgebraMap — Mathlib

English

An isomorphism of algebras e induces an isomorphism between a subalgebra S of A and its image S.map e in B.

Русский

Изоморфизм алгебр e индуцирует изоморфизм между подалгеброй S ⊆ A и её образом S.map e в B.

LaTeX

$$$S \mapsto S.map (e: A \to_{R} B)$ defines an isomorphism $S \cong_R S.map (e)$$$

Lean4

/-- Given an equivalence `e : A ≃ₐ[R] B` of `R`-algebras and a subalgebra `S` of `A`,
`subalgebraMap` is the induced equivalence between `S` and `S.map e` -/
@[simps!]
def subalgebraMap (e : A ≃ₐ[R] B) (S : Subalgebra R A) : S ≃ₐ[R] S.map (e : A →ₐ[R] B) :=
  { e.toRingEquiv.subsemiringMap S.toSubsemiring with commutes' := fun r => by ext; exact e.commutes r }

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