Theorems · Definition · commutative algebra

Module.Presentation.cokernelRelations

{A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  {f : M₁ →ₗ[A] M₂} → {ι : Type w₁} → {g₁ : ι → M₁} → pres₂.CokernelData f g₁ → Module.Relations A

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₁.

Defined in

Mathlib.Algebra.Module.Presentation.Cokernel

Cited by

6 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms

Assumes

RingAddCommGroupModuleAddCommGroupModule