A projective-image terminal module lemma

This file isolates the unconditional linear-algebra step in a torsion presentation: a surjection from a product which kills its free factor factors through the first factor. It does not assert that a torsion module admits such a presentation.

theorem AlgebraicAnalysis.TorsionProjectiveImage.linearMap_product_factor_first {R : Type u_1} {P : Type u_2} {F : Type u_3} {T : Type u_4} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup F] [Module R F] [AddCommGroup T] [Module R T] (q : P × F →ₗ[R] T) (hkill : ∀ (z : F), q (0, z) = 0) : ∃ (q₁ : P →ₗ[R] T), q = q₁ ∘ₗ LinearMap.fst R P F

A linear map out of a product which vanishes on the second factor is already a map out of the first factor.

theorem AlgebraicAnalysis.TorsionProjectiveImage.surjective_factor_first_of_surjective {R : Type u_1} {P : Type u_2} {F : Type u_3} {T : Type u_4} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup F] [Module R F] [AddCommGroup T] [Module R T] (q : P × F →ₗ[R] T) (hkill : ∀ (z : F), q (0, z) = 0) (hq : Function.Surjective ⇑q) : ∃ (q₁ : P →ₗ[R] T), Function.Surjective ⇑q₁

Surjectivity also descends through the factorization in linearMap_product_factor_first.

theorem AlgebraicAnalysis.TorsionProjectiveImage.projective_leftIdeal_image_of_terminal_split {R : Type u_1} {P : Type u_2} {F : Type u_3} {T : Type u_4} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup F] [Module R F] [AddCommGroup T] [Module R T] (I : Submodule R R) [Module.Projective R ↥I] (e : P ≃ₗ[R] ↥I × F) (q : P →ₗ[R] T) (hq : Function.Surjective ⇑q) (hkill : ∀ (z : F), q (e.symm (0, z)) = 0) : ∃ (qI : ↥I →ₗ[R] T), Function.Surjective ⇑qI ∧ Module.Projective R ↥I

If a module P is identified with a projective left ideal times a free factor, and a quotient map kills that free factor, then the target is a homomorphic image of the projective left ideal. Here I : Submodule R R is a left ideal of the ring.