ι_range_map_lift — Mathlib

English

The range of the composed map from ι_Q through lift equals the range of the original linear map f; i.e., lifting preserves the generated subspace structure of M inside Clifford(Q).

Русский

Образ композиции ι_Q затем подъем равен образу f; подъем сохраняет порождаемое подпространство M внутри Clifford(Q).

LaTeX

$$$(\\mathrm{range}(\\iota_Q)).map(\\mathrm{lift}\\ Q ⟨f, cond⟩).toLinearMap = \\mathrm{range}(f)$$$

Lean4

@[simp]
theorem ι_range_map_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
    (LinearMap.range (ι Q)).map (lift Q ⟨f, cond⟩).toLinearMap = LinearMap.range f := by
  rw [← LinearMap.range_comp, ι_comp_lift]

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