Theorems · Definition · category theory

ModuleCat.shortComplexOfConj

{R : Type u} →
  [inst : Ring R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {N : Type v} →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                {L : Type v} →
                  [inst_5 : AddCommGroup L] →
                    [inst_6 : Module R L] →
                      {M' : Type u_1} →
                        {N' : Type u_2} →
                          {L' : Type u_3} →
                            [inst_7 : AddCommGroup M'] →
                              [inst_8 : AddCommGroup N'] →
                                [inst_9 : AddCommGroup L'] →
                                  [inst_10 : Module R M'] →
                                    [inst_11 : Module R N'] →
                                      [inst_12 : Module R L'] →
                                        (M ≃ₗ[R] M') →
                                          (N ≃ₗ[R] N') →
                                            (L ≃ₗ[R] L') →
                                              (f : M' →ₗ[R] N') →
                                                (g : N' →ₗ[R] L') →
                                                  g ∘ₗ f = 0 → CategoryTheory.ShortComplex (ModuleCat R)

Suppose that f and g are linear maps that compose to zero, and that eM, eN, and eL indicated in the diagram below are linear equivalences to modules that all belong to the same universe. Then this is the short complex in ModuleCat given by the bottom row in the diagram. M --f--> N --g--> L | | | eM eN eL | | | v v v M' --> N' --> L' This complex is exact when we have Function.Exact f g, see ModuleCat.shortComplexOfConj_exact.

Defined in

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Cited by

2 results in Mathlib

Foundations

Depth 51 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupAddCommGroupAddCommGroupModuleModuleModule