Theorems · Theorem · commutative algebra

ModuleCat.span_exact

∀ {ι : Type u_1} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.Exact →
    ∀ {v : ι → ↑S.X₁} {β : Type u_4} {u : ι ⊕ β → ↑S.X₂},
      u ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom S.f) ∘ v →
        ⊤ ≤ Submodule.span R (Set.range v) →
          ⊤ ≤ Submodule.span R (Set.range (⇑(CategoryTheory.ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)) →
            ⊤ ≤ Submodule.span R (Set.range u)

In the commutative diagram `` f g 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 v spans X₁ and w spans X₃, then u spans X₂`.

Defined in

Mathlib.Algebra.Category.ModuleCat.Free

Cited by

1 results in Mathlib

Foundations

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

Assumes

Ring