cokernelRelations — Mathlib

English

There is an obvious solution to the cokernel equations in the cokernel of f, living on M₂ modulo the range of f.

Русский

Существуют очевидные решения уравнений коконеленной системы в коконеленной фактор-модуля M₂ / range(f).

LaTeX

$$$pres_2.\\text{cokernelSolution}: (pres_2.\\text{cokernelRelations data}).\\text{Solution} (M_2 / \\mathrm{range}(f))$$$

Lean4

/-- The shape of the presentation by generators and relations of the cokernel
of `f : M₁ →ₗ[A] M₂`. It consists of a generator for each generator of `M₂`, and
there are two types of relations: one for each relation in the presentation in `M₂`,
and one for each generator of `M₁`. -/
@[simps]
def cokernelRelations : Relations A where
  G := pres₂.G
  R := Sum pres₂.R ι
  relation
    | .inl r => pres₂.relation r
    | .inr i => data.lift i

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