Commit 2024-01-08 19:30 1f780d69

feat: generalize FiniteDimensional.finrank_mul_finrank (#9046) Generalize the conditions of the tower law FiniteDimensional.finrank_mul_finrank' in FieldTheory/Tower from [CommRing F] [Algebra F K] to [Ring F] [Module F K], and remove the [Module.Finite F K] and [Module.Finite K A] conditions. The generalized version applies to situations when we have a tower C/B/A where the A-module structure on C is induced from the B-module structure via a RingHom from A to B, and the A-module structure on B is induced by the same RingHom. In particular, it applies when the A-module structure on B and the B-module structure on C come from two RingHoms, and the A-module structure on C comes from the composition of them, regardless of whether A and B are commutative or not. As prerequisites, I also generalized lemmas originally introduced by @kckennylau in [mathlib3#3355](https://github.com/leanprover-community/mathlib/pull/3355/files) to prove the tower law. They were split into three PRs:

• LinearAlgebra/Span #9380: add span_eq_closure and closure_induction which say that Submodule.span R s is generated by R • s as an AddSubmonoid. I feel that the existing span_induction should be replaced by closure_induction as the latter is stronger, and allow us to remove the commutativity condition in span_smul_of_span_eq_top in Algebra/Tower.
• Algebra/Tower #9382: switching from CommSemiring/Algebra to Semiring/Module here requires proving the curious lemma IsScalarTower.isLinearMap which states that for a tower of modules A/S/R, any S-linear map from S to A is also R-linear. If the map is injective, we can deduce that S/S/R also form a tower. (By ringHomEquivModuleIsScalarTower in #9381, there is therefore a canonical RingHom from R to S.)
• Lemmas for free modules over rings including finrank_mul_finrank' are moved from FieldTheory/Tower to LinearAlgebra/Dimension/Free Zulip