isInducing_mapGL — Mathlib

English

If the algebra map A → B induces the topology, then the induced map mapGL B: SL_n(A) → GL_n(B) is inducing.

Русский

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

LaTeX

$$$IsInducing(mapGL B)$$$

Lean4

theorem isInducing_mapGL (h : Topology.IsInducing (algebraMap A B)) : Topology.IsInducing (mapGL B : SL n A → GL n B) :=
  by
  -- TODO: add `IsInducing.units_map` and deduce `IsInducing.generalLinearGroup_map`

  refine isInducing_toGL.comp ?_
  refine .of_comp ?_ continuous_induced_dom (h.matrix_map.comp (Topology.IsInducing.induced _))
  rw [continuous_induced_rng]
  exact continuous_subtype_val.matrix_map h.continuous

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