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.
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
Direct limit of modules, abelian groups, rings, and fields. #754
Conversation
Nice! |
What about adding some documentation at the top of the file |
src/ring_theory/free_comm_ring.lean
Outdated
|
||
def free_comm_ring (α : Type u) : Type u := | ||
free_abelian_group $ multiset α | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think this should end up in mathlib. If you feel that strongly about decidability assumptions refactor polynomials.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If I use polynomial instead of this, where should I put the things about supported
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can't really work with mv_polynomial. It is really slow.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The use of free_comm_ring
has been approved in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/free_comm_ring . @ChrisHughes24
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
By "separate PR" do you mean #734?
@ChrisHughes24 do you have other comments? |
@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. |
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) | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hid
and Hcomp
are not great names here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
changed to map_self
and map_map
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. |
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. |
Added docstrings. @sgouezel |
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 |
Doesn't work for fields. |
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. |
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 |
This whole thing still works with a |
@ChrisHughes24 in this comment \up Reid points out that in fact the result hold true in an even greater generality. |
What exactly are the weakest hypotheses necessary to just define |
Just tried getting rid of it, and I probably can't. |
…b into direct_limit
src/ring_theory/free_comm_ring.lean
Outdated
-/ | ||
|
||
import group_theory.free_abelian_group data.equiv.algebra data.equiv.functor data.polynomial | ||
import data.real.irrational |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For what do we need this file? It seems like a surprising import to me.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's part of a clever proof of is_supported_of {p} {s : set α} : is_supported (of p) s ↔ p ∈ s
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some comments, more will follow later.
src/ring_theory/free_comm_ring.lean
Outdated
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) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it make sense to call this is_supported_mono
?
|
||
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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe add is_supported_pow
.
@[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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
restriction
is a ring hom. Also, you could add simp
-lemmas for restriction_int
and restriction_pow
.
src/ring_theory/free_comm_ring.lean
Outdated
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, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
.
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, |
{ 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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sweet proof (-;
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
/-- 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
See #118.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list