English
There is a presentation of the free module G →₀ A with generators indexed by G and no relations, obtained from the finsupp equivalence.
Русский
Существует презентация свободного модуля G →₀ A с генераторами, индексированными по G, без отношений, полученная из эквивалентности finsupp.
LaTeX
$$$\\text{presentationFinsupp}(G) : \\text{Presentation } A(G \\to_0 A)$$$
Lean4
/-- The presentation of the `A`-module `G →₀ A` with generators indexed by `G`,
and no relation. (Note that there is an auxiliary universe parameter `w₁` for the
empty type `R`.) -/
@[simps! G R var]
noncomputable def presentationFinsupp (G : Type w₀) : Presentation.{w₀, w₁} A (G →₀ A)
where
G := G
R := PEmpty.{w₁ + 1}
relation := by rintro ⟨⟩
toSolution := Relations.solutionFinsupp _
toIsPresentation := by exact Relations.solutionFinsupp_isPresentation _
