Fixing the `erw` hell around concrete categories

Stream: mathlib4

[Anne Baanen]

It seems that unification hints can help us solve quite a bit of erw hell in the category theory area of the library: #17583 But it's failing in a few places because CommRingCat is getting unfolded to Bundled CommRing when it shouldn't. Anyone have ideas how to fix the regressions?

More details: We have a lot of erws and rfls in files dealing with concrete categories. This seems to be mostly due to the existence of two casts: ConcreteCategory.hasCoeToSort and Bundled.coeSort which both represent the forgetful functor from concrete categories to Type. The first is only a local instance but is needed to state lemmas on these concrete categories, while the second one is always available but only applies to categories defined as Bundled. The casts are defeq but not reducibly so, causing issues when rewriting with generic lemmas in the context of a specific Bundled category.

For some specific categories we already have a workaround by @Kim Morrison: a unification hint of the form ⊢ (forget CommRingCat).obj R ≟ R also fires at reducible transparency. Adding this for any Bundled c would generalize the fix to a large area of the library. But there are some regressions.

Looking at the Meta.isDefEq traces didn't help because I can't actually find where the unfolding happens.

Is there a way to avoid the unfolding of CommRingCat? Can we somehow fix this by setting the right priority? Where does the unfolding even happen?

[Anne Baanen]

Note that making docs#CommRingCat an abbrev doesn't fix the issue directly, since we still get an error failed to synthesize PreservesFilteredColimits (forget (Bundled CommRing)).

[Anne Baanen]

After staring at this for a while, it looks like the problem is indeed that the new unification hint for Bundled fires instead of the CommRingCat one. On master:

[Meta.isDefEq] ✅️ (CategoryTheory.forget ?m.4502).obj (?m.4508.stalk ?m.4509) =?= ↑X.functionField ▼
  [] ✅️ (CategoryTheory.forget ?m.4502).obj (?m.4508.stalk ?m.4509) =?= ↑X.functionField ▼
  [] ✅️ (CategoryTheory.forget ?m.4502).toPrefunctor.1 (?m.4508.stalk ?m.4509) =?= X.functionField.1 ▼
  [onFailure] ✅️ (CategoryTheory.forget ?m.4502).toPrefunctor.1 (?m.4508.stalk ?m.4509) =?= X.functionField.1 ▼
  [stuckMVar] found stuck MVar ?m.4506 : CategoryTheory.ConcreteCategory ?m.4502
  [isDefEq] 💥️ CategoryTheory.ConcreteCategory ?m.4502 =?= CategoryTheory.ConcreteCategory TopCommRingCat ▶
  [hint] (CategoryTheory.forget ?m.4502).toPrefunctor.1 (?m.4508.stalk ?m.4509) =?= X.functionField.1
  [hint] ❌️ hint SemiRingCat.forget_obj_eq_coe at (CategoryTheory.forget ?m.4502).toPrefunctor.1
      (?m.4508.stalk ?m.4509) =?= X.functionField.1 ▶
  [hint] ❌️ hint RingCat.forget_obj_eq_coe at (CategoryTheory.forget ?m.4502).toPrefunctor.1
      (?m.4508.stalk ?m.4509) =?= X.functionField.1 ▶
  [hint] ❌️ hint CommSemiRingCat.forget_obj_eq_coe at (CategoryTheory.forget ?m.4502).toPrefunctor.1
      (?m.4508.stalk ?m.4509) =?= X.functionField.1 ▶
  [hint] ✅️ hint CommRingCat.forget_obj_eq_coe at (CategoryTheory.forget CommRingCat).toPrefunctor.1
      (X.presheaf.stalk (genericPoint ↑↑X.toPresheafedSpace)) =?= X.functionField.1 ▼
  [isDefEq] ✅️ (CategoryTheory.forget CommRingCat).obj
      ?m.4607 =?= (CategoryTheory.forget ?m.4502).toPrefunctor.1 (?m.4508.stalk ?m.4509) ▶
  [isDefEq] ✅️ ↑(?m.4508.stalk ?m.4509) =?= X.functionField.1 ▶
  [] CommRingCat.forget_obj_eq_coe succeeded, applying constraints

On my branch:

  [] ✅️ (CategoryTheory.forget ?m.4631).toPrefunctor.1 (?m.4637.stalk ?m.4638) =?= X.functionField.1 ▼
  [onFailure] ✅️ (CategoryTheory.forget ?m.4631).toPrefunctor.1 (?m.4637.stalk ?m.4638) =?= X.functionField.1 ▼
  [stuckMVar] found stuck MVar ?m.4635 : CategoryTheory.ConcreteCategory ?m.4631
  [isDefEq] 💥️ CategoryTheory.ConcreteCategory ?m.4631 =?= CategoryTheory.ConcreteCategory TopCommRingCat ▼
  [] 💥️ ?m.4631 =?= TopCommRingCat ▼
  [] ?m.4631 [nonassignable] =?= TopCommRingCat [nonassignable]
  [hint] (CategoryTheory.forget ?m.4631).toPrefunctor.1 (?m.4637.stalk ?m.4638) =?= X.functionField.1
  [hint] ✅️ hint CategoryTheory.BundledHom.hint._@.Mathlib.CategoryTheory.ConcreteCategory.BundledHom._hyg.482 at (CategoryTheory.forget
            (CategoryTheory.Bundled CommRing)).toPrefunctor.1
      (X.presheaf.stalk (genericPoint ↑↑X.toPresheafedSpace)) =?= X.functionField.1 ▼
  [isDefEq] ✅️ (CategoryTheory.forget (CategoryTheory.Bundled ?m.4664)).obj
      ?m.4667 =?= (CategoryTheory.forget ?m.4631).toPrefunctor.1 (?m.4637.stalk ?m.4638) ▶

[Anne Baanen]

In particular, this depends on the order that we add the hints: declaring the generic one after the specialized one will make everything work. But we probably shouldn't make our solution order-dependent, since anyone adding a new Bundled synonym will then start encountering the same issues.

[Anne Baanen]

(Unification hints seem to have no priority mechanism, and again relying on priorities for correctness, rather than speed, strikes me as somewhat dubious.)

[Anne Baanen]

Anne Baanen said:

Note that making docs#CommRingCat an abbrev doesn't fix the issue directly, since we still get an error failed to synthesize PreservesFilteredColimits (forget (Bundled CommRing)).

I went back to this approach since it seems we really can't force Lean to stay with CommRingCat. And indeed, we did the same change in #11595 for non-commutative ring categories. Turns out the trick to making this work is to also delete the instances giving a duplicate (concrete) category structure on the synonyms.

[Anne Baanen]

@Matthew Ballard Do you remember why #11595 only turns the defs into abbrevs for non-commutative rings?

[Anne Baanen]

Oh, I just noticed #15314 touches most of the files that we were struggling with, let's see if that fixes the issues!

[Anne Baanen]

It does not fix the issues :(

[Anne Baanen]

Anne Baanen said:

Anne Baanen said:

Note that making docs#CommRingCat an abbrev doesn't fix the issue directly, since we still get an error failed to synthesize PreservesFilteredColimits (forget (Bundled CommRing)).

I went back to this approach since it seems we really can't force Lean to stay with CommRingCat. And indeed, we did the same change in #11595 for non-commutative ring categories. Turns out the trick to making this work is to also delete the instances giving a duplicate (concrete) category structure on the synonyms.

This indeed seems to make everything build! Let's try splitting into an abbrev PR and then a unif_hint PR.

[Anne Baanen]

Done! #17612 turns CommRingCat and CommSemiRingCat into abbrevs.

[Matthew Ballard]

Anne Baanen said:

Matthew Ballard Do you remember why #11595 only turns the defs into abbrevs for non-commutative rings?

I forgot commutative rings were a thing..? I just got annoyed by instRing and instRing' both existing

[Anne Baanen]

Matthew Ballard said:

I forgot commutative rings were a thing..? I just got annoyed by instRing and instRing' both existing

Interestingly for CommRingCat both of the instances were still needed. (Because one is for the Bundled.\alpha projection and the other is for the ConcreteCategory.hasCoeToSort non-instance instance.)

[Anne Baanen]

I wrote a little macro rule for erw that will first try rw and complain if that succeeds:

import Mathlib.Tactic.TryThis

/-- if we call `erw`, first try running regular `rw` and warn if that succeds. -/
macro_rules
  | `(tactic| erw $s $(loc)?) =>
    `(tactic| try_this rw $(.none)? $s $(loc)?)

#17615 applies the output of this macro to the whole of Mathlib, getting rid of a lot of false positive erws!

Should this be included by default in Mathlib? There are some false positives where rw succeeds but is not equivalent to erw, see branch#erw-to-rw-setup.

[Matthew Ballard]

Anne Baanen said:

Should this be included by default in Mathlib? There are some false positives where rw succeeds but is not equivalent to erw, see branch#erw-to-rw-setup.

I support this with some documentation for the end user to understand there can be different successful rewrites depending on the transparency.

[Ruben Van de Velde]

Something else that might be interesting: erw chains where only one or a small number of rewrites need the e

[Ruben Van de Velde]

Probably harder than that macro, though

[Anne Baanen]

I played around with a few alternative implementations, but I think the simplicity of the current approach wins. So let's go with that, adding a thorough explanation of the subtleties: #17638

[Anne Baanen]

So I spent some more time today on trying to understand why we need so much erw and I have some form of explanation.

Let's take ι_openEmbedding as an example. It starts by doing a rewrite, replacing the morphism (𝖣.ι i).base with the composition of two morphisms. Note however that type of (𝖣.ι i).base : D.U i ⟶ D.glued doesn't match the type of the composition: ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv) : (D.mapGlueData (forget C)).U i ⟶ (forget C).obj D.glued. The two types are defeq but not reducibly so.

The problem is however that the goal is equal to OpenEmbedding ⇑(D.ι i).base, where the coercion ⇑ has arguments D.U i and D.glued (and a few others). And rw doesn't care about these extra arguments at first because they are not part of the subterm to rewrite. (AFAICT, rw typechecks its motive at default transparency.) Then the next rw call happens and it's looking for the types D.U i and D.glued in the morphism (based on the arguments to ⇑). But rw only sees (D.mapGlueData (forget C)).U i and (forget C).obj D.glued, notices they are not reducibly defeq, and gives up. erw is able to unify the types and so it succeeds.

So that is the problem: we can rw our goal into something that is not type correct at reducible level, so the next rw errors on it.

[Anne Baanen]

A few solutions:

• Make more things reducible. I tried this and it works, but since there are so many operations on objects we'd just end up making this whole corner of the library reducible. (Idem for unification hints.)
• Fix the goal so it is type correct again. The problem is that some implicit arguments in the goal don't match the types we were expecting. So replace them with metavariables and reinfer them, correctly this time. Don't know how to put it into tactic code but show can do this for us if we copy and paste the displayed goal type. For example:

theorem ι_openEmbedding [HasLimits C] (i : D.J) : OpenEmbedding (𝖣.ι i).base := by
  rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _]
  -- Reinfer the types:
  show OpenEmbedding ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)
  rw [coe_comp] -- Works!
  refine
    OpenEmbedding.comp
      (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).openEmbedding
      (D.toTopGlueData.ι_openEmbedding i)

• Don't use rw lemmas that are not reducibly type-correct. I assume this involves introducing lots of identity morphisms everywhere, and even if not it certainly requires a lot more lemmas than we have.
• Think of a clever way to redefine docs#CategoryTheory.coe_comp. This seems to be a fruitful direction: coe_comp seems to be the most sensitive to these subtle non-defeq issues. So maybe we can rephrase it in such a way that it doesn't complain so often? Generalizing the thing just enough so it is still correct but no longer needs everything to be exactly equal? I played around with this but didn't find any easy ways to do it.

[Anne Baanen]

So that's pretty much where I'm stuck right now. I would appreciate any thoughts, especially insight from previous attempts.

[Christian Merten]

In #19065 I tried to implement a different approach to fixing this in AlgebraCat, one of the less used algebraic, concrete categories (so it is less painful to do the experiment): Make things less def-eq. On current master, the category instance on AlgebraCat is defined as

instance : Category (AlgebraCat.{v} R) where
  Hom A B := A →ₐ[R] B

The suggestion is to make a one field structure

structure Hom (A B : AlgebraCat.{v} R) where
  algHom : A →ₐ[R] B

and then define

instance : Category (AlgebraCat.{v} R) where
  Hom A B := Hom A B

This gets rid of all erws and simp [...]; rfls in AlgebraCat.Basic. I found the following example insightful: This is extracted from the current proof of docs#AlgebraCat.adj:

import Mathlib.Algebra.Category.AlgebraCat.Basic
open CategoryTheory AlgebraCat
variable {R : Type u} [CommRing R]
set_option pp.analyze true

example : free.{u} R ⊣ forget (AlgebraCat.{u} R) :=
  Adjunction.mkOfHomEquiv
    { homEquiv := fun _ _ => (FreeAlgebra.lift _).symm
      homEquiv_naturality_left_symm := by
        intro X Y Z f g
        apply FreeAlgebra.hom_ext
        ext x
        simp only [Equiv.symm_symm, Function.comp_apply, free_map]
        /- Eq (α := Z)
             (((FreeAlgebra.lift R) (f ≫ g) :
               Prefunctor.obj (Functor.toPrefunctor (free R)) X ⟶ Z) (FreeAlgebra.ι R x) : ↑Z) _
        -/
        erw [FreeAlgebra.lift_ι_apply]
        sorry
      homEquiv_naturality_right := sorry }

While we can fix coe lemmas by supplying no_index or simply providing all possible combinations of .ofHom and .of, I think we can't fix this type of problem without making everything reducible. Namely here,
docs#FreeAlgebra.lift_ι_apply expects (FreeAlgebra.lift R) (f ≫ g) to be of type FreeAlgebra R X →ₐ[R] Z, but this is not reducibly def-eq to the synthesized type.

[Eric Wieser]

Christian Merten said:

The suggestion is to make a one field structure

structure Hom (A B : AlgebraCat.{v} R) where
  algHom : A →ₐ[R] B

and then define

instance : Category (AlgebraCat.{v} R) where
  Hom A B := A →ₐ[R] B

Did you mean

instance : Category (AlgebraCat.{v} R) where
  Hom A B := Hom A B

[Christian Merten]

Oops, yes!

[Jiang Jiedong]

If applied to CommRingCat, I believe this change will help in solving part of the IsLocalHom issue.

This is a common phenomenon that due to defeq, when Lean need to infer the type F in a theorem with signature {F} [FunLike F A B] (f : F), behaves undesirably when there are multiple defeq choices. This change will completely distinguish hom from the real RingHom.

[Adam Topaz]

I've been advocating for this approach for a while. It worked out quite well when I did a similar refactor for morphisms of sheaves, cf. CategoryTheory.Sheaf.Hom, even without the FunLike infrastructure. It would be really nice if we also had some automation to help out here.

[Andrew Yang]

I’ve wrapped scheme morphisms into structures for this very same reason.
I did extends OldStructure instead of one field structures which kept all the dot notations and it was quite nice.

[Eric Wieser]

I used this approach when building docs#QuadraticModuleCat.Hom too

[Adam Topaz]

For now, what do folks think about adding a simple command like this?

import Lean

open Lean Parser Elab Command

@[command_parser]
def wrapperParser := leading_parser
  declModifiers false >> "wrap" >> declId >> (many <| Term.bracketedBinder) >> Term.typeSpec

@[command_elab wrapperParser]
def elabWrapper : CommandElab
  | `($mods:declModifiers wrap $name $args* : $res) => do
      elabCommand <| ← `($mods:declModifiers structure $name $args* where as : $res)
  | _ => throwUnsupportedSyntax

@[ext]
wrap NatWrapper (a b : Nat) : Nat

#check NatWrapper.as
#check NatWrapper.mk
#check NatWrapper.ext

[Adam Topaz]

It doesn't to anything really, but it could be expanded later on.

[Eric Wieser]

I think this isn't really solving the right problem; I think we want something more like

@[wrap]
structure WrappedFoo where ofFoo :: toFoo : Foo

which gives the user the freedom to name things as they like, but then generates all the extra boilerplate around it

[Eric Wieser]

For category theory wrappers, we probably want to call the field hom or similar, whereas elsewhere in mathlib we might want to choose different names

[Adam Topaz]

Yeah I think you’re right. Maybe we should collect some cases where wrapping in this way is useful. Category theory is an obvious one, especially for concrete categories. Any others?

[Eric Wieser]

Any type of "strong" type synonym like Polynomial or SkewMonoidAlgebra

[Eric Wieser]

Arguably what's missing there is a deriving handler for single-field structures.

[Eric Wieser]

Something that generates an Equiv to the field would be handy too

[Kim Morrison]

I think we should get started on this! I think it's okay to work incrementally (i.e. we don't need to change all the concrete categories in one go)

[Christian Merten]

I have some progress for the ring categories in a branch that I can push, but there is a design question that I still have not figured out:

All the mentioned examples in this thread are examples without a FunLike instance on the homs and a lot of the coe_comp issues with the current design have no reason to vanish with the one-field structure design. Consider for example:

Toy

import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

class Foo (X : Type u) where

structure FooCat where
  carrier : Type u
  [foo : Foo carrier]

namespace FooCat

attribute [instance] foo

instance : CoeSort FooCat (Type u) where
  coe := carrier

@[ext]
structure Hom (X Y : FooCat) where
  toFun : X → Y

instance : Category FooCat where
  Hom := Hom
  id X := ⟨id⟩
  comp f g := ⟨g.toFun ∘ f.toFun⟩

lemma hom_ext {X Y : FooCat} {f g : X ⟶ Y} (h : f.toFun = g.toFun) : f = g := by
  cases f
  cases g
  aesop

instance (X Y : FooCat) : FunLike (X ⟶ Y) X Y where
  coe f := f.toFun
  coe_injective' _ _ h := hom_ext h

def of (X : Type u) [Foo X] : FooCat.{u} where
  carrier := X

def ofHom {X Y : Type u} [Foo X] [Foo Y] (f : X → Y) : of X ⟶ of Y where
  toFun := f

@[simp] lemma coe_of (X : Type u) [Foo X] : of X = X := rfl
@[simp] lemma coe_toFun {X Y : FooCat} [Foo X] (f : X ⟶ Y) : f.toFun = ⇑f := rfl

@[simp] lemma coe_ofHom {X Y : Type u} [Foo X] [Foo Y] (f : X → Y) :
    DFunLike.coe (α := X) (β := fun _ ↦ Y) (ofHom f) = f := rfl

@[simp] lemma coe_id (X : FooCat) : ⇑(𝟙 X) = id := rfl
@[simp] lemma coe_comp {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := rfl
@[simp] lemma coe_comp_of {X Y : FooCat} {Z : Type u} [Foo Z] (f : X ⟶ Y) (g : Y ⟶ of Z) :
    DFunLike.coe (α := X) (β := fun _ ↦ Z) (f ≫ g) = ⇑g ∘ ⇑f := rfl
@[simp] lemma coe_of_comp {X : Type u} [Foo X] {Y Z : FooCat} (f : of X ⟶ Y) (g : Y ⟶ Z) :
    DFunLike.coe (α := X) (β := fun _ ↦ Z) (f ≫ g) = ⇑g ∘ ⇑f := rfl
@[simp] lemma coe_of_comp_of {X Z : Type u} [Foo X] [Foo Z] {Y : FooCat}
    (f : of X ⟶ Y) (g : Y ⟶ of Z) :
    DFunLike.coe (α := X) (β := fun _ ↦ Z) (f ≫ g) = ⇑g ∘ ⇑f := rfl
@[simp] lemma coe_id_of (X : Type u) [Foo X] :
    DFunLike.coe (α := X) (β := fun _ ↦ X) (𝟙 (of X)) = id := rfl

section Test

example (X : Type u) [Foo X] : ⇑(𝟙 (of X)) = id := by simp

example {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := by simp

example {X Y Z : Type u} [Foo X] [Foo Y] [Foo Z] (f : X → Y) (g : Y → Z) :
    ⇑(ofHom f ≫ ofHom g) = g ∘ f := by simp

example {X Y : Type u} [Foo X] [Foo Y] {Z : FooCat} (f : X → Y) (g : of Y ⟶ Z) :
    ⇑(ofHom f ≫ g) = g ∘ f := by simp

example {X Y : FooCat} {Z : Type u} [Foo Z] (f : X ⟶ Y) (g : Y ⟶ of Z) :
    ⇑(f ≫ g) = g ∘ f := by simp

example {Y Z : FooCat} {X : Type u} [Foo X] (f : of X ⟶ Y) (g : Y ⟶ Z) :
    ⇑(f ≫ g) = g ∘ f := by simp

example {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp

example (X : FooCat) : ⇑(𝟙 X) = id := by simp

end Test

As you can see, we still need 9 coe_ lemmas to make all the examples work. Can we do better?

[Christian Merten]

A good sign is that so far I have not needed more no_index tweaking.

[Christian Merten]

I started a try on automatically performing theses tests, but my meta skills are too non-existent to make significant progress.

[Eric Wieser]

Do we actually want a FunLike (X ⟶ Y) X Y instance?

[Eric Wieser]

I'd argue that if you want to talk about applying functions, you should jump out of category theory land and write f.hom instead

[Christian Merten]

I had the same thought a few days ago, but I think we want this instance. For example AG is already now very heavy on notation, so without the FunLike instance for a morphism of schemes f, application to an element would now be f.base.hom x. Maybe this could be remedied by a shortcut Scheme.Hom.apply, but this would then lead to a bunch of new _apply lemmas.

[Christian Merten]

(Note that with the current approach, all these coe lemmas are also needed and you can convince yourself that taking the test examples from above and specializing to e.g. CommRingCat many of them will fail.)

[Johan Commelin]

Christian Merten said:

I had the same thought a few days ago, but I think we want this instance. For example AG is already now very heavy on notation, so without the FunLike instance for a morphism of schemes f, application to an element would now be f.base.hom x. Maybe this could be remedied by a shortcut Scheme.Hom.apply, but this would then lead to a bunch of new _apply lemmas.

So maybe we should create shortcut abbrevs specifically for schemes. Because they are a pretty special case within the larger zoo of concrete categories. (In particular they are not concrete...)

[Christian Merten]

I don't really see a problem with adding (many) boilerplate coe lemmas, but we have to do it systematically. An automatic way of generating the tests above would be a first step in this direction.

[Eric Wieser]

Avoiding FunLike seems to solve the problem above

[Eric Wieser]

import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

class Foo (X : Type u) where

structure FooCat where
  carrier : Type u
  [foo : Foo carrier]

namespace FooCat

attribute [instance] foo

instance : CoeSort FooCat (Type u) where
  coe := carrier

@[ext]
structure Hom (X Y : FooCat) where
  toFun : X → Y

instance : Category FooCat where
  Hom := Hom
  id X := ⟨id⟩
  comp f g := ⟨g.toFun ∘ f.toFun⟩

lemma hom_ext {X Y : FooCat} {f g : X ⟶ Y} (h : f.toFun = g.toFun) : f = g := by
  cases f
  cases g
  aesop

-- `CoeFun` is inlined, unlike FunLike
instance (X Y : FooCat) : CoeFun (X ⟶ Y) (fun _ => X → Y) where
  coe f := f.toFun

def of (X : Type u) [Foo X] : FooCat.{u} where
  carrier := X

def ofHom {X Y : Type u} [Foo X] [Foo Y] (f : X → Y) : of X ⟶ of Y where
  toFun := f

@[simp] lemma coe_toFun {X Y : FooCat} [Foo X] (f : X ⟶ Y) : f.toFun = ⇑f := rfl

@[simp] lemma coe_ofHom {X Y : Type u} [Foo X] [Foo Y] (f : X → Y) :
  (ofHom f).toFun = f := rfl

@[simp] lemma coe_id (X : FooCat) : ⇑(𝟙 X) = id := rfl
@[simp] lemma coe_comp {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := rfl

section Test

example (X : Type u) [Foo X] : ⇑(𝟙 (of X)) = id := by simp

example {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) : ⇑(f ≫ g) = ⇑g ∘ ⇑f := by simp

example {X Y Z : Type u} [Foo X] [Foo Y] [Foo Z] (f : X → Y) (g : Y → Z) :
    ⇑(ofHom f ≫ ofHom g) = g ∘ f := by simp

example {X Y : Type u} [Foo X] [Foo Y] {Z : FooCat} (f : X → Y) (g : of Y ⟶ Z) :
    ⇑(ofHom f ≫ g) = g ∘ f := by simp

example {X Y : FooCat} {Z : Type u} [Foo Z] (f : X ⟶ Y) (g : Y ⟶ of Z) :
    ⇑(f ≫ g) = g ∘ f := by simp

example {Y Z : FooCat} {X : Type u} [Foo X] (f : of X ⟶ Y) (g : Y ⟶ Z) :
    ⇑(f ≫ g) = g ∘ f := by simp

example {X Y Z : FooCat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := by simp

example (X : FooCat) : ⇑(𝟙 X) = id := by simp

end Test

[Christian Merten]

Johan Commelin said:

Christian Merten said:

I had the same thought a few days ago, but I think we want this instance. For example AG is already now very heavy on notation, so without the FunLike instance for a morphism of schemes f, application to an element would now be f.base.hom x. Maybe this could be remedied by a shortcut Scheme.Hom.apply, but this would then lead to a bunch of new _apply lemmas.

So maybe we should create shortcut abbrevs specifically for schemes. Because they are a pretty special case within the larger zoo of concrete categories. (In particular they are not concrete...)

And (locally) ringed spaces, adic spaces, etc. I think adding the coe lemmas for TopCat in this case is less boilerplat than adding them for every cat. building on top of that.

[Christian Merten]

Aha, CoeFun it is then?

[Johan Commelin]

But then none of the map_add and map_mul lemmas will be able to fire, right?

[Christian Merten]

Ah, but we can't have FooHomClass (M ⟶ N) ... then, right?

[Christian Merten]

@Eric Wieser you say that CoeFun is inlined, unlike FunLike. What does this mean? Could FunLike be also inlined?

[Anne Baanen]

Christian Merten said:

Eric Wieser you say that CoeFun is inlined, unlike FunLike. What does this mean? Could FunLike be also inlined?

This means when we write f x we don't see CoeFun.coe f x, but f.toFun x. With a FunLike instance we'd get FunLike.toFun f x.

[Anne Baanen]

FooHomClasses need the FunLike.toFun there, otherwise map_foo f : FunLike.toFun f foo = foo wouldn't fire on Hom.toFun f foo.

[Eric Wieser]

In reality isn't SomeCategoryHom.toFun a type like AddMonoidHom anyway?

[Christian Merten]

But if f x becomes f.toFun x why does the FooHomClass instance for f.toFun not trigger?

[Eric Wieser]

So writing some_hom.toFun x really means DFunLike.coe some_hom.toFun x

[Eric Wieser]

Christian Merten said:

But if f x becomes f.toFun x why does the FooHomClass instance for f.toFun not trigger?

Do you have an example of this happening?

[Christian Merten]

Eric Wieser said:

Christian Merten said:

But if f x becomes f.toFun x why does the FooHomClass instance for f.toFun not trigger?

Do you have an example of this happening?

I deduced this from Johan's message above, let me try.

[Eric Wieser]

I think you confused things by calling the field toFun instead of toHom or hom or deCat or whatever

[Johan Commelin]

Yeah, I probably got confused there

[Christian Merten]

Indeed, I confirm when applying Eric's suggestion above to #19065, the following tests all work:

example {M N : AlgebraCat.{v} R} (f : M ⟶ N) (x y : M) : f (x + y) = f x + f y := by
  simp

example {M N : AlgebraCat.{v} R} (f : M ⟶ N) : f 0 = 0 := by
  simp

example {M N : AlgebraCat.{v} R} (f : M ⟶ N) (r : R) (m : M) : f (r • m) = r • f m := by
  simp

[Eric Wieser]

But my (perhaps-uninformed) recommendation would still be to not have the CoeFun instance at all

[Eric Wieser]

It's harmless enough, but now you have to decide whether to call the lemmas toFun_comp or coe_comp

[Christian Merten]

But isn't the CoeFun instance precisely doing what you suggested, but hidden by nice notation? I.e. f x is unfolded to f.hom x anyway, so I see no problem.

[Eric Wieser]

How often do you actually write f x when working in, say, AlgebraCat?

[Eric Wieser]

Isn't the point of category theory that you don't really "apply" your morphisms in the first place, and treat them as abstract arrows?

[Christian Merten]

I do write f x very often when working with CommRingCat or TopCat in the context of algebraic geometry.

[Christian Merten]

Eric Wieser said:

Isn't the point of category theory that you don't really "apply" your morphisms in the first place, and treat them as abstract arrows?

With concrete categories, you certainly want and need both perspectives.

[Christian Merten]

I updated #19065 with the CoeFun suggestion and added a bunch of example tests verifying that indeed simp works nicely.
Unfortunately, the benchmark does not look very good. There seems to be a +1.21% on lint which sounds like a big change and also some slowdown in Mathlib.Algebra.Cateogry.AlgebraCat.Limits, which I don't understand. Does anyone have an idea what is going wrong here?

[Christian Merten]

(the +1.21% was already there before adapting the CoeFun change)

[Anne Baanen]

I never really understood why the one-member structure helps until I see the effects in real life, and now I think I get it. By giving the algHom projection its own name, we avoid identifying ⟶ and →ₐ. So then the instances on those types don't get mixed up. That seems to be the main source of erws: when one rewrite saw through the defeq of ⟶ and →ₐ but then another one couldn't. Thanks for putting it in practice :light_bulb:

[Christian Merten]

And I am confident that with the CoeFun approach and hence no FooHomClass, this will also get rid of all the struggles with things like docs#IsLocalHom because there can't be confusion in the F variable anymore.

[Anne Baanen]

Right, because there is no FooHomClass on the Hom structure, but there is still one on the projection via CoeFun, it actually still works. Very clever!

[Kevin Buzzard]

Write a community blog post while the ideas are still fresh in your mind @Christian Merten !

[Eric Wieser]

Anne Baanen said:

By giving the algHom projection its own name, we avoid identifying ⟶ and →ₐ

It also means we can actually state lemmas like "categorical composition is LinearMap.comp` etc (as in docs#QuadraticModuleCat.toIsometry_comp) without this weird identification being used to make the types of the LHS and RHS match (as in docs#ModuleCat.comp_def)

[Eric Wieser]

Anne Baanen said:

because there is no FooHomClass on the Hom structure, but there is still one on the projection via CoeFun, it actually still works

note that in the infoview it will presumably still display as f.hom x, but I guess being able to write f x is the main thing

[Eric Wieser]

(and of course a custom delaborator for categorical morphisms is totally in the space of reasonable things to do)

[Matthew Ballard]

I left a comment on the PR to avoid some eta expansions. Like Eric I find the CoeFun’s somewhat icky but the battle is already lost with the CoeSort I think.

Should forget be inlined in addition to being reducible?

[Eric Wieser]

Agreed that the CoeFun and CoeSort are at least consistent

[Eric Wieser]

In the longer run I suppose you could do something nuts like ⧘f⧙ x and f : ⧘X⧙ →ₐ ⧘Y⧙ to explicitly mark the boundaries between categorical and non-categorical objects, with less visual noise than .toFun, .hom, etc

[Matthew Ballard]

Yes, anonymous destructors would be nice

[Eric Wieser]

Oh, I was just proposing a scoped notation specific to CategoryTheory

[Edward van de Meent]

this can just be a notation class, right?

[Edward van de Meent]

now of course ⧘ and ⧙ are nontrivial to type, so that will need some adaptation too, but this does seem like a workable solution.

[Christian Merten]

The main performance penalty of scrapping FunLike seems to come from instance synthesization of MulHomClass etc. for the underlying AlgHom. When using (the sadly deprecated) AlgHom.map_{one,zero,mul,add} instead of the corresponding map_{one,zero,mul,add} we are back to the old performance with the FunLike instance. This is a problem I have already encountered many times with AlgHoms, that the corresponding MulHomClass and friends take long to synthesize (sometimes leading to timeouts). So I think this is unrelated to this PR, it's just surfacing now, because f x gets unfolded to f.algHom x now. Should we accept this in this change then and investigate the synthesization slowness independently of this PR?

[Yaël Dillies]

Christian Merten said:

When using (the sadly deprecated) AlgHom.map_{one,zero,mul,add} instead of the corresponding map_{one,zero,mul,add} we are back to the old performance with the FunLike instance

Can we simply undeprecate those lemmas?

[Yaël Dillies]

cc @Kim Morrison who is currently removing uses of it throughout mathlib

[Christian Merten]

Yaël Dillies said:

Christian Merten said:

When using (the sadly deprecated) AlgHom.map_{one,zero,mul,add} instead of the corresponding map_{one,zero,mul,add} we are back to the old performance with the FunLike instance

Can we simply undeprecate those lemmas?

I would be in favor of this.

[Matthew Ballard]

It looks like it was originally done in #14168

[Matthew Ballard]

The keys for docs#map_pow

@DFunLike.coe _ _ _ _ _ (@HPow.hPow _ ℕ _ _ _ _)

vs docs#AlgHom.map_pow

@DFunLike.coe (AlgHom _ _ _ _ _ _ _ _) _ _ _ _ (@HPow.hPow _ ℕ _ _ _ _)

[Matthew Ballard]

The priority of docs#map_pow has already been lowered for this reason

[Kevin Buzzard]

We could also do with a blog post on what the heck keys/discrimination trees are and what a mathematician needs to know about them.

In 2017/18 sometimes when I understood something useful I'd write a Xena blog post and some of these still get referred to in Zulip now

[Ruben Van de Velde]

Yeah, I thought that was me. Duplicating all those lemmas across all the kinds of homs that they apply to is pretty bad - I'd hope we'd only do that as a temporary measure while we wait for lean to get cleverer

[Eric Wieser]

Matthew Ballard said:

The keys for docs#map_pow

@DFunLike.coe _ _ _ _ _ (@HPow.hPow _ ℕ _ _ _ _)

vs docs#AlgHom.map_pow

@DFunLike.coe (AlgHom _ _ _ _ _ _ _ _) _ _ _ _ (@HPow.hPow _ ℕ _ _ _ _)

This looks to be working as intended to me, so long as the subsequent MonoidHomClass lookup that happens after trying the key is fast

[Christian Merten]

I found the two bad simp lemmas in #19065: AlgebraCat.forget_obj and AlgebraCat.forget_map, they have the keys:

#[Prefunctor.0, *, CategoryTheory.Functor.0, CategoryTheory.ConcreteCategory.0, *]

and

#[Prefunctor.1, *, *, *, CategoryTheory.Functor.0, CategoryTheory.ConcreteCategory.0, *]

respectively. So neither of them mention AlgebraCat. Is this expected?
In the meantime, I just removed the @[simp] from these (they are not @[simp] on master either) and the +1.2% lint is gone.

[Christian Merten]

@Eric Wieser suggested to do a poll on the naming of the field of AlgebraCat.Hom. For comparison, docs#QuadraticModuleCat uses toIsometry, docs#AlgebraicGeometry.Scheme uses toHom with a custom simps projection toLRSHom. So here goes a poll:

[Christian Merten]

/poll How should we name the field in FooCat.Hom?
toFooHom (e.g. toRingHom, toAlgHom)
fooHom (e.g. ringHom, algHom)
toHom
hom

[Eric Wieser]

One downside of hom is that when working with e : X ≅ Y, the underlying map is e.hom.hom

[Christian Merten]

True, but also it is the shortest to type.

[Christian Merten]

(but slightly strange in the case Foo = Top)

[Christian Merten]

The poll has a tendency towards .hom so I went with this.

[Johan Commelin]

I could even imagine refactoring Iso to have a .fwd and .inv instead of .hom and .inv.

[Anne Baanen]

The AlgebraCat hom structure got merged! I'm taking a look at ModuleCat now...

[Anne Baanen]

I pushed my progress to PR #19511. I got it almost working, except for two files:

In file#Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed there are two definitions sorry'd there that should be easy to implement for someone who knows what they're doing.

In file#Mathlib/AlgebraicGeometry/Modules/Tilde we call docs#Limits.Concrete.colimit_no_zero_smul_divisor which essentially asserts we're in a subcategory of ModuleCat by requiring a LinearMapClass instance on the homs. But the point of doing this refactor is to make the homs not a linear map, so I'm not sure how to proceed. There are also a few errors downstream of that that I haven't looked at in details.

[Christian Merten]

Can we reformulate docs#colimit_no_zero_smul_divisor with the assumption [HasForget₂ C ModuleCat]?

[Anne Baanen]

Ooh, that's a good idea! I have to work on other projects right now, feel free to make any changes you want to the PR :)

[Anne Baanen]

I left a lot of comments on the PR with todo notes.

[Anne Baanen]

I had some time today to try out the HasForget₂ suggestion, and unfortunately I don't understand this enough to make substantial progress.

I feel like something like the below should work, but I get type mismatches and can't find how to deal with them:

import Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
import Mathlib.Algebra.Category.ModuleCat.Basic
import Mathlib.Tactic.CategoryTheory.Elementwise

universe t w v u r

open CategoryTheory

namespace CategoryTheory.Limits.Concrete

attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort

variable {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C]

/--
If the forgetful functors factors through `ModuleCat`, morphisms preserve zero.
-/
-- TODO: use something like `HasForget₂ C AddMonCat` instead?
lemma map_zero_of_hasForget₂ (R : Type*) [Ring R] [∀ c : C, AddCommMonoid c] [∀ c : C, Module R c]
    [HasForget₂ C (ModuleCat R)] {X Y : C} (f : X ⟶ Y) :
    f 0 = 0 := by
  convert ((forget₂ C (ModuleCat R)).map f).hom.map_zero
  -- goal contains `((forget₂ C (ModuleCat R)).map f).hom` of type
  --   `(forget₂ C (ModuleCat R)).obj X →ₗ[R] (forget₂ C (ModuleCat R)).obj Y`
  -- we want `f : (forget C).obj X → (forget C).obj Y`
  sorry

/--
If the forgetful functors factors through `ModuleCat`, morphisms preserve scalar multiplication.
-/
lemma map_smul_of_hasForget₂ {R : Type*} [Ring R] [∀ c : C, AddCommMonoid c] [∀ c : C, Module R c]
    [HasForget₂ C (ModuleCat R)] (r : R) {X Y : C} (f : X ⟶ Y) (x : (forget C).obj X) :
    f (r • x) = r • f x := by
  convert ((forget₂ C (ModuleCat R)).map f).hom.map_smul r _
  · -- goal contains `((forget₂ C (ModuleCat R)).map f).hom` of type
    --   `(forget₂ C (ModuleCat R)).obj X →ₗ[R] (forget₂ C (ModuleCat R)).obj Y`
    -- we want `f : (forget C).obj X → (forget C).obj Y`
    sorry
  · -- `x : (forget C).obj X`
    -- we want a `(forget₂ C (ModuleCat R)).obj X`
    sorry

[Anne Baanen]

Anyone who actually knows what they're doing who can advise? :)

[Christian Merten]

I think these instances [∀ c : C, AddCommMonoid c] cause trouble here. The HasForget_2 will give a different AddCommMonoid instance.

[Christian Merten]

The issue seems to me that the only sensible spelling of your first lemma is

lemma map_zero_of_hasForget₂ (R : Type*) [Ring R]
    [HasForget₂ C (ModuleCat R)] {X Y : C} (f : X ⟶ Y) :
    (forget₂ C (ModuleCat R)).map f 0 = 0 := by
  simp

which is of course not very insightful.

[Anne Baanen]

Christian Merten said:

I think these instances [∀ c : C, AddCommMonoid c] cause trouble here. The HasForget_2 will give a different AddCommMonoid instance.

Hmm, but if I remove those instances it says the HSMul R ((forget C).obj X) ?m.4059 instance can't be found...

[Anne Baanen]

I suppose an alternative solution is to add the LinearMapClass instances locally in the file defining docs#Limits.Concrete.colimit_no_zero_smul_divisor ?

[Anne Baanen]

That is: HasForget_2 C (ModuleCat R) implies LinearMapClass (X --> Y)

[Christian Merten]

Maybe for now it is fine to just formulate the problematic file for ModuleCat? Or are they used in cases where C is not ModuleCat? I think this should not stop this refactor.

[Anne Baanen]

It seems to be only used for ModuleCat itself: rg reports

Mathlib/AlgebraicGeometry/Modules/Tilde.lean
192:  refine Limits.Concrete.colimit_no_zero_smul_divisor

Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean
22:- `CategoryTheory.Limits.Concrete.colimit_no_zero_smul_divisor`: Let `C` be a category where its
59:lemma colimit_no_zero_smul_divisor

[Christian Merten]

Anne Baanen said:

That is: HasForget_2 C (ModuleCat R) implies LinearMapClass (X --> Y)

This won't work until you also have instances like

instance [HasForget₂ C AddMonCat] (X : C) : AddCommMonoid X :=
  sorry

right?

[Anne Baanen]

Christian Merten said:

Anne Baanen said:

That is: HasForget_2 C (ModuleCat R) implies LinearMapClass (X --> Y)

This won't work until you also have instances like

instance [HasForget₂ C AddMonCat] (X : C) : AddCommMonoid X :=
  sorry

right?

Ah, because otherwise there is nothing saying the AddCommMonoid X instance coincides with the one induced by the forget_2 map?

[Christian Merten]

Yes

[Christian Merten]

And I don't think there is a good way to get this AddCommMonoid X instance in a sane way with the current definition of HasForget_2. Maybe HasForget_2 should be changed to:

class HasForget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
  [Category.{v'} D] [ConcreteCategory.{w} D] where
  forget₂ : C ⥤ D
  forgetComp : forget₂ ⋙ forget D ≅ forget C

So that we can have data carrying arround the actual isomorphism forget₂ ⋙ forget D ≅ forget C. Then we should be able to have instances like

instance [HasForget₂ C AddMonCat] (X : C) : AddCommMonoid X :=
  sorry

by transporting the AddCommMonoid instance on (forget AddMonCat).obj ((forget₂ C AddMonCat).obj X) via the isomorphism forgetComp.app X to (forget C).obj X.

[Christian Merten]

But this has nothing to do with the ModuleCat refactor, so I vote for just specializing the problematic file to ModuleCat for now.

[Anne Baanen]

I did a lot of cleanup in #19511 and it should now be ready for review :D

[Johan Commelin]

Major effort! Everybody who regularly works with these types of categories is invited to take a look.
cc @Christian Merten @Andrew Yang @Junyan Xu (random subset, others are welcome to review as well).

[Kim Morrison]

Mostly this is looking really nice.

But there are some problems where we need to fill in too many sources and targets by hand. e.g. Mathlib.AlgebraicGeometry.Modules.Tilde. So further pinging @Jujian Zhang to see if they have suggestions!

[Johan Commelin]

I agree that the diff is looking very nice now.
@Joël Riou do you have opinions on this refactor?

[Joël Riou]

This is a great effort, and it certainly goes in the right direction!

[Anne Baanen]

I have been experimenting with making a class for ConcreteCategory which has a bundled Hom type, so that we can write elementwise lemmas in high generality without having to convert them from ConcreteCategory.forget-style definitions. (This was prompted by Kim's comment on https://github.com/leanprover-community/mathlib4/pull/19511#discussion_r1867083077).

import Mathlib

namespace CategoryTheory

universe w v u

class BundledHomCategory (C : Type u) [Category.{v} C]
    (F : outParam <| C → C → Type*) (carrier : outParam <| C → Type w)
    [∀ X Y, FunLike (F X Y) (carrier X) (carrier Y)] where
  (hom : ∀ {X Y}, (X ⟶ Y) → F X Y)
  (ofHom : ∀ {X Y}, F X Y → (X ⟶ Y))
  (hom_ofHom : ∀ {X Y} (f : F X Y), hom (ofHom f) = f := by aesop_cat)
  (ofHom_hom : ∀ {X Y} (f : X ⟶ Y), ofHom (hom f) = f := by aesop_cat)
  (hom_id_apply : ∀ {X} (x : carrier X), hom (𝟙 X) x = x := by aesop_cat)
  (hom_comp_apply : ∀ {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) (x : carrier X),
    hom (f ≫ g) x = hom g (hom f x) := by aesop_cat)

class BundledZeroHomCategory (C : Type u) [Category.{v} C]
    (F : outParam <| C → C → Type*) (carrier : outParam <| C → Type w)
    [∀ X Y, FunLike (F X Y) (carrier X) (carrier Y)]
    [CategoryTheory.Limits.HasZeroMorphisms C] [∀ X, Zero (carrier X)]
    extends BundledHomCategory C F carrier where
  (hom_zero_apply : ∀ {X Y} (x : carrier X), hom (0 : X ⟶ Y) x = 0 := by aesop_cat)

namespace BundledHomCategory

variable {C : Type u} [Category.{v} C] {F : C → C → Type*} {carrier : C → Type w}
variable [∀ X Y, FunLike (F X Y) (carrier X) (carrier Y)]
variable [BundledHomCategory C F carrier]

attribute [simp] hom_id_apply hom_comp_apply

instance {X Y : C} : CoeFun (X ⟶ Y) (fun _ ↦ carrier X → carrier Y) where
  coe f := hom f

def homEquiv {X Y : C} : (X ⟶ Y) ≃ F X Y where
  toFun := hom
  invFun := ofHom
  left_inv := ofHom_hom
  right_inv := hom_ofHom

lemma hom_bijective {X Y : C} : Function.Bijective (hom : (X ⟶ Y) → F X Y) :=
  homEquiv.bijective

lemma hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → F X Y) :=
  hom_bijective.injective

@[ext] lemma ext {X Y : C} {f g : X ⟶ Y} (h : hom f = hom g) : f = g :=
  hom_injective h

@[ext]
lemma coe_ext {X Y : C} {f g : X ⟶ Y} (h : ⇑(hom f) = ⇑(hom g)) : f = g :=
  ext (DFunLike.coe_injective h)

@[ext]
lemma ext_apply {X Y : C} {f g : X ⟶ Y} (h : ∀ x, f x = g x) : f = g :=
  ext (DFunLike.ext _ _ h)

instance : ConcreteCategory C where
  forget.obj := carrier
  forget.map f := ⇑(hom f)
  forget_faithful.map_injective h := coe_ext h

end BundledHomCategory

namespace BundledZeroHomCategory

open BundledHomCategory

variable {C : Type u} [Category.{v} C] {F : C → C → Type*} {carrier : C → Type w}
variable [∀ X Y, FunLike (F X Y) (carrier X) (carrier Y)]
variable [CategoryTheory.Limits.HasZeroMorphisms C] [∀ X, Zero (carrier X)]
variable [BundledZeroHomCategory C F carrier]

attribute [simp] hom_zero_apply

open Limits

@[simp]
lemma cokernel_condition
    {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f]
     (x) :
    hom (cokernel.π f) (hom f x) = 0 := by
  simpa only [hom_comp_apply, hom_zero_apply x]
    using BundledHomCategory.ext_apply_iff.mp (CategoryTheory.Limits.cokernel.condition f) x

#discr_tree_key cokernel_condition

end BundledZeroHomCategory

namespace ModuleCat

open Limits BundledHomCategory BundledZeroHomCategory

variable {R : Type u} [Ring R]

instance : BundledZeroHomCategory (ModuleCat.{v} R) (fun M N ↦ M →ₗ[R] N) (ModuleCat.carrier) where
  hom := ModuleCat.Hom.hom
  ofHom := ModuleCat.ofHom

lemma foo {M N : ModuleCat.{v} R} (g : M ⟶ N) (x : M) : hom (cokernel.π g) (hom g x) = 0 := by simp

#discr_tree_key foo

end ModuleCat

end CategoryTheory

/-! ## Can we restate the specialized lemmas about colimits in general again? -/

universe t w v u r

open CategoryTheory

namespace CategoryTheory.Limits.Concrete

variable {J : Type w} [Category.{r} J]
variable {C : Type u} [Category.{v} C] (carrier : C → Type (max t w))
variable {FC : C → C → Type*} [∀ X Y, FunLike (FC X Y) (carrier X) (carrier Y)]
variable [BundledHomCategory C FC carrier]

section zero

open BundledHomCategory

lemma colimit_rep_eq_iff_exists' (F : J ⥤ C) [PreservesColimit F (forget C)] [IsFiltered J]
    [HasColimit F] {i j : J} (x : (forget C).obj (F.obj i)) (y : (forget C).obj (F.obj j)) :
    (colimit.ι F i) x = (colimit.ι F j) y ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
  colimit_rep_eq_iff_exists F x y

theorem colimit_rep_eq_zero'
    (F : J ⥤ C) [PreservesColimit F (forget C)] [IsFiltered J]
    [∀ c : C, Zero ((forget C).obj c)]
    [∀ {c c' : C}, ZeroHomClass (FC c c') ((forget C).obj c) ((forget C).obj c')] [HasColimit F]
    (j : J) (x : (forget C).obj (F.obj j)) (hx : colimit.ι F j x = 0) :
    ∃ (j' : J) (i : j ⟶ j'), F.map i x = 0 := by
  rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists'] at hx
  obtain ⟨j', i, y, g⟩ := hx
  exact ⟨j', i, g ▸ by simp⟩

end zero

section module

open BundledHomCategory

theorem colimit_exists_rep' (F : J ⥤ C) [PreservesColimit F (forget C)]
    [HasColimit F] (x : carrier (colimit F)) :
    ∃ (j : J) (y : carrier (F.obj j)), colimit.ι F j y = x :=
  colimit_exists_rep F x

/--
if `r` has no zero smul divisors for all small-enough sections, then `r` has no zero smul divisors
in the colimit.
-/
@[simp]
lemma colimit_no_zero_smul_divisor'
    (F : J ⥤ C) [PreservesColimit F (forget C)] [IsFiltered J] [HasColimit F]
    (R : Type*) [Semiring R]
    [∀ c : C, AddCommMonoid (carrier c)] [∀ c : C, Module R (carrier c)]
    [∀ {c c' : C}, LinearMapClass (FC c c') R (carrier c) (carrier c')]
    (r : R) (H : ∃ (j' : J), ∀ (j : J) (_ : j' ⟶ j), ∀ (c : carrier (F.obj j)), r • c = 0 → c = 0)
    (x : (forget C).obj (colimit F)) (hx : r • x = 0) : x = 0 := by
  classical
  obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep' carrier F x
  rw [← map_smul (BundledHomCategory.hom (colimit.ι F j))] at hx
  obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero' (hx := hx)
  obtain ⟨j'', H⟩ := H
  -- Restate to apply to `hom` instead of `ConcreteCategory.instFunLike`.
  have : ∀ {j j'} (i : j ⟶ j') (x : carrier (F.obj j)), (colimit.ι F j') ((F.map i) x) = (colimit.ι F j) x :=
    fun i => elementwise_of% (colimit.w F i)
  simpa [this, map_zero] using congr(colimit.ι F _
    $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
      (IsFiltered.toSup _ _ <| by simp)
      (F.map (IsFiltered.toSup _ _ <| by simp) x)
      (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
        hom_comp_apply, ← map_smul, ← map_smul, h, map_zero])))

end module

end CategoryTheory.Limits.Concrete

/-! ## Can we apply the above for `ModuleCat`? -/

namespace ModuleCat

open CategoryTheory CategoryTheory.Limits BundledHomCategory
variable {R : Type*} [Ring R]

theorem cokernel_π_imageSubobject_ext' {L M N : ModuleCat.{v} R} (f : L ⟶ M) [HasImage f]
    (g : (imageSubobject f : ModuleCat.{v} R) ⟶ N) [HasCokernel g] {x y : N} (l : L)
    (w : x = y + hom g (factorThruImageSubobject f l)) : hom (cokernel.π g) x = hom (cokernel.π g) y := by
  subst w
  simp

end ModuleCat

[Anne Baanen]

The main drawback I see here is an extra level of indirection on the hom field of the class, so hom (ofHom f) isn't reducibly defeq to f anymore:

-- Current setup with #19511 reduces.
example (M N : ModuleCat.{v} R) (f : M →ₗ[R] N) :
    ModuleCat.Hom.hom (ofHom f : M ⟶ N) = f := by
  with_reducible rfl

-- Indirection via a typeclass doesn't reduce.
example (M N : ModuleCat.{v} R) (f : M →ₗ[R] N) :
    BundledHomCategory.hom (BundledHomCategory.ofHom f : M ⟶ N) = f := by
  fail_if_success with_reducible rfl
  with_reducible_and_instances rfl -- We need one step higher on the reducibility ladder.

[Anne Baanen]

There's also the verbose boilerplates of the variable lines:

variable {C : Type u} [Category.{v} C] (carrier : C → Type (max t w))
variable {FC : C → C → Type*} [∀ X Y, FunLike (FC X Y) (carrier X) (carrier Y)]
variable [BundledHomCategory C FC carrier]

But this is only necessary when working in generality over concrete categories, and hopefully we can upgrade the elementwise metaprograms for generating most of that from abstract categorical statements.

[Anne Baanen]

I'm happily surprised that deriving ConcreteCategory from BundledHomCategory doesn't cause any interop issues with existing bits of the library, like for colimit_rep_eq_iff_exists', colimit_rep_eq_zero' and colimit_no_zero_smul_divisor'.

[Kim Morrison]

I'm in favour!

[Kim Morrison]

I wonder if we should push the AlgebraCat/ModuleCat refactor a bit further first, though.

[Christian Merten]

CommRingCat and co. are in the works ...

[Anne Baanen]

Indeed, I might well be missing some issue that lurks in a very different category (topological spaces?)

[Anne Baanen]

On the other hand, the more we continue on the existing path, the more .homs we'll need to turn into hom _s. :)

[Kim Morrison]

CommRingCat is definitely the next most important example. If we want "coverage", then TopCommRingCat is good for having many typeclasses.

[Christian Merten]

With CommRingCat I am now running into two major obstacles:

• The first one I think is caused by the existence of ConcreteCategory.instFunLike, see https://github.com/leanprover-community/mathlib4/pull/19757/files#r1872319971. I think to work around that we would need lemmas like

lemma CommRingCat.forget_map_apply {R S : CommRingCat} (f : R ⟶ S)
    (x : (CategoryTheory.forget CommRingCat).obj R) :
    @DFunLike.coe _ _ _ ConcreteCategory.instFunLike f x = f x :=
  rfl

to go back and forth between DFunLike.coe f x and f.hom x. But this is painful. Instead I think it is worth a try to replace ConcreteCategory.instFunLike by a CoeFun.

• The second one is similar to the one @Anne Baanen experienced with ModuleCat: In file#Mathlib/Topology/Sheaves/CommRingCat we have the following:

/-- A subpresheaf with a submonoid structure on each of the components. -/
structure SubmonoidPresheaf [∀ X : C, MulOneClass X] [∀ X Y : C, MonoidHomClass (X ⟶ Y) X Y]
    (F : X.Presheaf C) where
  obj : ∀ U, Submonoid (F.obj U)
  map : ∀ {U V : (Opens X)ᵒᵖ} (i : U ⟶ V), obj U ≤ (obj V).comap (F.map i)

variable {F : X.Presheaf CommRingCat.{w}} (G : F.SubmonoidPresheaf)

But of course now, this no longer works because there is no MonoidHomClass on X ⟶ Y for X Y : CommRingCat anymore. So either we try out Anne's BundledHomCategory approach or do the cheap trick and specialize to CommRingCat again.

[Christian Merten]

Maybe also the first point is best solved by BundledHomCategory: delete ConcreteCategory.instFunLike (with no replacement) and reformulate all declarations depending on it in terms of BundledHomCategory. In this way, (forget C).map f x no longer appears in general lemmas, but always directly the correct hom f x.

[Anne Baanen]

Based on my ModuleCat experience, that first class of issue is best fixed for now by adding a change/have statement to punch through the defeq between hom and ConcreteCategory.instFunLike all at once. (Relying on defeq to do rewriting, essentially.)

In the longer term we should find a way to get rid of the fact that we state a lot of results in the language of that instFunLike but the actual coercions from morphisms to functions don't invoke that instance. So either we redefine ConcreteCategory to unbundle FunLike from it (meaning we can pass in the FunLike that we actually want), we redefine the ConcreteCategory instances so they at least reduce to the hom projections, or as you say we avoid talking about the forgetful functor and use something like BundledHomCategory instead.

[Anne Baanen]

I discussed something like this previously with Johan, about dealing with the mismatch between docs#CategoryTheory.Bundled.coeSort and docs#CategoryTheory.ConcreteCategory.hasCoeToSort by unbundling the coercion from ConcreteCategory. There I concluded that this does not help enough since the coercion would get unfolded for specific categories but we'd end up with CoeSort.coe for the generic lemmas. For coercion to functions that issue does not exist as long as we can ensure that we end up with FunLike.coe everywhere.

[Anne Baanen]

For the second issue: rg '(Hom|Map)Class .* ⟶' suggests the one you point out is the only remaining case where we want to assume morphisms satisfy a HomClass. So if we do decide to go for specialization, that would be the last of it and we'd only have to touch those three cases (ZeroHomClass and LinearMapClass in the ModuleCat.Hom refactor, and RingHomClass now).

[Anne Baanen]

Anne Baanen said:

Based on my ModuleCat experience, that first class of issue is best fixed for now by adding a change/have statement to punch through the defeq between hom and ConcreteCategory.instFunLike all at once. (Relying on defeq to do rewriting, essentially.)

I pushed a commit to your branch doing this for RingedSpace, feel free to modify or revert.

[Christian Merten]

Anne Baanen said:

In the longer term we should find a way to get rid of the fact that we state a lot of results in the language of that instFunLike but the actual coercions from morphisms to functions don't invoke that instance. So either we redefine ConcreteCategory to unbundle FunLike from it (meaning we can pass in the FunLike that we actually want), we redefine the ConcreteCategory instances so they at least reduce to the hom projections, or as you say we avoid talking about the forgetful functor and use something like BundledHomCategory instead.

I like the "modify ConcreteCategory idea". Maybe we could add a field coeFun with default value the one induced from (forget C).map and a proof field that the passed coeFun agrees with the default one.

[Christian Merten]

Then when working in a general setting, one could even locally add @[simp] to the proof field.

[Anne Baanen]

I tried implementing the BundledHomCategory class above to replace ConcreteCategory (renaming the current ConcreteCategory as HasForget), see branch#redesign-ConcreteCategory

[Anne Baanen]

It seems to go smoother than introducing the Hom structures, although I didn't get very far down (goal is to get Mathlib.Topology.Sheaves.CommRingCat building so I can experiment with sheaves on concrete categories)

[Anne Baanen]

The last few days I was looking at one issue in ModuleCat.Hom, which is that the type synonym docs#ModuleCat.restrictScalars gets unfolded more eagerly by the ofHom constructor. That lead to missing and conflicting instances, which we worked around by adding more type hints, see for example in docs#ModuleCat.semilinearMapAddEquiv on line 132.

Inserting explicit maps between M and (restrictScalars f).obj M is not quite enough, since the unfolding happens by the ofHom constructor before the toFun field of a linear map is elaborated. So the solution seems to require making restrictScalars irreducible, which I did by wrapping it in a structure: #19941. The problem I found with the PR is that the defeq M = (restrictScalars f).obj M is used implicitly a lot when working with (pre)sheaves of modules over (pre)sheaves of rings, since the restriction maps on rings give rise to restrictScalars on the modules involved. All of these implicit identifications now have to be done by explicit natural isomorphisms. In the end, I made such a mess that I don't believe this change is worth it in the current form.

[Anne Baanen]

One way to go forward might be to redesign (pre)sheaves of modules so they bundle the ring together with the module. If I understand it correctly, this means we remember an (explicit) isomorphism of the bundled ring in the module presheaf with the ring from the presheaf.

@Joël Riou, you appear to be the main author of sheaves of modules, do you think a refactor in this way is something we should be working towards?

[Joël Riou]

Anne Baanen said:

One way to go forward might be to redesign (pre)sheaves of modules so they bundle the ring together with the module. If I understand it correctly, this means we remember an (explicit) isomorphism of the bundled ring in the module presheaf with the ring from the presheaf.

Joël Riou, you appear to be the main author of sheaves of modules, do you think a refactor in this way is something we should be working towards?

No, this does not seem reasonable to me. The situation was already greatly improved when I refactored the definition to define a presheaf of modules as a bunch of objects in various ModuleCat categories. (Making restrictScalars.obj a little bit less prone to dsimp, and encouraging the use of explicit tautological isomorphisms would be ok with me, but making it irreducible seems a little bit too extreme for me.)
(If someone really wants to do a refactor of presheaves of modules, the better generality would be to take an abstract pseudofunctor F from a category J to the 2-category of categories (e.g. given a presheaf of rings R, this could be the pseudofunctor which sends j : J to the category of modules over R.obj j, along with the restriction of scalars functors, etc), so that we may define a category whose objects are families of objects in F.obj j, with "restriction" maps, etc. Then, presheaves of modules would be a particular case of this construction. Working with a general pseudofunctor would make it impossible to "abuse" defeq.)
But, at some point, I believe we should stop doing redesigns and making more mathematical developments with the existing definitions.

[Anne Baanen]

Okay! Since only inserting the explicit maps doesn't help much, then I'll close #19941 as not worth it. Thanks for the detailed explanation!