adjoin_range_ι — Mathlib

English

The subalgebra generated by the image of M under ι_R is the whole tensor algebra; i.e., the range of ι_R generates TensorAlgebra R M as an algebra.

Русский

Подалгебра, порождаемая образом M через ι_R, равна всей TensorAlgebra R M; диапазон ι_R порождает алгебру.

LaTeX

$$$\\operatorname{adjoin}_R\\bigl(\\mathrm{Set.range}(\\iota_R\\ (M))\\bigr) = \\top$$$

Lean4

@[simp]
theorem adjoin_range_ι : Algebra.adjoin R (Set.range (ι R (M := M))) = ⊤ :=
  by
  refine top_unique fun x hx => ?_; clear hx
  induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)

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