feat: definition and basic properties of linearly disjoint #9651

acmepjz · 2024-01-11T13:05:46Z

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

alreadydone · 2024-01-11T16:08:47Z

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

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.
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.
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?

Mathlib/FieldTheory/LinearlyDisjoint.lean

AntoineChambert-Loir · 2024-01-12T01:06:49Z

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 · 2024-01-12T01:25:39Z

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

AntoineChambert-Loir · 2024-01-12T07:43:58Z

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

Mathlib/FieldTheory/LinearDisjoint.lean

acmepjz · 2024-02-26T20:06:47Z

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 · 2024-02-27T18:08:15Z

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

alreadydone · 2024-02-29T01:41:58Z

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 · 2024-03-05T12:56:17Z

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?

# Conflicts: # Mathlib/LinearAlgebra/LinearDisjoint.lean

…arly disjoint of submodules (#12434) 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.

leanprover-community-mathlib4-bot · 2024-07-10T11:03:40Z

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: 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~~
By Dependent Issues (🤖). Happy coding!

# Conflicts: # Mathlib.lean

github-actions · 2024-07-10T11:18:32Z

PR summary 63dbf292de

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.LinearAlgebra.TensorProduct.Subalgebra`	1158
`Mathlib.RingTheory.LinearDisjoint`	1482
`Mathlib.FieldTheory.LinearDisjoint`	1508

Declarations diff

+ LinearDisjoint.of_subsingleton
+ LinearDisjoint.symm_of_commute
+ _root_.AlgebraicIndependent.algEquivField
+ _root_.AlgebraicIndependent.algebraMap_algEquivField
+ _root_.AlgebraicIndependent.transcendental
+ _root_.FractionRing.algEquiv!!!
+ _root_.FractionRing.card_le
+ _root_.IntermediateField.finrank_sup_le
+ _root_.IntermediateField.mem_adjoin_range_iff
+ _root_.IntermediateField.rank_sup_le_of_isAlgebraic
+ _root_.IsAlgebraic.of_aeval
+ _root_.IsFractionRing.algEquivOfAlgEquiv
+ _root_.IsLocalization.algEquivOfAlgEquiv
+ _root_.IsTranscendenceBasis.isAlgebraic_field
+ _root_.Localization.card_le
+ _root_.Localization.card_le'
+ _root_.MulEquiv.map_nonZeroDivisors
+ _root_.MvPolynomial.algebraicIndependent_X
+ _root_.MvPolynomial.transcendental_X
+ _root_.Polynomial.aeval_comp!!!
+ _root_.Polynomial.transcendental
+ _root_.Polynomial.transcendental_X
+ _root_.Transcendental.aeval
+ _root_.Transcendental.linearIndependent_sub_inv
+ _root_.exists_isTranscendenceBasis'
+ _root_.rank_fractionRing_mvPolynomial_eq
+ _root_.transcendental_algebraMap_iff
+ _root_.transcendental_iff
+ _root_.transcendental_iff_algebraicIndependent
+ _root_.transcendental_iff_injective_aeval
+ _root_.transcendental_iff_ker_eq_bot
+ adjoin_rank_eq_rank_left
+ adjoin_rank_eq_rank_right
+ comm_trans_lTensorBot
+ comm_trans_rTensorBot
+ eq_bot_of_commute_of_self
+ finrank_sup_le_of_free
+ finrank_sup_of_free
+ inf_eq_bot_of_commute
+ instance (priority := 10) _root_.IntermediateField.instAlgebraAlgebraAdjoin
+ instance (priority := 10) _root_.IntermediateField.instIsFractionRingAlgebraAdjoin
+ instance (priority := 10) _root_.IntermediateField.instIsScalarTowerAlgebraAdjoin
+ instance (priority := 10) _root_.IntermediateField.instModuleAlgebraAdjoin
+ instance (priority := 10) _root_.IntermediateField.instSMulAlgebraAdjoin
+ lTensorBot
+ lTensorBot_one_tmul
+ lTensorBot_symm_apply
+ lTensorBot_tmul
+ linearDisjoint_iff'
+ linearDisjoint_symm_of_commute
+ linearIndependent_left
+ linearIndependent_left_of_flat
+ linearIndependent_left_of_flat_of_commute
+ linearIndependent_left_op_of_flat
+ linearIndependent_mul
+ linearIndependent_mul'
+ linearIndependent_mul_of_flat
+ linearIndependent_mul_of_flat_left
+ linearIndependent_mul_of_flat_right
+ linearIndependent_right
+ linearIndependent_right'
+ linearIndependent_right_of_flat
+ mulLeftMap_ker_eq_bot_iff_linearIndependent_op
+ mulMap'
+ mulMap'_surjective
+ mulMap_bot_left_eq
+ mulMap_bot_right_eq
+ mulMap_comm
+ mulMap_range
+ mulMap_tmul
+ mulMap_toLinearMap
+ mulRightMap_ker_eq_bot_iff_linearIndependent
+ of_basis_left_of_commute
+ of_basis_left_op
+ of_basis_mul'
+ of_basis_right'
+ of_finrank_coprime
+ of_finrank_coprime_of_free
+ of_finrank_sup_of_free
+ of_le
+ of_le'
+ of_le_left
+ of_le_left_of_flat
+ of_le_of_flat_left
+ of_le_of_flat_right
+ of_le_right
+ of_le_right'
+ of_le_right_of_flat
+ of_linearDisjoint_finite
+ of_linearDisjoint_finite_left
+ of_linearDisjoint_finite_right
+ rTensorBot
+ rTensorBot_symm_apply
+ rTensorBot_tmul
+ rTensorBot_tmul_one
+ rank_eq_one_of_commute_of_flat_of_self_of_inj
+ rank_eq_one_of_flat_of_self_of_inj
+ rank_inf_eq_one_of_commute_of_flat_left_of_inj
+ rank_inf_eq_one_of_commute_of_flat_of_inj
+ rank_inf_eq_one_of_commute_of_flat_right_of_inj
+ rank_inf_eq_one_of_flat_left_of_inj
+ rank_inf_eq_one_of_flat_of_inj
+ rank_inf_eq_one_of_flat_right_of_inj
+ rank_sup_le_of_free
+ rank_sup_of_free
+ self_right
+ sup_free_of_free
+ val_mulMap'_tmul
+ val_mulMap_tmul
++ LinearDisjoint.symm
++ bot_left
++ bot_right
++ eq_bot_of_self
++ inf_eq_bot
++ linearDisjoint_symm
++ mulMap
++ of_basis_left
++ of_basis_mul
++ of_basis_right
+++ LinearDisjoint

You can run this locally as follows

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

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

…d by multiplication for subalgebras (#14611) This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).

add lienarly disjoint

59dcfbd

acmepjz added WIP Work in progress t-algebra Algebra (groups, rings, fields etc) labels Jan 11, 2024

acmepjz changed the title ~~feat(FieldTheory/LinearlyDisjoint): definition of lienarly disjoint and basic properties~~ feat(FieldTheory/LinearlyDisjoint): definition of linearly disjoint and basic properties Jan 11, 2024

fix sorry

8697393

alreadydone reviewed Jan 11, 2024

View reviewed changes

Mathlib/FieldTheory/LinearlyDisjoint.lean Outdated Show resolved Hide resolved

apply suggestions and add some more results

fd4987f

rename file

006ccbe

acmepjz commented Jan 23, 2024

View reviewed changes

Mathlib/FieldTheory/LinearDisjoint.lean Outdated Show resolved Hide resolved

acmepjz added 2 commits February 21, 2024 07:39

Merge branch 'master' into acmepjz_lin_disj

cc8279b

fix compile errors

de83290

acmepjz added 2 commits March 13, 2024 12:03

Merge branch 'master' into acmepjz_lin_disj

ca8a007

Merge branch 'master' into acmepjz_lin_disj

8c71e11

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Mar 23, 2024

acmepjz changed the title ~~feat(FieldTheory/LinearlyDisjoint): definition of linearly disjoint and basic properties~~ feat(): definition of linearly disjoint and basic properties Mar 23, 2024

acmepjz added 3 commits March 24, 2024 03:43

copy a file from #10824

18f6d82

move file

cae7252

WIP with a lot of sorry

716f393

acmepjz changed the title ~~feat(): definition of linearly disjoint and basic properties~~ feat(LinearAlgebra/LinearDisjoint): definition of linearly disjoint and basic properties Mar 23, 2024

acmepjz added 3 commits March 25, 2024 03:56

add of_map_linearIndependent_(left|right)

3aa9f75

add [of_]map_linearIndependent_mul[...]

a9425e9

add properties regarding inclusion

1d1c257

acmepjz added 12 commits May 5, 2024 07:07

Merge branch 'acmepjz_lin_disj_1' into acmepjz_lin_disj

63cf1f7

# Conflicts: # Mathlib/LinearAlgebra/LinearDisjoint.lean

split Subalgebra.mulMap to another file

ad5d203

add results for intermediate fields (WIP)

1e2a0aa

golf

a48366b

add Subalgebra.(l|r)TensorBot

6476f50

add random results (WIP)

d7f1d4d

add some more WIP results

ea15a3b

adapt #12846 and move some results

42ea134

adapt #12847 and #12849

b0b6ce1

Merge branch 'master' into acmepjz_lin_disj

ad4dd9a

adapt recent changes

9775c61

add more WIP

f694d96

leanprover-community-mathlib4-bot added the blocked-by-other-PR label May 27, 2024

YaelDillies removed the blocked-by-other-PR label May 28, 2024

leanprover-community-mathlib4-bot added the blocked-by-other-PR label May 28, 2024

YaelDillies removed the blocked-by-other-PR label May 28, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jun 9, 2024

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Jul 10, 2024

acmepjz added 2 commits July 10, 2024 19:16

copy files from master

219dff5

Merge branch 'master' into acmepjz_lin_disj

411a991

# Conflicts: # Mathlib.lean

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 10, 2024

fix build error

90beed2

acmepjz mentioned this pull request Jul 10, 2024

[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras #14611

Closed

fix line length

63dbf29

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Jul 16, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: definition and basic properties of linearly disjoint #9651

feat: definition and basic properties of linearly disjoint #9651

acmepjz commented Jan 11, 2024 •

edited

Loading

alreadydone commented Jan 11, 2024 •

edited

Loading

AntoineChambert-Loir commented Jan 12, 2024

acmepjz commented Jan 12, 2024 •

edited

Loading

AntoineChambert-Loir commented Jan 12, 2024

acmepjz commented Feb 26, 2024 •

edited

Loading

acmepjz commented Feb 27, 2024

alreadydone commented Feb 29, 2024

acmepjz commented Mar 5, 2024

leanprover-community-mathlib4-bot commented Jul 10, 2024

github-actions bot commented Jul 10, 2024 •

edited

Loading

Declarations diff

feat: definition and basic properties of linearly disjoint #9651

Are you sure you want to change the base?

feat: definition and basic properties of linearly disjoint #9651

Conversation

acmepjz commented Jan 11, 2024 • edited Loading

alreadydone commented Jan 11, 2024 • edited Loading

AntoineChambert-Loir commented Jan 12, 2024

acmepjz commented Jan 12, 2024 • edited Loading

AntoineChambert-Loir commented Jan 12, 2024

acmepjz commented Feb 26, 2024 • edited Loading

acmepjz commented Feb 27, 2024

alreadydone commented Feb 29, 2024

acmepjz commented Mar 5, 2024

leanprover-community-mathlib4-bot commented Jul 10, 2024

github-actions bot commented Jul 10, 2024 • edited Loading

PR summary 63dbf292de

Import changes for modified files

Declarations diff

acmepjz commented Jan 11, 2024 •

edited

Loading

alreadydone commented Jan 11, 2024 •

edited

Loading

acmepjz commented Jan 12, 2024 •

edited

Loading

acmepjz commented Feb 26, 2024 •

edited

Loading

github-actions bot commented Jul 10, 2024 •

edited

Loading