Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(ring_theory/algebra_tower): alg_hom_equiv_sigma #5345

Closed
wants to merge 15 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Dec 13, 2020

Proves that algebra homomorphisms from the top of an is_scalar_tower are the same as a pair of algebra homomorphisms.

This is useful for counting algebra homomorphisms.


@bryangingechen bryangingechen added the awaiting-review The author would like community review of the PR label Dec 13, 2020
tb65536 and others added 4 commits December 14, 2020 11:07
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
src/ring_theory/algebra_tower.lean Outdated Show resolved Hide resolved
src/ring_theory/algebra_tower.lean Outdated Show resolved Hide resolved
src/ring_theory/algebra_tower.lean Outdated Show resolved Hide resolved
tb65536 and others added 3 commits December 15, 2020 20:41
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@eric-wieser
Copy link
Member

@tb65536, CI is not running on this PR because your email address has not been verified with github, it seems.

src/ring_theory/algebra_tower.lean Outdated Show resolved Hide resolved
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 16, 2020
bors bot pushed a commit that referenced this pull request Dec 16, 2020
Proves that algebra homomorphisms from the top of an is_scalar_tower are the same as a pair of algebra homomorphisms.

This is useful for counting algebra homomorphisms.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
@bors
Copy link

bors bot commented Dec 16, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/algebra_tower): alg_hom_equiv_sigma [Merged by Bors] - feat(ring_theory/algebra_tower): alg_hom_equiv_sigma Dec 16, 2020
@bors bors bot closed this Dec 16, 2020
@bors bors bot deleted the alg_hom_tower branch December 16, 2020 23:49
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants