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

yuma-mizuno · 2022-04-11T11:08:56Z

riccardobrasca · 2022-04-13T09:04:23Z

src/ring_theory/ideal/local_ring.lean

@@ -32,53 +32,43 @@ universes u v w

 /-- A commutative ring is local if it has a unique maximal ideal. Note that
  `local_ring` is a predicate. -/
-class local_ring (R : Type u) [comm_ring R] extends nontrivial R : Prop :=
-(is_local : ∀ (a : R), (is_unit a) ∨ (is_unit (1 - a)))
+class local_ring (R : Type u) [comm_semiring R] extends nontrivial R : Prop :=


Can you add back the old nonunits_add? Now it is immediate from the definition, but it could be useful.

The old nonunits_add can be accessed with the same name local_ring.nonunits_add in the new definition. I would like to remark that the proof of the old nonunits_add is moved to the proof of the lemma local_of_is_unit_or_is_unit_one_sub_self, which plays the same role as the old version constructor of local_ring.

But since local_ring is a class in practice there will be no h : local_ring R, so it will b annoying to access it. Or do you see another way?

Yes, if I understand correctly, the current local_ring.nonunits_add is intended to be used either with the fully specified name local_ring.nonunit_add or with nonunits_add followed by open local_ring (or in the namespace local_ring). With the new definition this lemma is exactly the projection of local_ring that is automatically generated when the class is defined.

In fact, nonunits_add is used in the definition of local_ring.maximal_ideal here, but there was no need to change this part in this PR.

Ah yes, it works because the lemma I want is automatically created by Lean.

src/ring_theory/ideal/local_ring.lean

riccardobrasca · 2022-04-13T09:08:05Z

src/ring_theory/ideal/local_ring.lean


 namespace local_ring

-variables {R : Type u} [comm_ring R] [local_ring R]
+variables {R : Type u}


I think it is more readable if you put [comm_semiring R] [local_ring R] here., and use another variable S with [comm_ring S] [local_ring S].

Thank you for your suggestion! Although it's different from the proposed method, I have divided lemmas for comm_semiring and comm_ring into two sections. I think the order of the lemmas has become logically easier to read. What do you think about this?

src/ring_theory/ideal/local_ring.lean

riccardobrasca · 2022-04-13T13:59:07Z

src/ring_theory/ideal/local_ring.lean

+end comm_semiring
+
+section comm_ring
+variables {R : Type u} [comm_ring R] [local_ring R]


You can move this line at the beginning of the file, so you only write {R : Type u} {S : Type v} once, and then you only need [comm_ring] and similar.

riccardobrasca · 2022-04-13T14:02:49Z

There are still a lot of [semiring R] floating around. It would be better to move all the lemmas in the appropriate section. Essentially almost no lemma should have [ring R]/[semiring R] written explicitly (there are exceptions of course).

to reduce implicit arguments

riccardobrasca · 2022-04-14T09:30:03Z

src/ring_theory/ideal/local_ring.lean

-universes u v w
+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


This needs to be fixed.

riccardobrasca · 2022-04-14T09:31:00Z

src/ring_theory/ideal/local_ring.lean

-lemma is_unit_of_mem_nonunits_one_sub_self (a : R) (h : (1 - a) ∈ nonunits R) :
-  is_unit a :=
-or_iff_not_imp_right.1 (is_local a) h
+lemma of_nonunits_ideal (hnze : (0:R) ≠ 1) (h : ∀ x y ∈ nonunits R, x + y ∈ nonunits R) :


Instead of hnze I would use nontrivial R.

riccardobrasca · 2022-04-14T09:34:32Z

src/ring_theory/ideal/local_ring.lean

+
+end local_ring
+
+end comm_ring

 /-- A local ring homomorphism is a homomorphism between local rings


This needs to be fixed.

riccardobrasca · 2022-04-14T22:05:22Z

src/ring_theory/ideal/local_ring.lean

@@ -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. -/


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

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?

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

riccardobrasca · 2022-04-15T10:00:57Z

Thanks!

bors d+

bors · 2022-04-15T10:00:58Z

✌️ yuma-mizuno can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

yuma-mizuno · 2022-04-15T10:33:01Z

bors r+

bors · 2022-04-15T10:38:44Z

Build failed:

Build mathlib

yuma-mizuno · 2022-04-15T14:12:38Z

bors r+

bors · 2022-04-15T17:08:51Z

Pull request successfully merged into master.

Build succeeded:

The main ingredient of this PR is the definition of `is_localization.lift` that works for semirings. The previous definition uses `ring_hom.mk'` that essentially states that `f 0 = 0` follows from other conditions. This does not holds for semirings. Instead, this PR defines the localization of monoid with zero, and uses this to define `is_localization.lift`. - I think definitions around `localization_with_zero_map` might be ad hoc, and any suggestions for improvement are welcome! - I plan to further generalize the localization API for semirings. This needs generalization of other ring theory stuff such as `local_ring` and `is_domain` (generalizing `local_ring` is partially done in #13341).

…13471) What is essentially new is the proof of `local_ring.of_surjective` and `local_ring.is_unit_or_is_unit_of_is_unit_add`. - I changed the definition of local ring to `local_ring.of_is_unit_or_is_unit_of_add_one`, which is reminiscent of the definition before the recent change in #13341. The equivalence of the previous definition is essentially given by `local_ring.is_unit_or_is_unit_of_is_unit_add`. The choice of the definition is insignificant here because they are all equivalent, but I think the choice here is better for the default constructor because this condition is "weaker" than e.g. `local_ring.of_non_units_add` in some sense. - The proof of `local_ring.of_surjective` needs `[is_local_ring_hom f]`, which was not necessary for commutative rings in the previous proof. So the new version here is not a genuine generalization of the previous version. The previous version was renamed to `local_ring.of_surjective'`.

yuma-mizuno added 2 commits April 11, 2022 18:32

init

5e6d655

minor change

6dc7766

yuma-mizuno added the awaiting-review The author would like community review of the PR label Apr 11, 2022

riccardobrasca reviewed Apr 13, 2022

View reviewed changes

yuma-mizuno added 3 commits April 13, 2022 20:09

rename lemma

fb950fa

separate comm_semiring and comm_ring

152f2aa

golf

f9ccbb2

riccardobrasca reviewed Apr 13, 2022

View reviewed changes

yuma-mizuno added 3 commits April 14, 2022 09:32

rearrange lemmas

a23c973

to reduce implicit arguments

lint style

d053d93

fix

8f2561d

riccardobrasca approved these changes Apr 14, 2022

View reviewed changes

yuma-mizuno added 2 commits April 14, 2022 18:53

fix docs

1eb6cb4

use nontrivial R instead of hnze

54cb6fd

riccardobrasca reviewed Apr 14, 2022

View reviewed changes

yuma-mizuno mentioned this pull request Apr 15, 2022

[Merged by Bors] - feat(ring_theory/localization/basic): generalize to semiring #13459

Closed

1 task

yuma-mizuno added 2 commits April 15, 2022 17:26

fix docs

c1f7aef

update docs for is_local_ring_hom

f563be0

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 15, 2022

bors bot pushed a commit that referenced this pull request Apr 15, 2022

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

d63d9a5

yuma-mizuno added 2 commits April 15, 2022 19:49

Merge branch 'master' into local-semiring

ade415c

fix

b1213a3

bors bot pushed a commit that referenced this pull request Apr 15, 2022

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

2194eef

bors bot changed the title ~~chore(ring_theory/ideal/local_ring): generalize to semirings~~ [Merged by Bors] - chore(ring_theory/ideal/local_ring): generalize to semirings Apr 15, 2022

bors bot closed this Apr 15, 2022

bors bot deleted the local-semiring branch April 15, 2022 17:08

yuma-mizuno mentioned this pull request Apr 15, 2022

[Merged by Bors] - feat(ring_theory/ideal/local_ring): generalize lemmas to semirings #13471

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

yuma-mizuno commented Apr 11, 2022

riccardobrasca Apr 13, 2022

yuma-mizuno Apr 13, 2022

riccardobrasca Apr 13, 2022

yuma-mizuno Apr 14, 2022 •

edited

riccardobrasca Apr 14, 2022

riccardobrasca Apr 13, 2022

yuma-mizuno Apr 13, 2022

riccardobrasca Apr 13, 2022

riccardobrasca commented Apr 13, 2022

riccardobrasca Apr 14, 2022

riccardobrasca Apr 14, 2022

riccardobrasca Apr 14, 2022

riccardobrasca Apr 14, 2022

yuma-mizuno Apr 15, 2022

riccardobrasca Apr 15, 2022

yuma-mizuno Apr 15, 2022

riccardobrasca commented Apr 15, 2022

bors bot commented Apr 15, 2022

yuma-mizuno commented Apr 15, 2022

bors bot commented Apr 15, 2022

yuma-mizuno commented Apr 15, 2022

bors bot commented Apr 15, 2022

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

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

Conversation

yuma-mizuno commented Apr 11, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

yuma-mizuno Apr 14, 2022 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

riccardobrasca commented Apr 13, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

riccardobrasca commented Apr 15, 2022

bors bot commented Apr 15, 2022

yuma-mizuno commented Apr 15, 2022

bors bot commented Apr 15, 2022

yuma-mizuno commented Apr 15, 2022

bors bot commented Apr 15, 2022

yuma-mizuno Apr 14, 2022 •

edited