Conversation
….uliftPreservesColimits
PR summary 1abc6e6424Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Category.Grp.Ulift | 827 | 1511 | +684 (+82.71%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Category.Grp.Ulift |
684 |
Declarations diff
+ Quot.desc_quotQuotUliftAddEquiv
+ instance : CreatesColimitsOfSize.{w, u} uliftFunctor.{v, u}
+ instance : PreservesColimitsOfSize.{w', w} uliftFunctor.{v, u}
+ quotQuotUliftAddEquiv
+ quotToQuotUlift
+ quotToQuotUlift_ι
+ quotUliftToQuot
+ quotUliftToQuot_ι
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (3.00, 0.00)
| Current number | Change | Type |
|---|---|---|
| 1417 | 3 | erw |
Current commit 1abc6e6424
Reference commit 1b34e3c465
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).
|
This is a very nice result. In the case of colimits of types, with Markus Himmel, we had used a kind of similar argument, where It would be great if you could refactor the file |
#20474 for the first step. |
|
Wouldn't it also make sense to rewrite |
I did it as a warmup for groups: #20508 |
|
#20512 does another necessary step, the fact that a morphism of abelian groups is bijective if and only the dual morphism between |
|
And we're done! I updated the proof here to use the lemmas in |
…mmutative additive groups preserves colimits (#20417) Prove that the functor `AddCommGrp.ulift` preserves all colimits, hence creates small colimits. (This also finished the proof that it is an exact functor.) Method: Suppose that we have a functor `K : J ⥤ AddCommGrp.{u}` (with `J` any category), a colimit cocone `c` of `K` and a cocone `lc` of `K ⋙ uliftFunctor.{u v}`. We want to construct a morphism of cocones `uliftFunctor.mapCocone c → lc` witnessing the fact that `uliftFunctor.mapCocone c` is also a colimit cocone, but we have no direct way to do this. The idea is to use that `AddCommGrp.{max v u}` has a small cogenerator, which is just the additive (rational) circle `ℚ / ℤ`, so any abelian group of any size can be recovered from its morphisms into `ℚ / ℤ`. More precisely, the functor sending an abelian group `A` to its dual `A →+ ℚ / ℤ` is fully faithful, *if* we consider the dual as a (right) module over the endomorphism ring of `ℚ / ℤ`. So an abelian group `C` is totally determined by the restriction of the coyoneda functor `A ↦ (C →+ A)` to the category of abelian groups at a smaller universe level. We do not develop this totally here but do a direct construction. Every time we have a morphism from `lc.pt` into `ℚ / ℤ`, or more generally into any small abelian group `A`, we can construct a cocone of `K ⋙ uliftFunctor` by sticking `ULift A` at the cocone point (this is `CategoryTheory.Limits.Cocone.extensions`), and this cocone is actually made up of `u`-small abelian groups, hence gives a cocone of `K`. Using the universal property of `c`, we get a morphism `c.pt →+ A`. So we have constructed a map `(lc.pt →+ A) → (c.pt →+ A)`, and it is easy to prove that it is compatible with postcomposition of morphisms of small abelian groups. To actually get the morphism `c.pt →+ lc.pt`, we apply this to the canonical embedding of `lc.pt` into `Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` (this group is not small but is a product of small groups, so our construction extends). To show that the image of `c.pt` in this product is contained in that of `lc.pt`, we use the compatibility with postcomposition and the fact that we can detect elements of the image just by applying morphisms from `Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ` to `ℚ / ℤ`. - [x] depends on: #20416 - [x] depends on: #20512 - [x] depends on: #20522
|
Pull request successfully merged into master. Build succeeded: |
Prove that the functor
AddCommGrp.uliftpreserves all colimits, hence creates small colimits. (This also finished the proof that it is an exact functor.)Method: Suppose that we have a functor
K : J ⥤ AddCommGrp.{u}(withJany category), acolimit cocone
cofKand a coconelcofK ⋙ uliftFunctor.{u v}. We want toconstruct a morphism of cocones
uliftFunctor.mapCocone c → lcwitnessing the factthat
uliftFunctor.mapCocone cis also a colimit cocone, but we have no direct wayto do this. The idea is to use that
AddCommGrp.{max v u}has a small cogenerator,which is just the additive (rational) circle
ℚ / ℤ, so any abelian group ofany size can be recovered from its morphisms into
ℚ / ℤ. More precisely, the functorsending an abelian group
Ato its dualA →+ ℚ / ℤis fully faithful, if we considerthe dual as a (right) module over the endomorphism ring of
ℚ / ℤ. So an abeliangroup
Cis totally determined by the restriction of the coyonedafunctor
A ↦ (C →+ A)to the category of abelian groups at a smaller universe level.We do not develop this totally here but do a direct construction. Every time we have
a morphism from
lc.ptintoℚ / ℤ, or more generally into any small abelian groupA, we can construct a cocone ofK ⋙ uliftFunctorby stickingULift Aat thecocone point (this is
CategoryTheory.Limits.Cocone.extensions), and this cocone isactually made up of
u-small abelian groups, hence gives a cocone ofK. Usingthe universal property of
c, we get a morphismc.pt →+ A. So we have constructeda map
(lc.pt →+ A) → (c.pt →+ A), and it is easy to prove that it is compatible withpostcomposition of morphisms of small abelian groups. To actually get the
morphism
c.pt →+ lc.pt, we apply this to the canonical embedding oflc.ptintoΠ (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤ(this group is not small but is a product of smallgroups, so our construction extends). To show that the image of
c.ptin this productis contained in that of
lc.pt, we use the compatibility with postcomposition and thefact that we can detect elements of the image just by applying morphisms from
Π (_ : lc.pt →+ ℚ / ℤ), ℚ / ℤtoℚ / ℤ.