range_lift — Mathlib

English

The lift of f to a Clifford algebra homomorphism has image equal to the algebra generated by the range of f.

Русский

Образ подъема отображения совпадает с алгебра-, порождаемой образом диапазона f.

LaTeX

$$$(\\mathrm{lift}\\ Q ⟨f, cond⟩).\\mathrm{range} = \\mathrm{Algebra.adjoin}_R (\\mathrm{Set.range}(f))$$$

Lean4

@[simp]
theorem range_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
    (lift Q ⟨f, cond⟩).range = Algebra.adjoin R (Set.range f) := by
  simp_rw [← Algebra.map_top, ← adjoin_range_ι, AlgHom.map_adjoin, ← Set.range_comp, Function.comp_def, lift_ι_apply]

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