Theorems · Theorem · commutative algebra

ModuleCat.linearIndependent_leftExact

∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁},
      LinearIndependent R v →
        ∀ {u : ι ⊕ ι' → ↑S.X₂},
          LinearIndependent R (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr) →
            CategoryTheory.Mono S.f →
              u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v → LinearIndependent R u

In the commutative diagram `` f g 0 --→ X₁ --→ X₂ --→ X₃ ↑ ↑ ↑ v| u| w| ι → ι ⊕ ι' ← ι' ` where the top row is an exact sequence of modules and the maps on the bottom are Sum.inl and Sum.inr. If u is injective and v and w are linearly independent, then u` is linearly independent.

Defined in

Mathlib.Algebra.Category.ModuleCat.Free

Cited by

2 results in Mathlib

Foundations

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

Assumes

Ring