Personally I'm inclined to use the following as the definition:

/-- Two submodules K and L in an algebra S over R are linearly disjoint if the map
  `K ⊗[R] L →ₗ[R] S` induced by multiplication in S is injective. -/
def Submodule.LinearDisjoint (R S) [CommSemiring R] [Semiring S] [Algebra R S]
    (K L : Submodule R S) : Prop :=
  Injective (TensorProduct.lift <| ((LinearMap.domRestrict' L).comp <| .mul R S).domRestrict K)

and we should be able to show

1. it implies that every R-linearly independent set in L is K-linearly independent (your definition), if K is a subalgebra (Edit: K needs to be flat over R). If L/R is free (and the semirings are rings), it's equivalent to it, because the existence of a basis of L/R that is K-linearly independent implies injectivity.
2. it implies that every R-linearly independent set in K is (MulOpposite L)-linearly independent, if L is a subalgebra (flat over R). If K/R is free, it's equivalent to it.
3. it implies that the product of every R-linear independent set in K with one in L is R-linear independent (requires K or L flat over R (?)), if both K/R and L/R are free, it's equivalent to it.

Note that in general K ⊗[R] L →ₗ[R] S isn't an AlgHom, unless every element of K commutes with every element of L. Bourbaki's definition has this additional commutativity requirement. In general the image is the pointwise product KL, which may be a proper submodule of the subalgebra generated by K and L. Even when K and L are both subalgebras the image is exactly K ⊔ L, the multiplication may not agree: consider ℝ + ℝi and ℝ + ℝj in the quaternions.

I don't know if there are benefits of doing things in this generality; I just think it's better to find out most general statements we can prove. Maybe @AntoineChambert-Loir has thoughts?

I don't know if there are benefits of doing things in this generality; I just think it's better to find out most general statements we can prove. Maybe @AntoineChambert-Loir has thoughts?

I don't have a clear idea. When the target algebra is not commutative, it does not seem obvious that the IsLinearlyDisjoint is symmetric. But maybe it is anyway, I don't know. And maybe it's not so important.

I doubt that. In the proof I use mul_comm several times.

Maybe the right place for this file in mathlib's hierarchy is in Algebra.Algebra, or RingTheory (like Algebra.TensorProduct).

it implies that every R-linearly independent set in L is K-linearly independent (your definition), if K is a subalgebra.

I think that this requires K/R being flat, no?

[EDIT] Yes, it requires flatness, at least for the items 1 and 2. Otherwise there is a counterexample: let R=Z, S=Z×Fp×Fp×Fp, let K be the submodule generated by (1,1,1,1) and (0,1,1,0), S be the submodule generated by (1,1,1,1) and (0,0,1,1), then they are both subalgebras, not flat over R, isomorphic to Z⊕Fp as R-modules, and they are linearly disjoint if using tensor product definition. On the other hand, (p,0,0,0) is contained in their intersections, which is R-linearly independent, but not K-linearly independent nor L-linearly independent.

I don't know if there is counterexample for item 3. I can prove it if assuming one of K,L is flat over R.

The proof is quite simple without explicit computations (hopefully also in Lean):

Yes, it requires flatness, at least for the items 1 and 2. Otherwise there is a counterexample: let R=Z, S=Z×Fp×Fp×Fp, let K be the submodule generated by (1,1,1,1) and (0,1,1,0), S be the submodule generated by (1,1,1,1) and (0,0,1,1), then they are both subalgebras, not flat over R, isomorphic to Z⊕Fp as R-modules, and they are linearly disjoint if using tensor product definition. On the other hand, (p,0,0,0) is contained in their intersections, which is R-linearly independent, but not K-linearly independent nor L-linearly independent.

You're right! Thanks for the counterexample and sorry for my mistake. So either we assume flatness or we require R to be a field; both would be fine with me.

Personally I'm inclined to use the following as the definition:

/-- Two submodules K and L in an algebra S over R are linearly disjoint if the map
  `K ⊗[R] L →ₗ[R] S` induced by multiplication in S is injective. -/
def Submodule.LinearDisjoint (R S) [CommSemiring R] [Semiring S] [Algebra R S]
    (K L : Submodule R S) : Prop :=
  Injective (TensorProduct.lift <| ((LinearMap.domRestrict' L).comp <| .mul R S).domRestrict K)

I think it's better to give the map TensorProduct.lift <| ((LinearMap.domRestrict' L).comp <| .mul R S).domRestrict K a name, and we can prove some basic properties on it. What about Submodule.mulMap?

This PR/issue depends on:

• [Merged by Bors] - feat(LinearAlgebra/LinearDisjoint): definition and properties of linearly disjoint of submodules #12434
• [Merged by Bors] - feat(Mathlib/LinearAlgebra/DirectSum/Finsupp): tensor products of finsupp sums #11635
• [Merged by Bors] - feat(LinearAlgebra/DirectSum/Finsupp): add some more variants of finsuppTensorFinsupp #11598
• [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Basic): add LinearEquiv.(l|r)Tensor #11731
• [Merged by Bors] - feat(RingTheory/Flat/Basic): add lTensor_preserves_injective_linearMap #11748
• [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Finiteness): add some finiteness results of tensor product #11859
• [Merged by Bors] - feat(RingTheory/LinearDisjoint): properties of linearly disjoint of subalgebras (2) #15346
• [Merged by Bors] - feat: add Subalgebra.finite_(bot|sup) #12025
• [Merged by Bors] - feat: left-Noetherian rings and commutative rings satisfy OrzechProperty #13425
• [Merged by Bors] - feat: Generalize corollaries of rank-nullity theorem. #9626
• [Merged by Bors] - feat: add definition of opposite of subsemirings, subrings, and subalgebras #12846
• [Merged by Bors] - feat(Algebra/Algebra/Subalgebra/Rank): add some results on the ranks of subalgebras #12847
• [Merged by Bors] - feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot #12849
• [Merged by Bors] - feat: some results on dimension of field adjoin #18515
  By Dependent Issues (🤖). Happy coding!

All comments are addressed except for the remaining one.

Thanks 🎉
maintainer merge

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

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build