isPresentationCore — Mathlib

English

If a solution is a presentation, then the module is free.

Русский

Если решение является презентацией, то модуль свободен.

LaTeX

$$$Solution.IsPresentation \\Rightarrow Module.Free\\, A\\, M$$$

Lean4

/-- If `relations : Relations A` involves no relations (`[IsEmpty relations.R]`),
then the free module `relations.G →₀ A` satisfies the universal property of the
corresponding module defined by generators (and relations). -/
noncomputable def isPresentationCore : Solution.IsPresentationCore.{w} relations.solutionFinsupp
    where
  desc s := Finsupp.linearCombination _ s.var
  postcomp_desc := by aesop
  postcomp_injective h := by ext; apply Solution.congr_var h

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