-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(RingTheory/LinearDisjoint): definition and properties of linearly disjoint of subalgebras (1) #17820
Conversation
PR summary e3b75b0cf5Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a great piece of work!
Done. |
ping what's the progress? |
Thanks! |
🚀 Pull request has been placed on the maintainer queue by erdOne. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
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.
Build failed (retrying...): |
…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.
Build failed (retrying...): |
bors r- |
Canceled. |
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.
Pull request successfully merged into master. Build succeeded: |
Main definitions:
Subalgebra.LinearDisjoint
: two subalgebras are linearly disjoint, if they arelinearly disjoint as submodules (
Submodule.LinearDisjoint
).Subalgebra.LinearDisjoint.mulMap
: if two subalgebrasA
andB
ofS / R
arelinearly disjoint, then there is
A ⊗[R] B ≃ₐ[R] A ⊔ B
induced by multiplication inS
.Equivalent characterization of linearly disjointness:
Subalgebra.LinearDisjoint.linearIndependent_left_of_flat
:if
A
andB
are linearly disjoint, ifB
is a flatR
-module, then for any family ofR
-linearly independent elements ofA
, they are alsoB
-linearly independent.Subalgebra.LinearDisjoint.of_basis_left
:conversely, if a basis of
A
is alsoB
-linearly independent, thenA
andB
are linearly disjoint.Subalgebra.LinearDisjoint.linearIndependent_right_of_flat
:if
A
andB
are linearly disjoint, ifA
is a flatR
-module, then for any family ofR
-linearly independent elements ofB
, they are alsoA
-linearly independent.Subalgebra.LinearDisjoint.of_basis_right
:conversely, if a basis of
B
is alsoA
-linearly independent,then
A
andB
are linearly disjoint.Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat
:if
A
andB
are linearly disjoint, if one ofA
andB
is flat, then for any family ofR
-linearly independent elements{ a_i }
ofA
, and any family ofR
-linearly independent elements{ b_j }
ofB
, the family{ a_i * b_j }
inS
isalso
R
-linearly independent.Subalgebra.LinearDisjoint.of_basis_mul
:conversely, if
{ a_i }
is anR
-basis ofA
, if{ b_j }
is anR
-basis ofB
,such that the family
{ a_i * b_j }
inS
isR
-linearly independent,then
A
andB
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
inS
is linearly disjoint with any other subalgebras.Subalgebra.LinearDisjoint.sup_free_of_free
: the compositum of two linearly disjointsubalgebras 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
andB
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