Rank additivity for split sequences

Packet 2 cannot currently assert that noncommutative Ore localization is flat: the pinned Mathlib has no such theorem. This file therefore proves the exact additivity statements that require only an explicit linear equivalence after localization. In particular, whenever a localized short exact sequence is known to split, its localized middle term is equivalent to a product and the rank is additive. No flatness or exactness interface is postulated here.

theorem AlgebraicAnalysis.RankExact.rank_prod_add {Q : Type u} [DivisionRing Q] {V W : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup W] [Module Q W] : Module.rank Q (V × W) = Module.rank Q V + Module.rank Q W

theorem AlgebraicAnalysis.RankExact.rank_add_of_linearEquiv_prod {Q : Type u} [DivisionRing Q] {V W : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup W] [Module Q W] {U : Type v} [AddCommGroup U] [Module Q U] (e : U ≃ₗ[Q] V × W) : Module.rank Q U = Module.rank Q V + Module.rank Q W

theorem AlgebraicAnalysis.RankExact.rank_add_of_split_exact {Q : Type u} [DivisionRing Q] {V W : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup W] [Module Q W] {U : Type v} [AddCommGroup U] [Module Q U] (i : V →ₗ[Q] U) (p : U →ₗ[Q] W) (r : U →ₗ[Q] V) (s : W →ₗ[Q] U) (hri : r ∘ₗ i = LinearMap.id) (hps : p ∘ₗ s = LinearMap.id) (hpi : p ∘ₗ i = 0) (hrs : r ∘ₗ s = 0) (hdecomp : i ∘ₗ r + s ∘ₗ p = LinearMap.id) : Module.rank Q U = Module.rank Q V + Module.rank Q W

theorem AlgebraicAnalysis.RankExact.finrank_prod_add {Q : Type u} [DivisionRing Q] {V W : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup W] [Module Q W] [Module.Finite Q V] [Module.Finite Q W] : Module.finrank Q (V × W) = Module.finrank Q V + Module.finrank Q W

theorem AlgebraicAnalysis.RankExact.finrank_add_of_linearEquiv_prod {Q : Type u} [DivisionRing Q] {V W : Type v} [AddCommGroup V] [Module Q V] [AddCommGroup W] [Module Q W] {U : Type v} [AddCommGroup U] [Module Q U] [Module.Finite Q V] [Module.Finite Q W] (e : U ≃ₗ[Q] V × W) : Module.finrank Q U = Module.finrank Q V + Module.finrank Q W

theorem AlgebraicAnalysis.RankExact.oreRank_add_of_localized_prod_equiv {R : Type u} [Ring R] [Nontrivial R] [NoZeroDivisors R] [OreLocalization.OreSet (nonZeroDivisors Rᵐᵒᵖ)] {M N P : Type v} [AddCommGroup M] [Module Rᵐᵒᵖ M] [AddCommGroup N] [Module Rᵐᵒᵖ N] [AddCommGroup P] [Module Rᵐᵒᵖ P] (e : RankTorsion.LocalizedRightModule R M ≃ₗ[RankTorsion.FractionRingOp R] RankTorsion.LocalizedRightModule R N × RankTorsion.LocalizedRightModule R P) : RankTorsion.oreRank M = RankTorsion.oreRank N + RankTorsion.oreRank P