[Merged by Bors] - feat(CategoryTheory): define unbundled `ConcreteCategory` class by Vierkantor · Pull Request #20810 · leanprover-community/mathlib4

Vierkantor · 2025-01-17T13:23:14Z

This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980

This PR defines a new class ConcreteCategory that unbundles the coercion of morphisms to functions and objects to types, in order to allow ConcreteCategory to coexist alongisde existing coercions to functions/sorts. No instances are included yet, since those can be declared in parallel. See e.g. CommRingCat on the redesign-ConcreteCategory branch for examples of what a concrete category instance will end up looking like.

depends on: [Merged by Bors] - chore(CategoryTheory): rename ConcreteCategory to HasForget #20809

github-actions · 2025-01-17T13:24:07Z

PR summary 5f65e81a6b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ConcreteCategory.forget_map_eq_coe
+ HasForget.toConcreteCategory
+ HasForget.toFunLike
+ ToHom
+ ToType
+ Types.instConcreteCategory
+ Types.instFunLike
+ coe_ext
+ congr_arg
+ congr_fun
+ ext
+ ext_apply
+ forget_eq_ConcreteCategory_hom
+ forget_obj
+ homEquiv
+ hom_bijective
+ hom_comp
+ hom_id
+ hom_injective
+ instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ ToType X → ToType Y)
+ toHasForget

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.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Vierkantor · 2025-01-17T13:28:57Z

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

+They are specified that order, to avoid unnecessary universe annotations.
+-/
+class ConcreteCategory (C : Type u) [Category.{v} C]
+    (FC : outParam <| C → C → Type*) {CC : outParam <| C → Type w}


I noticed that CC can always be inferred through unification in the FunLike instance. So for conciseness I made it implicit. I was not expecting that to be possible!

Vierkantor · 2025-01-17T13:31:27Z

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

+/-- `ToType X` converts the object `X` of the concrete category `C` to a type.
+
+This is an `abbrev` so that instances on `X` (e.g. `Ring`) do not need to be redeclared.
+-/
+abbrev ToType [ConcreteCategory C FC] := CC
+
+/-- `ToHom X Y` is the type of (bundled) functions between objects `X Y : C`.
+
+This is an `abbrev` so that instances (e.g. `RingHomClass`) do not need to be redeclared.
+-/
+abbrev ToHom [ConcreteCategory C FC] := FC


We could also leave out ToType and ToHom and write CC/FC everywhere. I think this is neater, making things look like coercions. By defining this as abbrev, we don't commit (on the elaboration/tactic side) to a specific notation.

Vierkantor · 2025-01-17T13:35:54Z

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

+  hom_bijective.injective
+
+/-- In any concrete category, we can test equality of morphisms by pointwise evaluations. -/
+@[ext] lemma ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=


This is a replacement for hom_ext, that currently is defined in terms of HasForget. (Similarly for congr_fun, congr_arg, hom_id and hom_comp below.) Since we have no ConcreteCategory instances yet, we'll unfortunately need to keep both spellings for a while. At some point we'll also have to decide which name is nicer :)

mathlib4-dependent-issues-bot · 2025-01-17T14:20:37Z

This PR/issue depends on:

~~[Merged by Bors] - chore(CategoryTheory): rename ConcreteCategory to HasForget #20809~~
By Dependent Issues (🤖). Happy coding!

This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR defines a new class `ConcreteCategory` that unbundles the coercion of morphisms to functions and objects to types, in order to allow `ConcreteCategory` to coexist alongisde existing coercions to functions/sorts. No instances are included yet, since those can be declared in parallel. See e.g. `CommRingCat` on the `redesign-ConcreteCategory` branch for examples of what a concrete category instance will end up looking like.

…tion

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

…anyway

mattrobball · 2025-01-17T15:43:19Z

bors merge

This is a step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 This PR defines a new class `ConcreteCategory` that unbundles the coercion of morphisms to functions and objects to types, in order to allow `ConcreteCategory` to coexist alongisde existing coercions to functions/sorts. No instances are included yet, since those can be declared in parallel. See e.g. `CommRingCat` on the `redesign-ConcreteCategory` branch for examples of what a concrete category instance will end up looking like. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

mathlib-bors · 2025-01-17T16:00:07Z

Pull request successfully merged into master.

Build succeeded:

* polynomial-sequences: (149 commits) Aha, here's how to get Lean to stop showing S.elems' in the infoview. Try satisfying the linter gods again. Probably enough initial tidying to send the PR. Kill more temporary names. Touch more natDegree. Does protected satisfy the docstring linter? Bit shorter. More Quiet linters. Remove redundant imports. Copyright header and more twiddling. Rename lemma to 'degree_smul_of_leadingCoeff_rightRegular' and split out feat(Polynomial): polynomial sequences are bases for R[X] chore(Dynamics/PeriodicPts): don't import `MonoidWithZero` (#20765) chore(Associated): split out `Ring` results (#20737) feat(AlgebraicGeometry): flat morphisms of schemes (#19790) feat(AlgebraicGeometry): scheme-theoretic fibre (#19427) chore: split Mathlib.Analysis.Asymptotics.Asymptotics (#20785) doc: typo (#20829) feat(CategoryTheory): condition for an induced functor between comma categories to be final (#20139) feat(1000.yaml): allow statements of theorems also (#20637) feat(Algebra/Homology/Embedding): homology of truncGE' (#19570) chore: cleanup many porting notes in Combinatorics (#20823) chore: eliminate porting notes about `deriving Fintype` (#20820) feat(Algebra/Lie): a Lie algebra is solvable iff it is solvable after faithfully flat base change (#20808) feat: define bases of root pairings (#20667) feat(Tactic): basic ConcreteCategory support for elementwise (#20811) feat(CategoryTheory): define unbundled `ConcreteCategory` class (#20810) chore(CategoryTheory): rename `ConcreteCategory` to `HasForget` (#20809) feat: `CommSemiring (NonemptyInterval ℚ≥0)` (#20783) chore(yaml_check.py): re-format (#20807) feat: elementary estimate for Real.log (#20766) feat: definition of linear topologies (#14990) feat(RingTheory): flatness over a semiring (#19115) feat(Algebra/Homology/Embedding): the canonical truncation truncLE (#19550) feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex (#19203) feat(Algebra/Ring): `RingEquiv.piUnique` (#20794) feat(RingTheory/LocalRing): add instance `Unique (MaximalSpectrum R)` for a local ring `R` (#20801) chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) chore: restore `def` to `adicCompletion` (#20796) refactor: rename `UniqueContinuousFunctionalCalculus` to `ContinuousMap.UniqueHom` (#20643) feat(Algebra/Homology/Embedding): the morphism from a complex to its `truncGE` truncation (#19544) chore(Mathlib/Computability/TuringMachine): split file (#20790) feat(Data/Finset/Card): add `InjOn` and `SurjOn` versions of finset cardinality lemmas (#20753) feat(Order/WellFoundedSet): add convenience constructors for IsWF and IsPWO for WellFoundedLT types (#20752) feat(Set/Finite): a set is finite if its image and fibers are finite (#20751) chore: cleanup .gitignore files (#20795) feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) feat(Combinatorics/SimpleGraph): vertices in cycles (#20602) CI: merge `bot_fix_style` actions (#20789) ...

Vierkantor added the t-category-theory Category theory label Jan 17, 2025

Vierkantor commented Jan 17, 2025

View reviewed changes

Vierkantor mentioned this pull request Jan 17, 2025

[Merged by Bors] - feat(Tactic): basic ConcreteCategory support for elementwise #20811

Closed

1 task

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 17, 2025

Vierkantor added 3 commits January 17, 2025 15:27

For some reason, simp started working here again?

a445d24

nolint the unused argument in ToHom/ToFun: it is used for unifica…

dff99eb

…tion

Vierkantor force-pushed the redefine-ConcreteCategory branch from 7b4be55 to dff99eb Compare January 17, 2025 14:27

mattrobball reviewed Jan 17, 2025

View reviewed changes

Vierkantor and others added 3 commits January 17, 2025 16:35

whitespace

5dc1dba

Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

Turn rfl into with_reducible_and_instances rfl

540b773

Can remove these local instances, they're mentioned explicitly below …

5f65e81

…anyway

ghost added the ready-to-merge This PR has been sent to bors. label Jan 17, 2025

mathlib-bors bot changed the title ~~feat(CategoryTheory): define unbundled ConcreteCategory class~~ [Merged by Bors] - feat(CategoryTheory): define unbundled ConcreteCategory class Jan 17, 2025

mathlib-bors bot closed this Jan 17, 2025

mathlib-bors bot deleted the redefine-ConcreteCategory branch January 17, 2025 16:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(CategoryTheory): define unbundled `ConcreteCategory` class #20810

[Merged by Bors] - feat(CategoryTheory): define unbundled `ConcreteCategory` class #20810
Vierkantor wants to merge 6 commits intomasterfrom
redefine-ConcreteCategory

Vierkantor commented Jan 17, 2025 •

edited by mattrobball

Loading

Uh oh!

github-actions bot commented Jan 17, 2025 •

edited

Loading

Declarations diff

Uh oh!

Vierkantor Jan 17, 2025

Uh oh!

Vierkantor Jan 17, 2025

Uh oh!

Vierkantor Jan 17, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jan 17, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mattrobball commented Jan 17, 2025

Uh oh!

mathlib-bors bot commented Jan 17, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

Vierkantor commented Jan 17, 2025 • edited by mattrobball Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5f65e81a6b

Import changes for modified files

Declarations diff

Uh oh!

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib4-dependent-issues-bot commented Jan 17, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mattrobball commented Jan 17, 2025

Uh oh!

mathlib-bors bot commented Jan 17, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Vierkantor commented Jan 17, 2025 •

edited by mattrobball

Loading

github-actions bot commented Jan 17, 2025 •

edited

Loading