adjoin_range_eq_range_freeAlgebra_lift

English

For any f: X → A, the subalgebra of A generated by the range of f equals the range of the lift FreeAlgebra.lift R f.

Русский

Для любого отображения f: X → A подалгебра A, порождаемая образами f, равна образу отображения lift R f.

LaTeX

$$$ \\operatorname{Algebra.adjoin}_R (\\operatorname{Set.range} f) = (\\mathrm{FreeAlgebra.lift}\\, R\\, f).\\mathrm{range} $$$

Lean4

/-- Noncommutative version of `Algebra.adjoin_range_eq_range_aeval`. -/
theorem _root_.Algebra.adjoin_range_eq_range_freeAlgebra_lift (f : X → A) :
    Algebra.adjoin R (Set.range f) = (FreeAlgebra.lift R f).range := by
  simp only [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp, Function.comp_def, lift_ι_apply]

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