isEmbedding_mapGL — Mathlib

English

If the algebra map A → B is an embedding, then the induced map mapGL B: SL_n(A) → GL_n(B) is an embedding.

Русский

Если алгебраическое отображение A → B является вложением, то индуцированное отображение mapGL B: SL_n(A) → GL_n(B) является вложением.

LaTeX

$$$IsEmbedding(mapGL B)$$$

Lean4

theorem isEmbedding_mapGL (h : Topology.IsEmbedding (algebraMap A B)) :
    Topology.IsEmbedding (mapGL B : SL n A → GL n B) :=
  haveI : FaithfulSMul A B := (faithfulSMul_iff_algebraMap_injective _ _).mpr h.2
  ⟨isInducing_mapGL h.isInducing, mapGL_injective⟩

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