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

[Merged by Bors] - chore(ring_theory/ideal/local_ring): generalize to semirings #13341

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - chore(ring_theory/ideal/local_ring): generalize to semirings #13341

Changes from 1 commit
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
5e6d655
init
yuma-mizuno Apr 11, 2022
6dc7766
minor change
yuma-mizuno Apr 11, 2022
fb950fa
rename lemma
yuma-mizuno Apr 13, 2022
152f2aa
separate `comm_semiring` and `comm_ring`
yuma-mizuno Apr 13, 2022
f9ccbb2
golf
yuma-mizuno Apr 13, 2022
a23c973
rearrange lemmas
yuma-mizuno Apr 14, 2022
d053d93
lint style
yuma-mizuno Apr 14, 2022
8f2561d
fix
yuma-mizuno Apr 14, 2022
1eb6cb4
fix docs
yuma-mizuno Apr 14, 2022
54cb6fd
use `nontrivial R` instead of `hnze`
yuma-mizuno Apr 14, 2022
c1f7aef
fix docs
yuma-mizuno Apr 15, 2022
f563be0
update docs for `is_local_ring_hom`
yuma-mizuno Apr 15, 2022
ade415c
Merge branch 'master' into local-semiring
yuma-mizuno Apr 15, 2022
b1213a3
fix
yuma-mizuno Apr 15, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
3 changes: 1 addition & 2 deletions src/ring_theory/ideal/local_ring.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,7 @@ universes u v w u'

variables {R : Type u} {S : Type v} {T : Type w} {K : Type u'}

/-- A commutative ring is local if it has a unique maximal ideal. Note that
`local_ring` is a predicate. -/
/-- A semiring is local if it has a unique maximal ideal. Note that `local_ring` is a predicate. -/
Copy link
Member

Choose a reason for hiding this comment

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

I mean that now the definition is not that there is only one maximal ideal.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks I see what you mean.

Having unique maximal ideal ii not the definition itself even in the previous file. I guess that the previous author wrote such docs as the file show the equivalence of the definitions soon after. Should we write the actual definition here?

Copy link
Member

Choose a reason for hiding this comment

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

Yes, you can add a comment saying it is equivalent to the usual one.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

OK!

class local_ring (R : Type u) [semiring R] extends nontrivial R : Prop :=
(nonunits_add : ∀ {a b : R}, a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R)

Expand Down