isRepresentationCore — Mathlib

English

If each index i provides a presentation of the i-th relation, then the direct sum with those per-index presentations presents the direct-sum module. That is, the direct sum of presentations is again a presentation.

Русский

Если для каждого индекса i дана презентация i-й отношения, то прямая сумма с этими локальными презентациями образует презентацию самой прямой суммы модуля.

LaTeX

$$$(\\text{Solution.IsPresentationCore})\\; (\\text{directSum solution}).IsPresentation$$$

Lean4

/-- The direct sum admits a presentation by generators and relations. -/
noncomputable def isRepresentationCore : Solution.IsPresentationCore.{w'} (directSum solution)
    where
  desc s := DirectSum.toModule _ _ _ (fun i ↦ (h i).desc (directSumEquiv s i))
  postcomp_desc s := by ext ⟨i, g⟩; simp
  postcomp_injective
    h' := by
    ext i : 1
    apply (h i).postcomp_injective
    ext g
    exact Solution.congr_var h' ⟨i, g⟩

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