Finite iteration of unimodular splittings

This file packages the unconditional finite iteration of normalized functionals. It does not assert that such a sequence can be constructed from rank or torsion hypotheses.

def AlgebraicAnalysis.FreeSummandInduction.emptyFactorEquiv {R : Type u_1} [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] : M ≃ₗ[R] M × (Fin 0 → R)

The harmless zero-factor equivalence used at the start of an iteration.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicAnalysis.FreeSummandInduction.emptyFactorEquiv_apply {R : Type u_1} [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] (m : M) : (emptyFactorEquiv M) m = (m, fun (i : Fin 0) => i.elim0)

theorem AlgebraicAnalysis.FreeSummandInduction.finite_unimodular_splitting {R : Type u_1} [Ring R] (M : ℕ → Type u_2) [(i : ℕ) → AddCommGroup (M i)] [(i : ℕ) → Module R (M i)] (φ : (i : ℕ) → M i →ₗ[R] R) (x : (i : ℕ) → M i) (hx : ∀ (i : ℕ), (φ i) (x i) = 1) (hres : (i : ℕ) → M (i + 1) ≃ₗ[R] ↥(φ i).ker) (n : ℕ) : Nonempty (M 0 ≃ₗ[R] M n × (Fin n → R))

If every stage in a finite sequence has a specified unimodular element, and the next module is identified with the preceding kernel, then all the specified free rank-one factors split off simultaneously.