chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal` #13175

xroblot · 2024-05-24T16:41:54Z

This PR adds a new file RingTheory.Ideal.IsPrincipal and moves most of the (basic) results about Ideal.IsPrincipal and Ideal.span_singleton from Ideal.Basic and Ideal.Operations to this file. (Some very basic results or results related to Submodule.span_singleton are left in place.)

The need for this PR comes from a discussion in #12780 about where to put the proof that the equivalence between principal ideals and associates is actually a MulEquiv (#13177).

Some remarks:

no_lost_declarations.sh says

* 25  added declarations
* 25  removed declarations
* 5  paired declarations

this is due to some renames in the variables and also namespace changes. I have checked that the added declarations correspond exactly to the removed declarations

Some results that could not stay in Ideal.Basic but are not really related to principal ideals have been moved (for the moment?) to the end of Ideal.IsPrincipal (see the misc section). I thought about putting them in Ideal.Operations but the file is already quite large (about 1400 lines). Note that Ideal.Operations imports Ideal.IsPrincipal and these additional results do not add any extra import to Ideal.IsPrincipal. Still, they should probably go somewhere else...

faenuccio · 2024-05-24T18:18:05Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

@@ -0,0 +1,299 @@
+/-
+Copyright (c) 2018 Kenny Lau. All rights reserved.


Is this copyright correct?

Well, that's what I did in my previous splits: just copy the copyright of the original file. I am not sure it is the best way to proceed but, well, that's the only one I know...

faenuccio · 2024-05-24T18:18:47Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+
+/-!
+# Principal Ideals
+-/


Do we want a small list of the principal results? Also, perhaps, a couple of words about what is what (i.e. in the whole file R is a semiring, sometimes supposed to be a ring...)

faenuccio · 2024-05-24T18:19:10Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+variable [Semiring R]
+
+@[simp]
+theorem zero_eq_bot : (0 : Ideal R) = ⊥ :=


This could stay in Basic no? EDIT It was actually in Operation but Basic seems more appropriate.

Yes, it was in Operations. I moved it here because I need it here and, after all, zero is a principal ideal. It cannot be in Basic because of imports and I don't want to change Basic imports.

I think this can go under Submodule.zero_eq_bot?

Okay after reading the remaining of the file, maybe add a new file RingTheory/Ideal/Lattice?

Yeah, I think I'm going to put this PR on hold. There is first a need to split Operations into several smaller files first for this to work.

faenuccio · 2024-05-24T18:19:33Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+open Submodule Set
+
+@[simp]
+theorem one_eq_top : (1 : Ideal R) = ⊤ := by erw [Submodule.one_eq_range, LinearMap.range_id]


This could remain in Basic, I think.

This is the same as above

faenuccio · 2024-05-24T18:21:01Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+        (mul_dvd_mul_iff_left h₁).1 <| by rwa [mul_one, ← Ideal.span_singleton_le_span_singleton]
+#align ideal.factors_decreasing Ideal.factors_decreasing
+
+lemma Ideal.isPrime_of_maximally_disjoint  [CommSemiring R] (I : Ideal R) (S : Submonoid R)


Why has this been moved here?

As I mentioned in the description, a certain number of results could not stay in Basic since they depend on results that have been moved to IsPrincipal. For the moment, I moved those results to IsPrincipal as a temporary solution (in the misc section). I could put these results in Operations but the file is already quite big so I am not sure it's the best way to proceed. I welcome any suggestions on what to do with those...

faenuccio · 2024-05-24T18:21:09Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+    rw [← hr₁, ← hr₂]
+    ring
+
+theorem Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top [CommSemiring R] [Nontrivial R] :


(Same as above)

faenuccio · 2024-05-24T18:21:19Z

Mathlib/RingTheory/Ideal/IsPrincipal.lean

+    exact lt_top (I.mul_mem_right _ mem)
+#align ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top
+
+theorem Ring.not_isField_iff_exists_prime [CommSemiring R] [Nontrivial R] :


Once more... why here?

(Same as above)

faenuccio

I was all in favour of creating this new file, and so of course this PR looks very good to me. I wonder why many lemmas about prime/maximal ideals ended up in the IsPrincipal one although they do not have anything to do with principality, AFAICT.

…rincipal_step1

xroblot · 2024-05-25T13:51:21Z

Well, I think I am going to close this PR. I do not think into possible to put everything about IsPrincipal in a single file before a major refactor of Operations has been done.

xroblot added 4 commits May 24, 2024 18:30

1st commit

42fb9f8

Remove new results

1488f65

Add docstring

f0a5a73

Add misc section

e456090

xroblot mentioned this pull request May 24, 2024

[Merged by Bors] - feat: add a version of Ideal.associatesEquivIsPrincipal for generators that are non-zero-divisors #12780

Closed

3 tasks

xroblot changed the title ~~chore(RingTheory/Ideal): add Ideal.IsPrincipal~~ chore(RingTheory/Ideal): add new file Ideal.IsPrincipal May 24, 2024

xroblot added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels May 24, 2024

xroblot mentioned this pull request May 24, 2024

[Merged by Bors] - feat(Ideal.IsPrincipal): Prove that the equiv between principal ideals and associates is a MulEquiv #13177

Closed

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 24, 2024

faenuccio reviewed May 24, 2024

View reviewed changes

xroblot added 2 commits May 25, 2024 09:06

Merge remote-tracking branch 'origin/master' into xfr-split_ideal_isp…

f922b0b

…rincipal_step1

Shake

c92a835

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 25, 2024

github-actions bot removed the awaiting-CI label May 25, 2024

xroblot added WIP Work in progress and removed awaiting-review labels May 25, 2024

xroblot closed this May 25, 2024

xroblot deleted the xfr-split_ideal_isprincipal_step1 branch June 3, 2024 16:41

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal` #13175

chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal` #13175

xroblot commented May 24, 2024 •

edited

Loading

faenuccio May 24, 2024

xroblot May 25, 2024

faenuccio May 24, 2024

faenuccio May 24, 2024 •

edited

Loading

xroblot May 25, 2024

erdOne May 25, 2024

erdOne May 25, 2024

xroblot May 25, 2024

faenuccio May 24, 2024

xroblot May 25, 2024

faenuccio May 24, 2024

xroblot May 25, 2024

faenuccio May 24, 2024

xroblot May 25, 2024

faenuccio May 24, 2024

xroblot May 25, 2024

faenuccio left a comment

xroblot commented May 25, 2024

		@@ -0,0 +1,299 @@
		/-
		Copyright (c) 2018 Kenny Lau. All rights reserved.

chore(RingTheory/Ideal): add new file Ideal.IsPrincipal #13175

chore(RingTheory/Ideal): add new file Ideal.IsPrincipal #13175

Conversation

xroblot commented May 24, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

faenuccio May 24, 2024 • edited Loading

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

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

faenuccio left a comment

Choose a reason for hiding this comment

xroblot commented May 25, 2024

chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal` #13175

chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal` #13175

xroblot commented May 24, 2024 •

edited

Loading

faenuccio May 24, 2024 •

edited

Loading