ModuleCat.linearIndependent_leftExact
theorem 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 (⇑S.g ∘ u ∘ Sum.inr) →
CategoryTheory.Mono S.f → u ∘ Sum.inl = ⇑S.f ∘ v → LinearIndependent R u
This theorem, `ModuleCat.linearIndependent_leftExact`, asserts that in a specific commutative diagram involving a sequence of modules and certain maps, if certain conditions hold, then a function `u` is linearly independent.
It can be described as such: Given two types `ι` and `ι'` and a ring `R`, and given a ShortComplex `S` in the category of `R`-modules, if this ShortComplex is exact, meaning that it's an exact sequence of modules, and we have a mapping function `v` from `ι` to `S.X₁` that is linearly independent over `R`. If we have another mapping function `u` from the sum of `ι` and `ι'` to `S.X₂` such that the composition of `S.g`, `u` and `Sum.inr` is linearly independent over `R`, and if `S.f` is a monomorphism (injective), and the composition of `u` and `Sum.inl` is equal to the composition of `S.f` and `v`, then `u` is linearly independent over `R`.
In simpler terms, this theorem shows a certain condition under which a function in a diagram involving modules is linearly independent.
More concisely: If `S` is an exact sequence of `R`-modules, `v` is a linearly independent mapping from `ι` to `S.X₁`, `u` maps `ι ⊕ ι'` to `S.X₂`, `S.f` is a monomorphism, and `u ∘ Sum.inl = S.f ∘ v`, then `u` is linearly independent over `R`.
|
ModuleCat.span_exact
theorem 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 = ⇑S.f ∘ v →
⊤ ≤ Submodule.span R (Set.range v) →
⊤ ≤ Submodule.span R (Set.range (⇑S.g ∘ u ∘ Sum.inr)) → ⊤ ≤ Submodule.span R (Set.range u)
In the context of modules over a ring, consider a commutative diagram where the top row is an exact sequence of modules and the maps on the bottom are formed by the `Sum.inl` and `Sum.inr` operations. The theorem states that if v spans the module `X₁` and w spans the module `X₃`, then u must span the module `X₂`. More formally, given a ring `R` and a short complex of modules `S` that is exact, and given mappings `v : ι → ↑S.X₁`, `u : ι ⊕ β → ↑S.X₂` such that `u` composed with `Sum.inl` equals `S.f` composed with `v`, if the span of the range of `v` equals the whole module `X₁` and the span of the range of `S.g` composed with `u` composed with `Sum.inr` equals the whole module `X₃`, then the span of the range of `u` equals the whole module `X₂`.
More concisely: Given a commutative diagram of exact modules over a ring where the top row maps are given by `Sum.inl`, if the ranges of given mappings `v` from `ι` to `X₁` and `u` from `ι ⊕ β` to `X₂` satisfy `u ∘ Sum.inr ∘ S.g = id_{X₃}` and the spans of `v` and `u` equal `X₁` and `X₃`, respectively, then `u` spans `X₂`.
|
ModuleCat.free_shortExact
theorem ModuleCat.free_shortExact :
∀ {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
S.ShortExact → ∀ [inst_1 : Module.Free R ↑S.X₁] [inst_2 : Module.Free R ↑S.X₃], Module.Free R ↑S.X₂
This theorem states that in a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` in the category of modules over a ring `R`, if the modules `X₁` and `X₃` are free, then the module `X₂` is also free. A short exact sequence is a sequence of morphisms between modules such that the image of each morphism is the kernel of the next, and being free is a property of a module meaning that it has a basis, i.e., it is isomorphic to a direct sum of copies of the underlying ring.
More concisely: In the category of modules over a ring, if a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` has free modules `X₁` and `X₃`, then `X₂` is also free.
|
ModuleCat.linearIndependent_shortExact
theorem 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 (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w))
The theorem named `ModuleCat.linearIndependent_shortExact` states the following: Given a short exact sequence of `R`-modules, denoted as `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, and two families of vectors `v : ι → N` and `w : ι' → P` that are linearly independent over `R`, we can construct a new family `ι ⊕ ι' → M` which is also linearly independent over `R`. This new family is created by combining the function `v` composed with the morphism from `X₁` to `X₂` and the function `w` composed with the inverse of the morphism from `X₂` to `X₃`.
More concisely: Given a short exact sequence of R-modules and two linearly independent families of vectors, there exists a linearly independent family obtained by combining their compositions with the morphisms between the modules.
|
ModuleCat.span_rightExact
theorem ModuleCat.span_rightExact :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
S.Exact →
∀ {v : ι → ↑S.X₁} {w : ι' → ↑S.X₃},
⊤ ≤ Submodule.span R (Set.range v) →
⊤ ≤ Submodule.span R (Set.range w) →
CategoryTheory.Epi S.g →
⊤ ≤ Submodule.span R (Set.range (Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w)))
This theorem states that given an exact sequence of R-modules `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` and two families `v : ι → X₁` and `w : ι' → X₃` that span the modules `X₁` and `X₃` respectively, we can construct a family `ι ⊕ ι' → X₂` that spans the module `X₂`. The function `Sum.elim (⇑S.f ∘ v) (Function.invFun S.g.toFun ∘ w)` is used to construct the spanning family for `X₂` from the spanning families of `X₁` and `X₃`. Additionally, it's required that `S.g` is an epimorphism.
More concisely: Given an exact sequence of R-modules `X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, and families `v : ι → X₁` and `w : ι' → X₃` spanning `X₁` and `X₃` respectively, there exists a family `ι ⊕ ι' → X₂` spanning `X₂`, constructed using `Sum.elim` from `v` and `w`, with `S.g : X₁ ⟶ X₃` an epimorphism.
|