Theorems · Theorem · category theory

ModuleCat.shortComplexOfConj_shortExact

∀ {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'] (eM : M ≃ₗ[R] M')
  (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L') (exact : Function.Exact ⇑f ⇑g),
  Function.Injective ⇑f → Function.Surjective ⇑g → (ModuleCat.shortComplexOfConj eM eN eL f g ⋯).ShortExact

Defined in

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

Cited by

0 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModuleAddCommGroupModuleAddCommGroupAddCommGroupAddCommGroupModuleModuleModule