[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820

acmepjz · 2024-10-16T10:31:36Z

Main definitions:

Subalgebra.LinearDisjoint: two subalgebras are linearly disjoint, if they are
linearly disjoint as submodules (Submodule.LinearDisjoint).
Subalgebra.LinearDisjoint.mulMap: if two subalgebras A and B of S / R are
linearly disjoint, then there is A ⊗[R] B ≃ₐ[R] A ⊔ B induced by multiplication in S.

Equivalent characterization of linearly disjointness:

Subalgebra.LinearDisjoint.linearIndependent_left_of_flat:
if A and B are linearly disjoint, if B is a flat R-module, then for any family of
R-linearly independent elements of A, they are also B-linearly independent.
Subalgebra.LinearDisjoint.of_basis_left:
conversely, if a basis of A is also B-linearly independent, then A and B are linearly disjoint.
Subalgebra.LinearDisjoint.linearIndependent_right_of_flat:
if A and B are linearly disjoint, if A is a flat R-module, then for any family of
R-linearly independent elements of B, they are also A-linearly independent.
Subalgebra.LinearDisjoint.of_basis_right:
conversely, if a basis of B is also A-linearly independent,
then A and B are linearly disjoint.
Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat:
if A and B are linearly disjoint, if one of A and B is flat, then for any family of
R-linearly independent elements { a_i } of A, and any family of
R-linearly independent elements { b_j } of B, the family { a_i * b_j } in S is
also R-linearly independent.
Subalgebra.LinearDisjoint.of_basis_mul:
conversely, if { a_i } is an R-basis of A, if { b_j } is an R-basis of B,
such that the family { a_i * b_j } in S is R-linearly independent,
then A and B are linearly disjoint.

Other main results:

Subalgebra.LinearDisjoint.symm_of_commute, Subalgebra.linearDisjoint_symm_of_commute:
linearly disjoint is symmetric under some commutative conditions.
Subalgebra.LinearDisjoint.bot_left, Subalgebra.LinearDisjoint.bot_right:
the image of R in S is linearly disjoint with any other subalgebras.
Subalgebra.LinearDisjoint.sup_free_of_free: the compositum of two linearly disjoint
subalgebras is a free module, if two subalgebras are also free modules.
Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, Subalgebra.LinearDisjoint.inf_eq_bot:
if A and B are linearly disjoint, under suitable technical conditions, they are disjoint.

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

github-actions · 2024-10-16T10:32:24Z

PR summary e3b75b0cf5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.LinearDisjoint`	1586

Declarations diff

+ LinearDisjoint
+ LinearDisjoint.of_subsingleton
+ LinearDisjoint.symm
+ LinearDisjoint.symm_of_commute
+ bot_left
+ bot_right
+ eq_bot_of_commute_of_self
+ eq_bot_of_self
+ inf_eq_bot
+ inf_eq_bot_of_commute
+ linearDisjoint_iff
+ linearDisjoint_symm
+ linearDisjoint_symm_of_commute
+ linearIndependent_left_of_flat
+ linearIndependent_left_of_flat_of_commute
+ linearIndependent_left_op_of_flat
+ linearIndependent_mul_of_flat
+ linearIndependent_mul_of_flat_left
+ linearIndependent_mul_of_flat_right
+ linearIndependent_right_of_flat
+ mulLeftMap_ker_eq_bot_iff_linearIndependent_op
+ mulMap
+ mulRightMap_ker_eq_bot_iff_linearIndependent
+ of_basis_left
+ of_basis_left_of_commute
+ of_basis_left_op
+ of_basis_mul
+ of_basis_right
+ of_le_left_of_flat
+ of_le_of_flat_left
+ of_le_of_flat_right
+ of_le_right_of_flat
+ of_linearDisjoint_finite
+ of_linearDisjoint_finite_left
+ of_linearDisjoint_finite_right
+ sup_free_of_free
+ val_mulMap_tmul

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.

erdOne · 2024-10-16T10:59:30Z

Sorry for dropping the ball on this. This looks good to me. I'll wait if @kbuzzard wants to give it a look and I'll maintainer merge it this evening otherwise.

kbuzzard

This is a great piece of work!

Mathlib/RingTheory/LinearDisjoint.lean

acmepjz · 2024-10-16T13:03:56Z

Done.

acmepjz · 2024-10-26T16:34:25Z

ping what's the progress?

erdOne · 2024-10-28T04:52:31Z

Thanks!
maintainer merge

github-actions · 2024-10-28T04:52:49Z

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

jcommelin

bors d+

Mathlib/RingTheory/LinearDisjoint.lean

mathlib-bors · 2024-10-28T05:54:41Z

✌️ 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.

Co-authored-by: Johan Commelin <johan@commelin.net>

acmepjz · 2024-10-28T06:22:46Z

bors r+

…y disjoint of subalgebras (1) (#17820) Main definitions: - `Subalgebra.LinearDisjoint`: two subalgebras are linearly disjoint, if they are linearly disjoint as submodules (`Submodule.LinearDisjoint`). - `Subalgebra.LinearDisjoint.mulMap`: if two subalgebras `A` and `B` of `S / R` are linearly disjoint, then there is `A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. Equivalent characterization of linearly disjointness: - `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`: if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of `R`-linearly independent elements of `A`, they are also `B`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_left`: conversely, if a basis of `A` is also `B`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`: if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of `R`-linearly independent elements of `B`, they are also `A`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_right`: conversely, if a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`: if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of `R`-linearly independent elements `{ a_i }` of `A`, and any family of `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is also `R`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_mul`: conversely, if `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`, such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent, then `A` and `B` are linearly disjoint. Other main results: - `Subalgebra.LinearDisjoint.symm_of_commute`, `Subalgebra.linearDisjoint_symm_of_commute`: linearly disjoint is symmetric under some commutative conditions. - `Subalgebra.LinearDisjoint.bot_left`, `Subalgebra.LinearDisjoint.bot_right`: the image of `R` in `S` is linearly disjoint with any other subalgebras. - `Subalgebra.LinearDisjoint.sup_free_of_free`: the compositum of two linearly disjoint subalgebras is a free module, if two subalgebras are also free modules. - `Subalgebra.LinearDisjoint.inf_eq_bot_of_commute`, `Subalgebra.LinearDisjoint.inf_eq_bot`: if `A` and `B` are linearly disjoint, under suitable technical conditions, they are disjoint. The results with name containing "of_commute" also have corresponding specified versions assuming `S` is commutative.

mathlib-bors · 2024-10-28T07:22:32Z

Build failed (retrying...):

Build

…y disjoint of subalgebras (1) (#17820) Main definitions: - `Subalgebra.LinearDisjoint`: two subalgebras are linearly disjoint, if they are linearly disjoint as submodules (`Submodule.LinearDisjoint`). - `Subalgebra.LinearDisjoint.mulMap`: if two subalgebras `A` and `B` of `S / R` are linearly disjoint, then there is `A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. Equivalent characterization of linearly disjointness: - `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`: if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of `R`-linearly independent elements of `A`, they are also `B`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_left`: conversely, if a basis of `A` is also `B`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`: if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of `R`-linearly independent elements of `B`, they are also `A`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_right`: conversely, if a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`: if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of `R`-linearly independent elements `{ a_i }` of `A`, and any family of `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is also `R`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_mul`: conversely, if `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`, such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent, then `A` and `B` are linearly disjoint. Other main results: - `Subalgebra.LinearDisjoint.symm_of_commute`, `Subalgebra.linearDisjoint_symm_of_commute`: linearly disjoint is symmetric under some commutative conditions. - `Subalgebra.LinearDisjoint.bot_left`, `Subalgebra.LinearDisjoint.bot_right`: the image of `R` in `S` is linearly disjoint with any other subalgebras. - `Subalgebra.LinearDisjoint.sup_free_of_free`: the compositum of two linearly disjoint subalgebras is a free module, if two subalgebras are also free modules. - `Subalgebra.LinearDisjoint.inf_eq_bot_of_commute`, `Subalgebra.LinearDisjoint.inf_eq_bot`: if `A` and `B` are linearly disjoint, under suitable technical conditions, they are disjoint. The results with name containing "of_commute" also have corresponding specified versions assuming `S` is commutative.

mathlib-bors · 2024-10-28T08:12:32Z

Build failed (retrying...):

Build

acmepjz · 2024-10-28T08:43:48Z

bors r-

mathlib-bors · 2024-10-28T08:43:50Z

Canceled.

acmepjz · 2024-10-28T09:07:03Z

bors r+

…y disjoint of subalgebras (1) (#17820) Main definitions: - `Subalgebra.LinearDisjoint`: two subalgebras are linearly disjoint, if they are linearly disjoint as submodules (`Submodule.LinearDisjoint`). - `Subalgebra.LinearDisjoint.mulMap`: if two subalgebras `A` and `B` of `S / R` are linearly disjoint, then there is `A ⊗[R] B ≃ₐ[R] A ⊔ B` induced by multiplication in `S`. Equivalent characterization of linearly disjointness: - `Subalgebra.LinearDisjoint.linearIndependent_left_of_flat`: if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module, then for any family of `R`-linearly independent elements of `A`, they are also `B`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_left`: conversely, if a basis of `A` is also `B`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_right_of_flat`: if `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of `R`-linearly independent elements of `B`, they are also `A`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_right`: conversely, if a basis of `B` is also `A`-linearly independent, then `A` and `B` are linearly disjoint. - `Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat`: if `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of `R`-linearly independent elements `{ a_i }` of `A`, and any family of `R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is also `R`-linearly independent. - `Subalgebra.LinearDisjoint.of_basis_mul`: conversely, if `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`, such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent, then `A` and `B` are linearly disjoint. Other main results: - `Subalgebra.LinearDisjoint.symm_of_commute`, `Subalgebra.linearDisjoint_symm_of_commute`: linearly disjoint is symmetric under some commutative conditions. - `Subalgebra.LinearDisjoint.bot_left`, `Subalgebra.LinearDisjoint.bot_right`: the image of `R` in `S` is linearly disjoint with any other subalgebras. - `Subalgebra.LinearDisjoint.sup_free_of_free`: the compositum of two linearly disjoint subalgebras is a free module, if two subalgebras are also free modules. - `Subalgebra.LinearDisjoint.inf_eq_bot_of_commute`, `Subalgebra.LinearDisjoint.inf_eq_bot`: if `A` and `B` are linearly disjoint, under suitable technical conditions, they are disjoint. The results with name containing "of_commute" also have corresponding specified versions assuming `S` is commutative.

mathlib-bors · 2024-10-28T09:36:49Z

Pull request successfully merged into master.

Build succeeded:

add

475196c

acmepjz added the t-algebra Algebra (groups, rings, fields, etc) label Oct 16, 2024

acmepjz mentioned this pull request Oct 16, 2024

feat(RingTheory/LinearDisjoint): properties of linearly disjoint of subalgebras (2) #15346

Open

2 tasks

fix import

559c1e0

kbuzzard approved these changes Oct 16, 2024

View reviewed changes

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

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

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

kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 16, 2024

acmepjz added 2 commits October 16, 2024 21:03

add a little bit docstring

ef201dd

apply suggestions

5eb3441

acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 16, 2024

github-actions bot added the maintainer-merge label Oct 28, 2024

jcommelin reviewed Oct 28, 2024

View reviewed changes

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

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

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

leanprover-community-mathlib4-bot added the delegated label Oct 28, 2024

Apply suggestions from code review

6a67407

Co-authored-by: Johan Commelin <johan@commelin.net>

acmepjz added 2 commits October 28, 2024 16:46

Merge branch 'master' into acmepjz_lin_disj_subalg_1

8333def

fix

e3b75b0

mathlib-bors bot changed the title ~~feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1)~~ [Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) Oct 28, 2024

mathlib-bors bot closed this Oct 28, 2024

mathlib-bors bot deleted the acmepjz_lin_disj_subalg_1 branch October 28, 2024 09:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820

[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820

acmepjz commented Oct 16, 2024

github-actions bot commented Oct 16, 2024 •

edited

Loading

Declarations diff

erdOne commented Oct 16, 2024

kbuzzard left a comment

acmepjz commented Oct 16, 2024

acmepjz commented Oct 26, 2024

erdOne commented Oct 28, 2024

github-actions bot commented Oct 28, 2024

jcommelin left a comment

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820

[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820

Conversation

acmepjz commented Oct 16, 2024

github-actions bot commented Oct 16, 2024 • edited Loading

PR summary e3b75b0cf5

Import changes for modified files

Declarations diff

erdOne commented Oct 16, 2024

kbuzzard left a comment

Choose a reason for hiding this comment

acmepjz commented Oct 16, 2024

acmepjz commented Oct 26, 2024

erdOne commented Oct 28, 2024

github-actions bot commented Oct 28, 2024

jcommelin left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

acmepjz commented Oct 28, 2024

mathlib-bors bot commented Oct 28, 2024

github-actions bot commented Oct 16, 2024 •

edited

Loading