Direct limit of modules, abelian groups, rings, and fields. by kckennylau · Pull Request #754 · leanprover-community/mathlib3

kckennylau · 2019-02-23T18:59:36Z

See #118.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

ChrisHughes24 · 2019-02-23T19:59:36Z

Nice!

sgouezel · 2019-02-23T21:04:40Z

What about adding some documentation at the top of the file direct_limit.lean, and comments and docstrings in the file itself about the contents of the definitions, statements, and design decisions? And yes, very nice indeed!

ChrisHughes24 · 2019-02-23T21:37:59Z

src/ring_theory/free_comm_ring.lean

+
+def free_comm_ring (α : Type u) : Type u :=
+free_abelian_group $ multiset α
+


I don't think this should end up in mathlib. If you feel that strongly about decidability assumptions refactor polynomials.

If I use polynomial instead of this, where should I put the things about supported?

I can't really work with mv_polynomial. It is really slow.

The use of free_comm_ring has been approved in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/free_comm_ring . @ChrisHughes24

I'd prefer that this part is in a separate PR, but if Chris knows what's going on here I'm fine with him making the call.

By "separate PR" do you mean #734?

kckennylau · 2019-02-23T23:37:42Z

@ChrisHughes24 do you have other comments?

kckennylau · 2019-02-24T00:06:27Z

@sgouezel I don't really know what doc-strings to add. They are all standard facts about direct limits that one can find in e.g. Atiyah-Mcdonald.

ChrisHughes24 · 2019-02-24T00:07:29Z

src/algebra/direct_limit.lean

+class directed_system (f : Π i j, i ≤ j → G i →ₗ[R] G j) : Prop :=
+(Hid : ∀ i x h, f i i h x = x)
+(Hcomp : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x)
+


Hid and Hcomp are not great names here.

changed to map_self and map_map

src/algebra/direct_limit.lean

sgouezel · 2019-02-24T08:50:17Z

Sure it's standard material, but think of someone who doesn't know Atiyah-Mcdonald and reads a theory where there is one of your lemmas. Hovering on the lemma, it is always good to have a docstring explaining the content of the lemma for ignorant people. And then, if he clicks on your lemma and gets to your file, it would be good if he could understand what you are doing in this file without having to go to the library or to libgen. A general rule when you write mathematics (not specific to Lean): don't expect your reader to know as much as you do!

Also, there are several equivalent definitions of direct limits. You have chosen one using the universal objects and quotienting but there are also more constructive definitions (like, just take a quotient of the disjoint union under the natural equivalence relation, and check that it is a group/module/whatever). You can say explicitly why you favor the definition you used.

kim-em · 2019-02-24T09:27:27Z

It might even be nice to include references to the corresponding facts in Atiyah & MacDonald in the docstrings? Now that we're starting to get past undergraduate material, I think docstrings and references are more and more important.

kckennylau · 2019-02-24T14:02:56Z

Added docstrings. @sgouezel

rwbarton · 2019-02-24T15:04:01Z

These constructions (except for fields) actually work for arbitrary colimits in modules/abelian groups/rings/any category of models of an algebraic theory. It's only some of the theorems like "an element is zero iff it's zero at some point in the system" which need the directed hypothesis (actually filtered).

Also, you should use the category theory library to do category theory! Compare https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/types.lean#L49-L59 or https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/instances/topological_spaces.lean#L58-L74. It's the equivalent of direct_limit, the instances, of, of_f, lift, lift_of, lift_unique.

kckennylau · 2019-02-24T15:12:46Z

Doesn't work for fields.

rwbarton · 2019-02-24T15:53:47Z

What doesn't work for fields exactly? The limits library has been set up so that you can talk about the colimits of diagrams of certain shapes without requiring the category to have all colimits, precisely because there are lots of cases like this one where we only have colimits of filtered diagrams, or finite coproducts, etc. See https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/limits.lean#L454.

kckennylau · 2019-02-24T16:28:50Z

Ignore my comment about fields.

The last time I tried your colimit thing in category theory, I couldn't define the "shifting the index by one" endomorphism of \bigoplus_{i=1}^\infty X.

ChrisHughes24 · 2019-03-29T17:45:35Z

This whole thing still works with a directed_preorder assumption instead of a directed partial order.

jcommelin · 2019-03-29T17:58:55Z

These constructions (except for fields) actually work for arbitrary colimits in modules/abelian groups/rings/any category of models of an algebraic theory. It's only some of the theorems like "an element is zero iff it's zero at some point in the system" which need the directed hypothesis (actually filtered).

Also, you should use the category theory library to do category theory! Compare https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/limits/types.lean#L49-L59 or https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/instances/topological_spaces.lean#L58-L74. It's the equivalent of direct_limit, the instances, of, of_f, lift, lift_of, lift_unique.

@ChrisHughes24 in this comment \up Reid points out that in fact the result hold true in an even greater generality.

ChrisHughes24 · 2019-03-30T22:42:56Z

What exactly are the weakest hypotheses necessary to just define of for fields. Can I get rid of map_map : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x?

ChrisHughes24 · 2019-03-30T22:49:54Z

Just tried getting rid of it, and I probably can't. ring still works though.

src/algebra/direct_limit.lean

…b into direct_limit

jcommelin · 2019-05-30T12:52:18Z

src/ring_theory/free_comm_ring.lean

 -/

 import group_theory.free_abelian_group data.equiv.algebra data.equiv.functor data.polynomial
+import data.real.irrational


For what do we need this file? It seems like a surprising import to me.

It's part of a clever proof of is_supported_of {p} {s : set α} : is_supported (of p) s ↔ p ∈ s

jcommelin

Some comments, more will follow later.

jcommelin · 2019-05-31T04:30:44Z

src/ring_theory/free_comm_ring.lean

+def is_supported (x : free_comm_ring α) (s : set α) : Prop :=
+x ∈ ring.closure (of '' s)
+
+theorem is_supported_upwards {x : free_comm_ring α} {s t} (hs : is_supported x s) (hst : s ⊆ t) :


Would it make sense to call this is_supported_mono?

jcommelin · 2019-05-31T04:31:23Z

src/ring_theory/free_comm_ring.lean

+
+theorem is_supported_mul {x y : free_comm_ring α} {s} (hxs : is_supported x s) (hys : is_supported y s) :
+  is_supported (x * y) s :=
+is_submonoid.mul_mem hxs hys


Maybe add is_supported_pow.

jcommelin · 2019-05-31T04:35:18Z

src/ring_theory/free_comm_ring.lean

+@[simp] lemma restriction_neg : restriction s (-x) = -restriction s x := lift_neg _ _
+@[simp] lemma restriction_sub : restriction s (x - y) = restriction s x - restriction s y := lift_sub _ _ _
+@[simp] lemma restriction_mul : restriction s (x * y) = restriction s x * restriction s y := lift_mul _ _ _
+end restriction


restriction is a ring hom. Also, you could add simp-lemmas for restriction_int and restriction_pow.

jcommelin · 2019-05-31T04:41:45Z

src/ring_theory/free_comm_ring.lean

+suffices is_supported (of p) s → p ∈ s, from ⟨this, λ hps, ring.subset_closure ⟨p, hps, rfl⟩⟩,
+assume hps : is_supported (of p) s, begin
+  classical,
+  have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ q, if q ∈ s then 0 else real.sqrt 2) x = ↑q,


The type of q in λ q, if q ∈ s is alpha, and not Q. That might be confusing. I suggest we call it a or y.

Suggested change

have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ q, if q ∈ s then 0 else real.sqrt 2) x = ↑q,

have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ a, if a ∈ s then 0 else real.sqrt 2) x = ↑q,

jcommelin · 2019-05-31T04:51:51Z

src/ring_theory/free_comm_ring.lean

+    { rintros x y ⟨q, hq⟩ ⟨r, hr⟩, refine ⟨q+r, _⟩, rw [lift_add, hq, hr, rat.cast_add] } },
+  specialize this (of p) hps, rw [lift_of] at this, split_ifs at this, { exact h },
+  exfalso, exact irr_sqrt_two this
+end


Sweet proof (-;

jcommelin · 2019-05-31T14:24:15Z

src/algebra/direct_limit.lean

+variables [directed_order ι] [decidable_eq ι]
+variables (G : ι → Type w) [Π i, decidable_eq (G i)]
+
+/-- A directed system is a functor from the category (directed poset) to another category.


Suggested change

/-- A directed system is a functor from the category (directed poset) to another category.

/-- A directed system is a functor from a category (directed poset) to another category.

…er-community#754) * stuff * stuff * more stuff * pre merge commit * prove of_zero.exact * remove silly rewrite * slightly shorten proof * direct limit of modules * upgrade mathlib * direct limit of rings * direct limit of fields (WIP) * trying to prove zero_exact for rings * use sqrt 2 instead of F4 * direct limit of field * cleanup for mathlib * remove ununsed lemmas * clean up * docstrings * local * fix build * Replace real with polynomial int in proof * Update basic.lean

kckennylau and others added 16 commits February 23, 2019 10:35

stuff

fe03e76

stuff

4b68946

more stuff

696a984

pre merge commit

3667544

prove of_zero.exact

9ad20fc

remove silly rewrite

6ddf081

slightly shorten proof

84ada9f

direct limit of modules

c752316

upgrade mathlib

88caa1c

direct limit of rings

ce09a3c

direct limit of fields (WIP)

8fbae04

trying to prove zero_exact for rings

0617fd9

use sqrt 2 instead of F4

5b578ee

direct limit of field

cf8a619

cleanup for mathlib

5c0258a

remove ununsed lemmas

f2be1d5

ChrisHughes24 reviewed Feb 23, 2019

View reviewed changes

ChrisHughes24 reviewed Feb 24, 2019

View reviewed changes

clean up

83542ff

cipher1024 assigned ChrisHughes24 Feb 24, 2019

docstrings

c01e2df

Merge branch 'master' into direct_limit

681e886

ChrisHughes24 reviewed Apr 24, 2019

View reviewed changes

src/algebra/direct_limit.lean Outdated Show resolved Hide resolved

kckennylau added 2 commits May 25, 2019 16:49

local

2e99aa3

Merge branch 'direct_limit' of github.com:leanprover-community/mathli…

687bf3d

…b into direct_limit

kckennylau requested a review from a team as a code owner May 25, 2019 16:14

jcommelin and others added 2 commits May 30, 2019 07:19

Merge branch 'master' into direct_limit

f05191d

fix build

3d8a480

jcommelin reviewed May 30, 2019

View reviewed changes

jcommelin reviewed May 31, 2019

View reviewed changes

Replace real with polynomial int in proof

85937c6

jcommelin reviewed May 31, 2019

View reviewed changes

Update basic.lean

322c273

ChrisHughes24 approved these changes Jun 16, 2019

View reviewed changes

ChrisHughes24 added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jun 16, 2019

Merge branch 'master' into direct_limit

02443bb

mergify bot merged commit 7b715eb into master Jun 16, 2019

mergify bot deleted the direct_limit branch June 16, 2019 19:29

This was referenced Dec 9, 2024

refactor(Algebra/DirectLimit): change definition to quotient of Sigma type leanprover-community/mathlib4#19772

Closed

[Merged by Bors] - feat: algebraic hierarchy on DirectLimit leanprover-community/mathlib4#19893

Closed


		def free_comm_ring (α : Type u) : Type u :=
		free_abelian_group $ multiset α

	have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ q, if q ∈ s then 0 else real.sqrt 2) x = ↑q,
	have : ∀ x, is_supported x s → ∃ q : ℚ, lift (λ a, if a ∈ s then 0 else real.sqrt 2) x = ↑q,

	/-- A directed system is a functor from the category (directed poset) to another category.
	/-- A directed system is a functor from a category (directed poset) to another category.

Conversation

kckennylau commented Feb 23, 2019

Uh oh!

ChrisHughes24 commented Feb 23, 2019

Uh oh!

sgouezel commented Feb 23, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kckennylau Feb 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

kckennylau commented Feb 23, 2019

Uh oh!

kckennylau commented Feb 24, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel commented Feb 24, 2019

Uh oh!

kim-em commented Feb 24, 2019

Uh oh!

kckennylau commented Feb 24, 2019

Uh oh!

rwbarton commented Feb 24, 2019

Uh oh!

kckennylau commented Feb 24, 2019

Uh oh!

rwbarton commented Feb 24, 2019

Uh oh!

kckennylau commented Feb 24, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ChrisHughes24 commented Mar 29, 2019

Uh oh!

jcommelin commented Mar 29, 2019

Uh oh!

ChrisHughes24 commented Mar 30, 2019

Uh oh!

ChrisHughes24 commented Mar 30, 2019

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

kckennylau Feb 24, 2019 •

edited

Loading

kckennylau commented Feb 24, 2019 •

edited

Loading