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

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 <[email protected]>

…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 <[email protected]>

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

Pull request successfully merged into master.

Build succeeded:

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 to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (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 <[email protected]>

Turn rfl into with_reducible_and_instances rfl

540b773

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

5f65e81

…anyway

leanprover-community-mathlib4-bot 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 commented Jan 17, 2025 •

edited by mattrobball

Loading

github-actions bot commented Jan 17, 2025 •

edited

Loading

Declarations diff

Vierkantor Jan 17, 2025

Vierkantor Jan 17, 2025

Vierkantor Jan 17, 2025

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

mattrobball commented Jan 17, 2025

mathlib-bors bot commented Jan 17, 2025

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

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

Conversation

Vierkantor commented Jan 17, 2025 • edited by mattrobball Loading

github-actions bot commented Jan 17, 2025 • edited Loading

PR summary 5f65e81a6b

Import changes for modified files

Declarations diff

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

Vierkantor Jan 17, 2025

Choose a reason for hiding this comment

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

mattrobball commented Jan 17, 2025

mathlib-bors bot commented Jan 17, 2025

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

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

Vierkantor commented Jan 17, 2025 •

edited by mattrobball

Loading

github-actions bot commented Jan 17, 2025 •

edited

Loading