[Merged by Bors] - feat: algebraic hierarchy on DirectLimit#19893
[Merged by Bors] - feat: algebraic hierarchy on DirectLimit#19893alreadydone wants to merge 12 commits intomasterfrom
Conversation
PR summary 19359074a7Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 4897 | -6 | porting notes |
| 1497 | -1 | erw |
| 223 | 1 | bare open (scoped) Classical |
Current commit 19359074a7
Reference commit 2c66a57507
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
522a6e8 to
71b4ceb
Compare
| /-- This version is primed so that the `RingHomClass` versions aren't. -/ | ||
| theorem map_intCast' [AddGroupWithOne α] [AddGroupWithOne β] [FunLike F α β] |
There was a problem hiding this comment.
Is this not a strict generalization?
There was a problem hiding this comment.
Do you mean map_intCast? That one assumes RingHomClass so there's no need to supply a proof of f 1 = 1. This new lemma is in parallel to map_natCast'.
| /-- The direct limit constructed as a quotient of the direct sum is isomorphic to | ||
| the direct limit constructed as a quotient of the disjoint union. -/ | ||
| def linearEquiv : DirectLimit G f ≃ₗ[R] _root_.DirectLimit G f := |
There was a problem hiding this comment.
So now we have two definitions of DirectLimit, whereas we had only one in the past, right?
One is a bit more general, but the other has better defeqs and is easier to work with. Do I understand that correctly?
I think part of your PR commit message contains useful commentary that should also be embedded in a module docstring in one of these files.
There was a problem hiding this comment.
There were Module.DirectLimit, AddCommGroup.DirectLimit and Ring.DirectLimit, and I'm now adding DirectLimit in the root space. The three existing DirectLimits are in fact constructions of general colimits in the respective categories, while mine is restricted to directed colimits but applies to all kinds of algebraic structures. The point is that when the preorder is directed, the underlying type of all DirectLimits can be taken to be the same, no matter what algebraic structure you consider; in fact I simply take the DirectLimit in Type* and put all kinds of algebraic structures on it. The equivalence relation on that defines the DirectLimit in Type* is easy to understand, and is used to golf the of.zero_exact lemmas.
I'll check what part of the PR message is appropriate to include in the module docstrings.
There was a problem hiding this comment.
Thanks, this message is also very useful. So please also add a version of that info to the module docstring.
There was a problem hiding this comment.
Please check these two commits; is there anything I should add?
e7e2743 to
1935907
Compare
**Order/DirectedInverseSystem.lean**: define the DirectLimit of a DirectedSystem of types as a quotient (by a setoid (equivalence relation)) of the Sigma type (disjoint union). Provide the `induction` lemmas and `map`/`lift` constructions used to define algebraic operations on DirectLimit. New file **Algebra/Colimit/DirectLimit.lean**: the first 400 lines are boilerplate code that defines algebraic instances on DirectLImit from magma (Mul) to Field. To make everything "hom-polymorphic", the DirectedSystem consists of FunLikes rather than plain/unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere. The remaining 70 lines essentially shows that DirectLimit is the colimit in the categories of Module and Ring. **Algebra/DirectLimit.lean**: renamed to **Algebra/Colimit/ModuleRing.lean**. This file was originally added @kckennylau 5 years ago in [mathlib3#754](leanprover-community/mathlib3#754) and defines `Module.DirectLimit` and `Ring.DirectLimit` as quotients of the universal objects (DirectSum and FreeCommRing). This definition is more general and suitable for arbitrary colimits, but makes it very cumbersome to prove [`of.zero_exact`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectLimit.html#Ring.DirectLimit.of.zero_exact) lemmas (130+ lines!); for DirectLimit constructed as quotients of the disjoint union, these are just by definition. We golf these proofs by constructing isomorphisms between `Module/Ring.DirectLimit` and `_root_.DirectLimit`. I have more work done that generalizes most lemmas there to work for arbitrary colimits, that's why I put it under a new Colimit directory. **Data/Int/Cast/Lemmas.lean**: add `map_intCast'` **Data/Nat/Cast/Basic.lean**: golf a lemma **Order/Directed.lean**: add a lemma **ModelTheory/DirectLimit.lean**: change two lemmas to aliases of the general FunLike lemmas
|
Pull request successfully merged into master. Build succeeded: |
**Order/DirectedInverseSystem.lean**: define the DirectLimit of a DirectedSystem of types as a quotient (by a setoid (equivalence relation)) of the Sigma type (disjoint union). Provide the `induction` lemmas and `map`/`lift` constructions used to define algebraic operations on DirectLimit. New file **Algebra/Colimit/DirectLimit.lean**: the first 400 lines are boilerplate code that defines algebraic instances on DirectLImit from magma (Mul) to Field. To make everything "hom-polymorphic", the DirectedSystem consists of FunLikes rather than plain/unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere. The remaining 70 lines essentially shows that DirectLimit is the colimit in the categories of Module and Ring. **Algebra/DirectLimit.lean**: renamed to **Algebra/Colimit/ModuleRing.lean**. This file was originally added @kckennylau 5 years ago in [mathlib3#754](leanprover-community/mathlib3#754) and defines `Module.DirectLimit` and `Ring.DirectLimit` as quotients of the universal objects (DirectSum and FreeCommRing). This definition is more general and suitable for arbitrary colimits, but makes it very cumbersome to prove [`of.zero_exact`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/DirectLimit.html#Ring.DirectLimit.of.zero_exact) lemmas (130+ lines!); for DirectLimit constructed as quotients of the disjoint union, these are just by definition. We golf these proofs by constructing isomorphisms between `Module/Ring.DirectLimit` and `_root_.DirectLimit`. I have more work done that generalizes most lemmas there to work for arbitrary colimits, that's why I put it under a new Colimit directory. **Data/Int/Cast/Lemmas.lean**: add `map_intCast'` **Data/Nat/Cast/Basic.lean**: golf a lemma **Order/Directed.lean**: add a lemma **ModelTheory/DirectLimit.lean**: change two lemmas to aliases of the general FunLike lemmas
Order/DirectedInverseSystem.lean: define the DirectLimit of a DirectedSystem of types as a quotient (by a setoid (equivalence relation)) of the Sigma type (disjoint union). Provide the
inductionlemmas andmap/liftconstructions used to define algebraic operations on DirectLimit.New file Algebra/Colimit/DirectLimit.lean: the first 400 lines are boilerplate code that defines algebraic instances on DirectLImit from magma (Mul) to Field. To make everything "hom-polymorphic", the DirectedSystem consists of FunLikes rather than plain/unbundled functions, and we use algebraic hom typeclasses (e.g. LinearMapClass, RingHomClass) everywhere. The remaining 70 lines essentially shows that DirectLimit is the colimit in the categories of Module and Ring.
Algebra/DirectLimit.lean: renamed to Algebra/Colimit/ModuleRing.lean. This file was originally added @kckennylau 5 years ago in mathlib3#754 and defines
Module.DirectLimitandRing.DirectLimitas quotients of the universal objects (DirectSum and FreeCommRing). This definition is more general and suitable for arbitrary colimits, but makes it very cumbersome to proveof.zero_exactlemmas (130+ lines!); for DirectLimit constructed as quotients of the disjoint union, these are just by definition. We golf these proofs by constructing isomorphisms betweenModule/Ring.DirectLimitand_root_.DirectLimit. I have more work done that generalizes most lemmas there to work for arbitrary colimits, that's why I put it under a new Colimit directory.Data/Int/Cast/Lemmas.lean: add
map_intCast'Data/Nat/Cast/Basic.lean: golf a lemma
Order/Directed.lean: add a lemma
ModelTheory/DirectLimit.lean: change two lemmas to aliases of the general FunLike lemmas