Theorems · Theorem · commutative algebra

ModuleCat.linearIndependent_shortExact

∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact →
    ∀ {v : ι → ↑S.X₁},
      LinearIndependent R v →
        ∀ {w : ι' → ↑S.X₃},
          LinearIndependent R w →
            LinearIndependent R
              (Sum.elim (⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v)
                (Function.invFun (ModuleCat.Hom.hom S.g).toFun ∘ w))

Given a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of R-modules and linearly independent families v : ι → N and w : ι' → P, we get a linearly independent family ι ⊕ ι' → M

Defined in

Mathlib.Algebra.Category.ModuleCat.Free

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring