ι_comp_lift — Mathlib

English

The lift of the pair (f, cond) composed with the canonical embedding ι_Q is equal to f; i.e., the lift agrees with f on the image of M.

Русский

Подъем пары (f, cond) после вложения ι_Q совпадает с f на образе M.

LaTeX

$$$(\\mathrm{lift}\\ Q \\langle f, cond \\rangle).toLinearMap \\circ (\\iota_Q) = f$.$$

Lean4

@[simp]
theorem ι_comp_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = algebraMap _ _ (Q m)) :
    (lift Q ⟨f, cond⟩).toLinearMap.comp (ι Q) = f :=
  Subtype.mk_eq_mk.mp <| (lift Q).symm_apply_apply ⟨f, cond⟩

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