[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) by acmepjz · Pull Request #17820 · leanprover-community/mathlib4

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

[Merged by Bors] - feat(RingTheory/LinearDisjoint): properties of linearly disjoint of subalgebras (2) #15346

Closed

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 A reviewer has approved the changed; awaiting maintainer approval. 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

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

Conversation

acmepjz commented Oct 16, 2024

Uh oh!

github-actions bot commented Oct 16, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e3b75b0cf5

Import changes for modified files

Declarations diff

Uh oh!

erdOne commented Oct 16, 2024

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

acmepjz commented Oct 16, 2024

Uh oh!

acmepjz commented Oct 26, 2024

Uh oh!

erdOne commented Oct 28, 2024

Uh oh!

github-actions bot commented Oct 28, 2024

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 28, 2024

Uh oh!

acmepjz commented Oct 28, 2024

Uh oh!

mathlib-bors bot commented Oct 28, 2024

Uh oh!

mathlib-bors bot commented Oct 28, 2024

Uh oh!

acmepjz commented Oct 28, 2024

Uh oh!

mathlib-bors bot commented Oct 28, 2024

Uh oh!

acmepjz commented Oct 28, 2024

Uh oh!

mathlib-bors bot commented Oct 28, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Oct 16, 2024 •

edited

Loading