Matrix coordinates for a finite-rank direct summand

This file contains the coordinate-free-to-matrix step used by the general tangent-limit criterion. A complemented submodule of a finite coordinate module over a local ring is finite projective, hence finite free. Choosing a basis only inside the proof produces a column matrix and a retraction matrix. The matrices split, and their columns span exactly the original submodule.

structure AlgebraicAnalysis.SplitLatticePresentation.SplitMatrixPresentation {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (L : Submodule R (ι → R)) (r : ℕ) : Type (max u_1 u_2)

A matrix presentation constructed from a direct summand, with no chosen basis or retraction in the input.

• B : Matrix ι (Fin r) R

  Column matrix for the inclusion of the summand.

• C : Matrix (Fin r) ι R

  Retraction matrix for the chosen summand coordinates.

• leftInverse : self.C * self.B = 1
• columnsSpan : Submodule.span R (Set.range fun (j : Fin r) (i : ι) => self.B i j) = L

theorem AlgebraicAnalysis.SplitLatticePresentation.exists_splitMatrixPresentation {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} [Fintype ι] (L L' : Submodule R (ι → R)) (hcompl : IsCompl L L') (r : ℕ) (hrank : Module.finrank R ↥L = r) : Nonempty (SplitMatrixPresentation L r)

A finite-rank complemented submodule of a finite coordinate module over a local ring has split matrix coordinates. Finiteness descends along the projection onto the summand, projectivity comes from the split inclusion, and finite flat modules over local rings are free.

theorem AlgebraicAnalysis.SplitLatticePresentation.exists_splitMatrixPresentation_of_isComplemented {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} [Fintype ι] (L : Submodule R (ι → R)) (hcompl : IsComplemented L) (r : ℕ) (hrank : Module.finrank R ↥L = r) : Nonempty (SplitMatrixPresentation L r)

Property-valued form: no particular complement is part of the input.