feat: definition and basic properties of linearly disjoint

[acmepjz]

---

• [ ] depends on: #12434 [part one: submodule version]
  • [x] depends on: #11635
  • [x] depends on: #11598 [need finsuppTensorFinsupp'_symm_single]
  • [x] depends on: #11731
  • [x] depends on: #11748
  • [x] depends on: #11859
• Subalgebra version:
  • [x] depends on: #12025
  • [ ] depends on: #12076
  • [x] depends on: #9626
  • [ ] depends on: #12846
  • [x] depends on: #12847
  • [x] depends on: #12849

[alreadydone]

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?

[AntoineChambert-Loir]

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.

[acmepjz]

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

[AntoineChambert-Loir]

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

[acmepjz]

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.

[acmepjz]

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

[alreadydone]

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.

[acmepjz]

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?

[github-actions[bot]]

PR summary 28b8fd499c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.FieldTheory.LinearDisjoint (new file)	1754

---

Declarations diff

+ LinearDisjoint + LinearDisjoint.symm + bot_left + bot_right + eq_bot_of_self + finrank_sup + inf_eq_bot + linearDisjoint_iff + linearDisjoint_iff' + linearIndependent_left + linearIndependent_mul + linearIndependent_mul' + linearIndependent_right + linearIndependent_right' + of_basis_left + of_basis_mul + of_basis_mul' + of_basis_right + of_basis_right' + of_finrank_coprime + of_finrank_sup + of_le + of_le' + of_le_left + of_le_right + of_le_right' + rank_sup_of_isAlgebraic + self_right ++ linearDisjoint_comm_of_commute +++ linearDisjoint_comm -- linearDisjoint_symm -- linearDisjoint_symm_of_commute

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
219	-1	bare open (scoped) Classical

Current commit 28b8fd499c Reference commit a2a544ab0c

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12434~~
• ~~leanprover-community/mathlib4#11635~~
• ~~leanprover-community/mathlib4#11598~~
• ~~leanprover-community/mathlib4#11731~~
• ~~leanprover-community/mathlib4#11748~~
• ~~leanprover-community/mathlib4#11859~~
• ~~leanprover-community/mathlib4#15346~~
• ~~leanprover-community/mathlib4#12025~~
• ~~leanprover-community/mathlib4#13425~~
• ~~leanprover-community/mathlib4#9626~~
• ~~leanprover-community/mathlib4#12846~~
• ~~leanprover-community/mathlib4#12847~~
• ~~leanprover-community/mathlib4#12849~~
• ~~leanprover-community/mathlib4#18515~~ By Dependent Issues (🤖). Happy coding!

[acmepjz]

All comments are addressed except for the remaining one.

[alreadydone]

Thanks 🎉 maintainer merge

[github-actions[bot]]

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

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build