[Merged by Bors] - feat(LinearAlgebra/LinearDisjoint): definition and properties of linearly disjoint of submodules

[acmepjz]

This is part 1 of #9651.

We adapt the definitions in https://en.wikipedia.org/wiki/Linearly_disjoint.
Let R be a commutative ring, S be an R-algebra (not necessarily commutative).
Two R-submodules M and N in S are linearly disjoint,
if the natural R-linear map M ⊗[R] N →ₗ[R] S (Submodule.mulMap M N)
induced by the multiplication in S is injective.

The following is the first equivalent characterization of linearly disjointness:

• Submodule.LinearDisjoint.linearIndependent_left_of_flat:
  if M and N are linearly disjoint, if N is a flat R-module, then for any family of
  R-linearly independent elements { m_i } of M, they are also N-linearly independent,
  in the sense that the R-linear map from ι →₀ N to S which maps { n_i }
  to the sum of m_i * n_i (Submodule.mulLeftMap N m) is injective.

• Submodule.LinearDisjoint.of_basis_left:
  conversely, if { m_i } is an R-basis of M, which is also N-linearly independent,
  then M and N are linearly disjoint.

Dually, we have:

• Submodule.LinearDisjoint.linearIndependent_right_of_flat:
  if M and N are linearly disjoint, if M is a flat R-module, then for any family of
  R-linearly independent elements { n_i } of N, they are also M-linearly independent,
  in the sense that the R-linear map from ι →₀ M to S which maps { m_i }
  to the sum of m_i * n_i (Submodule.mulRightMap M n) is injective.

• Submodule.LinearDisjoint.of_basis_right:
  conversely, if { n_i } is an R-basis of N, which is also M-linearly independent,
  then M and N are linearly disjoint.

The following is the second equivalent characterization of linearly disjointness:

• Submodule.LinearDisjoint.linearIndependent_mul_of_flat:
  if M and N are linearly disjoint, if one of M and N is flat, then for any family of
  R-linearly independent elements { m_i } of M, and any family of
  R-linearly independent elements { n_j } of N, the family { m_i * n_j } in S is
  also R-linearly independent.

• Submodule.LinearDisjoint.of_basis_mul:
  conversely, if { m_i } is an R-basis of M, if { n_i } is an R-basis of N,
  such that the family { m_i * n_j } in S is R-linearly independent,
  then M and N are linearly disjoint.

Other results:

• Submodule.LinearDisjoint.symm_of_commute, Submodule.linearDisjoint_symm_of_commute:
  linearly disjoint is symmetric under some commutative conditions.

• Submodule.linearDisjoint_op:
  linearly disjoint is preserved by taking multiplicative opposite.

• Submodule.LinearDisjoint.of_le_left_of_flat, Submodule.LinearDisjoint.of_le_right_of_flat,
  Submodule.LinearDisjoint.of_le_of_flat_left, Submodule.LinearDisjoint.of_le_of_flat_right:
  linearly disjoint is preserved by taking submodules under some flatness conditions.

• Submodule.LinearDisjoint.of_linearDisjoint_fg_left,
  Submodule.LinearDisjoint.of_linearDisjoint_fg_right,
  Submodule.LinearDisjoint.of_linearDisjoint_fg:
  conversely, if any finitely generated submodules of M and N are linearly disjoint,
  then M and N themselves are linearly disjoint.

• Submodule.LinearDisjoint.bot_left, Submodule.LinearDisjoint.bot_right:
  the zero module is linearly disjoint with any other submodules.

• Submodule.LinearDisjoint.one_left, Submodule.LinearDisjoint.one_right:
  the image of R in S is linearly disjoint with any other submodules.

• Submodule.LinearDisjoint.of_left_le_one_of_flat,
  Submodule.LinearDisjoint.of_right_le_one_of_flat:
  if a submodule is contained in the image of R in S, then it is linearly disjoint with
  any other submodules, under some flatness conditions.

• Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat,
  Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat:
  if M and N are linearly disjoint, if one of M and N is flat, then any two commutative
  elements contained in the intersection of M and N are not R-linearly independent (namely,
  their span is not R ^ 2). In particular, if any two elements in the intersection of M and N
  are commutative, then the rank of the intersection of M and N is at most one.

• Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self:
  if M and itself are linearly disjoint, if M is flat, if any two elements in M
  are commutative, then the rank of M is at most one.

The results with name containing "of_commute" also have corresponding specified versions
assuming S is commutative.

---

discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Linearly.20disjoint

• depends on: [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Submodule): add some linear maps induced by multiplication for submodules #12498

[erdOne]

I've reviewed up to end mulMap (L297). I think everything until that point can go into a new file Mathlib.LinearAlgebra.TensorProduct.Submodule. And it will probably be merged sooner if it is split into a separate PR.

[acmepjz]

I've reviewed up to end mulMap (L297). I think everything until that point can go into a new file Mathlib.LinearAlgebra.TensorProduct.Submodule. And it will probably be merged sooner if it is split into a separate PR.

Added as #12498. Maybe some proof in this PR can be golfed since I added mulLeftMap_eq_mulRightMap_of_commute etc. in that PR.

[erdOne]

LGTM. Some small nitpicks on naming.

[erdOne]

What I was referring to before were the lemmas with hypothesis Module.Flat R M ∨ Module.Flat R N. Are they useful downstream?

[acmepjz]

It is not essential; there are some corollaries of it, stated using Module.Flat R M ∨ Module.Flat R N; it's always possible to rewrite the proof for splitting cases left and right.

But personally I think it's convenient if we have a ored version, just like IntermediateField.sup_toSubalgebra_of_isAlgebraic (sorry that is also contributed by me).

[erdOne]

Thanks!
maintainer merge
btw a diff of +600 is quite big for a PR and it makes this PR harder to review. Next time please try to split it up. (IMO +250 is max for a PR, and maybe +400 if it only touches one file, and this is probably on the high end among the consensus of all reviewers)

[erdOne]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[riccardobrasca]

Thanks a lot for this contribution! I see a lot of simp_rw, is there a particular reason?

bors d+

[riccardobrasca]

Why protected?

[acmepjz]

Because later we will have Subalgebra.LinearDisjoint, IntermediateField.LinearDisjoint and Field.LinearDisjoint.

[mathlib-bors]

✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[acmepjz]

I see a lot of simp_rw, is there a particular reason?

I forgot. Probably because rw and simp only don't work for items inside something.

[riccardobrasca]

I see a lot of simp_rw, is there a particular reason?

I forgot. Probably because rw and simp only don't work for items inside something.

OK, no problem.

[acmepjz]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style