feat: Equivs for AddMonoidAlgebras #7219
Conversation
Ruben-VandeVelde
added
the
awaiting-author
| @[simps] | ||
| def ringHomCongrLeft {R S G : Type _} [Semiring R] [Semiring S] [AddZeroClass G] (f : R →+* S) : | ||
| AddMonoidAlgebra R G →+* AddMonoidAlgebra S G := | ||
| { Finsupp.mapRange.addMonoidHom f.toAddMonoidHom with |
There was a problem hiding this comment.
If you use one of the lift functions can you avoid needing to prove the map_mul'?
| { ringHomCongrLeft f.toRingHom with | ||
| toFun := (Finsupp.mapRange f f.map_zero : AddMonoidAlgebra R G → AddMonoidAlgebra S G) | ||
| commutes' := fun r => by | ||
| -- Porting note: was `ext` | ||
| refine Finsupp.ext fun a => ?_ | ||
| simp_rw [AddMonoidAlgebra.coe_algebraMap, Function.comp_apply, Finsupp.mapRange_single] | ||
| congr 2 | ||
| rw [AlgHom.map_algebraMap] } |
There was a problem hiding this comment.
I think you can get here more quickly via AlgHom.ofLinearMap (or similar) and using the linear version of Finsupp.mapRange
|
@eric-wieser I didn't see how to apply your suggestions immediately; if you have a moment to share some more details, that would be appreciated, but if not, I'm happy to poke some more. |
| def mapDomainAlgEquiv (k A : Type _) [CommSemiring k] [Semiring A] [Algebra k A] {G H : Type _} | ||
| [AddMonoid G] [AddMonoid H] (f : G ≃+ H) : AddMonoidAlgebra A G ≃ₐ[k] AddMonoidAlgebra A H := |
There was a problem hiding this comment.
| def algAutCongrLeft {k R G : Type _} [CommSemiring k] [Semiring R] [Algebra k R] [AddMonoid G] : | ||
| (R ≃ₐ[k] R) →* AddMonoidAlgebra R G ≃ₐ[k] AddMonoidAlgebra R G where | ||
| toFun f := algEquivCongrLeft f | ||
| map_one' := by | ||
| ext | ||
| refine Finsupp.ext fun a => ?_ | ||
| simp [Finsupp.mapRange_apply] | ||
| map_mul' x y := by | ||
| ext | ||
| refine Finsupp.ext fun a => ?_ | ||
| simp [Finsupp.mapRange_apply] |
There was a problem hiding this comment.
The content of this and mapDomainAlgAut below is basically the comp/trans and id/refl lemmas I mentioned here, so one more reason to add them. Maybe we could do with these lemmas without making them bundled morphisms?
There was a problem hiding this comment.
@negiizhao, is this the only result you actually need in #6718? If so, I'd be inclined not to both with all the Ring versions of things, since you wanted the algebra version anyway.
Extracted from #6718.