linearMapEquiv — Mathlib

English

The uniq construction provides a canonical linear equivalence between any two presented modules, written as LinearEquiv.ofLinear of_desc and of_desc solution.

Русский

Конструкция uniq задаёт каноническое линейное эквивалентное отображение между двумя презентациями модуля.

LaTeX

$$$$ h.uniq h' = \\mathrm{LinearEquiv.ofLinear}\\Big(h.desc\\, solution'\\Big)\\Big(h'.desc\\, solution\\Big) $$$$

Lean4

/-- If `M` admits a presentation by generators and relations, then
linear maps from `M` can be (naturally) identified to the solutions of
certain linear equations. -/
@[simps]
noncomputable def linearMapEquiv : (M →ₗ[A] N) ≃ relations.Solution N
    where
  toFun f := solution.postcomp f
  invFun s := h.desc s
  left_inv f := h.postcomp_injective (by simp)
  right_inv s := by simp

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