Skip to content
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.

Sign up for GitHub

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

Jump to bottom

WIP: Remove the requirement from ideal that the underlying ring is commutative #3635

Closed
wants to merge 3 commits into from
Closed

WIP: Remove the requirement from ideal that the underlying ring is commutative #3635

wants to merge 3 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jul 30, 2020 •
edited

This seems to result in an awful lot of tedious theorem copying from submodule and subgroup.
Right now, I'm about a third of the way done with converting ideals.lean.

Will keep going with this another time, but more than happy for someone else to take over.

Some discussion at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Ideals.20over.20algebras

Depends on #3631 and #3634.

@eric-wieser eric-wieser added help-wanted The author needs attention to resolve issues WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jul 30, 2020
eric-wieser
eric-wieser commented Jul 30, 2020
View reviewed changes
src/ring_theory/ideals.lean Outdated
variables [comm_ring α] (I : ideal α) (J : ideal α)

-- these are all copied from submodule
instance : has_coe (ideal α) (set α) := ⟨λ s, s.carrier⟩
Copy link
Member Author

Choose a reason for hiding this comment

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

Submodule used has_coe_t, not sure what the difference is

@PatrickMassot
Copy link
Member

Thanks a lot for tackling this Eric! Everybody has been putting this off for years...

@eric-wieser eric-wieser mentioned this pull request Aug 5, 2020
Closed
bors bot pushed a commit that referenced this pull request Aug 5, 2020
@eric-wieser
chore(ring_theory/ideals): Move the definition of ideals out of algeb…
c63dad1 
…ra/module (#3692)

Neatness was the main motivation - it makes it easier to reason about what would need doing in #3635.
It also results in somewhere sensible for the docs about ideals. Also adds a very minimal docstring to `ring_theory/ideals.lean`.
@eric-wieser eric-wieser removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 6, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 23, 2020
@eric-wieser eric-wieser added please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. and removed help-wanted The author needs attention to resolve issues labels Nov 6, 2020
@eric-wieser
Copy link
Member Author

Everybody has been putting this off for years...

Now that Scott has added ring_quot, I don't really have any motivation for this any more. I've marked it as "please adopt", but won't object to it being closed if that's preferred.

@Ruben-VandeVelde
Copy link
Collaborator

Ref #7654

@jcommelin
Copy link
Member

@eric-wieser This can now be closed, right?

@eric-wieser
Copy link
Member Author

eric-wieser commented Jul 29, 2021 •
edited

I don't think the goal of this PR is fully achieved, but I also don't see myself ever coming back to this, and the diff likely conflicts too much now to be useful.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
merge-conflict Please `git merge origin/master` then a bot will remove this label. please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. WIP Work in progress
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@eric-wieser @PatrickMassot @Ruben-VandeVelde @jcommelin