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: generalize Module.Finite.trans
#9380
Conversation
Mathlib/Algebra/Algebra/Tower.lean
Outdated
theorem span_algebraMap_image_of_tower {S T : Type*} [CommSemiring S] [Semiring T] [Module R S] | ||
[IsScalarTower R S S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) : | ||
[Algebra R T] [Algebra S T] [IsScalarTower R S T] (a : Set S) : |
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 can't be generalized yet with what we include in this PR; this is an application of the CompatibleSMul
class but there's some unresolved controversy with @eric-wieser.
(restrictScalars
consumes CompatibleSMul
which was derived from LinearMap.IsScalarTower.compatibleSMul, but in the absence of IsScalarTower R S S
it can be directly supplied by
variable {R S : Type*} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂]
instance IsScalarTower.compatibleSMul' [SMul R S] [IsScalarTower R S M] :
CompatibleSMul S M R S
in #9046.)
Module.Finite.trans
Module.Finite.trans
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.
Thanks 🎉
bors merge
Add `span_eq_closure` and `closure_induction` which say that `Submodule.span R s` is generated by `R • s` as an AddSubmonoid. I feel that the existing `span_induction` should be replaced by `closure_induction` as the latter is stronger, and allow us to remove the commutativity condition in `span_smul_of_span_eq_top` in Algebra/Tower and generalize `Module.Finite.trans` to allow a non-commutative base ring. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Module.Finite.trans
Module.Finite.trans
Generalize the conditions of the tower law [FiniteDimensional.finrank_mul_finrank'](https://leanprover-community.github.io/mathlib4_docs/Mathlib/FieldTheory/Tower.html#FiniteDimensional.finrank_mul_finrank') in FieldTheory/Tower from `[CommRing F] [Algebra F K]` to `[Ring F] [Module F K]`, and remove the `[Module.Finite F K]` and `[Module.Finite K A]` conditions. The generalized version applies to situations when we have a tower C/B/A where the A-module structure on C is induced from the B-module structure via a RingHom from A to B, and the A-module structure on B is induced by the same RingHom. In particular, it applies when the A-module structure on B and the B-module structure on C come from two RingHoms, and the A-module structure on C comes from the composition of them, regardless of whether A and B are commutative or not. As prerequisites, I also generalized lemmas originally introduced by @kckennylau in [mathlib3#3355](https://github.com/leanprover-community/mathlib/pull/3355/files) to prove the tower law. They were split into three PRs: + LinearAlgebra/Span #9380: add `span_eq_closure` and `closure_induction` which say that `Submodule.span R s` is generated by `R • s` as an AddSubmonoid. I feel that the existing `span_induction` should be replaced by `closure_induction` as the latter is stronger, and allow us to remove the commutativity condition in `span_smul_of_span_eq_top` in Algebra/Tower. + Algebra/Tower #9382: switching from CommSemiring/Algebra to Semiring/Module here requires proving the curious lemma `IsScalarTower.isLinearMap` which states that for a tower of modules A/S/R, any S-linear map from S to A is also R-linear. If the map is injective, we can deduce that S/S/R also form a tower. (By `ringHomEquivModuleIsScalarTower` in #9381, there is therefore a canonical RingHom from R to S.) + Lemmas for free modules over rings including `finrank_mul_finrank'` are moved from FieldTheory/Tower to LinearAlgebra/Dimension/Free [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Puzzle.3A.20noncommutative.20RingHom.20as.20typeclasses/near/407347711) Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Add
span_eq_closure
andclosure_induction
which say thatSubmodule.span R s
is generated byR • s
as an AddSubmonoid. I feel that the existingspan_induction
should be replaced byclosure_induction
as the latter is stronger, and allow us to remove the commutativity condition inspan_smul_of_span_eq_top
in Algebra/Tower and generalizeModule.Finite.trans
to allow a non-commutative base ring.This is one of the uncontroversial parts of #9046.