lift_comp — Mathlib

English

The lift built from g composes with mkLinearMap to recover g: lift(S,g,h) ∘ mkLinearMap = g.

Русский

Подъем, построенный из g, композит с mkLinearMap даёт обратно g: lift(S,g,h) ∘ mkLinearMap = g.

LaTeX

$$$(\\mathrm{lift}\\, S\\, g\\, h) \\circ (\\mathrm{mkLinearMap}\\, S\\, M) = g$$$

Lean4

/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `lift g ∘ mkLinearMap = g`.
-/
theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
    (lift S g h).comp (mkLinearMap S M) = g := by
  ext x
  simp [LocalizedModule.lift_mk]

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