porting multiequalizers

Stream: mathlib4

[Adam Topaz]

If anyone is bored, the following porting PR still has a few sorries to take care of (and I have to run for a little while): !4#2786

[Adam Topaz]

This is the last dependency we need for the grothendieck topologies file :)

[Kevin Buzzard]

I've just done 7 hours of project orals so this would be a welcome break :-)

[Kevin Buzzard]

Trying to debug failing simp calls is really annoying when simp only [X] can do nothing without erroring. Did nobody open an issue for this in core? When is it ever a good thing to have simp silently do nothing and not let the user know? I can only see "who cares" situations and "this is annoying" situations

[Kevin Buzzard]

Right now I am deciding whether to go down the rabbithole of working out why a simp is failing or whether I should just copy the output of mathlib3 squeeze_simp and move on (i.e. I've fixed the first sorry but I want to know why simp was failing anyway)

[Kevin Buzzard]

lean4#2145 FWIW. I think that what's going on in this file is that we have a non-confluent simp set and we were just lucky in mathlib3 (the first sorry Adam left is where simp worked in mathlib3 but not in mathlib4). I'm trying to confluentize it (so basically I have been totally derailed :-) )

[Kevin Buzzard]

OK so moving on, in mathlib3 category_theory.limits.shapes.products we have

/-- A cofan over `f : β → C` consists of a collection of maps from every `f b` to an object `P`. -/
@[simps]
def cofan.mk {f : β → C} (P : C) (p : Π b, f b ⟶ P) : cofan f :=
{ X := P,
  ι := { app := λ X, p X.as } }

and @[simps?] tells me that this generates

cofan.mk_ι_app :
  ∀ {β : Type u_1} {C : Type u_3} [_inst_1 : category C] {f : β → C} (P : C) (p : Π (b : β), f b ⟶ P)
  (X : discrete β), (cofan.mk P p).ι.app X = p X.as

In mathlib4 we have

@[simps]
def Cofan.mk {f : β → C} (P : C) (p : ∀ b, f b ⟶ P) : Cofan f
    where
  pt := P
  ι := Discrete.natTrans (fun X => p X.as)

and whatsnew in tells me that this generates

CategoryTheory.Limits.Cofan.mk_ι.{w, v, u} {β : Type w} {C : Type u} [inst✝ : Category C] {f : β → C} (P : C)
  (p : (b : β) → f b ⟶ P) : (Cofan.mk P p).ι = Discrete.natTrans fun X => p X.as

which doesn't look the same to me. Is this apparent divergence in the behaviour of @[simps] expected behaviour?

[Kevin Buzzard]

Adam Topaz said:

If anyone is bored, the following porting PR still has a few sorries to take care of (and I have to run for a little while): !4#2786

It's sorry-free and pushed :D

[Kevin Buzzard]

I fixed the long lines; what is the current policy regarding giving docstrings to constructors for inductive types? IIRC Reid was arguing that no docstring was better than moronic "it is obbious what this is and I only wrote this docstring to satisfy the linter" docstrings.

[Matthew Ballard]

Don't know if it is official policy. I've been inherit_docing these instead of nolint docBlameing.

[Matthew Ballard]

Previously I was doing the moronic thing

[Matthew Ballard]

Some of the notation in category theory is pretty terse and uninformative. Ideally, I'd like to see something about the fields in the overall docstring.

[Kevin Buzzard]

I think that what Reid was objecting to was people porting stuff they didn't really understand, and adding content-free docstrings just to shut the linter up. Perhaps we can do better here.

[Adam Topaz]

Kevin Buzzard said:

Adam Topaz said:

If anyone is bored, the following porting PR still has a few sorries to take care of (and I have to run for a little while): !4#2786

It's sorry-free and pushed :D

Thanks Kevin! I'm going to start on grothendieck topologies now :)

[Adam Topaz]

This turned out to be quite straightforward: !4#2795

[Adam Topaz]

There was something strange though. On this line if I instead use the slightly more concise

def pullback (f : Y ⟶ X) : J.Cover X ⥤ J.Cover Y
    where
  obj S := S.pullback f
  map f := (Sieve.pullback_monotone _ f.le).hom

then lean complains that I should tag this def as noncomputable and the declarations that follow (pullbackId and pullbackComp) get a strange error:

IR check failed at 'CategoryTheory.GrothendieckTopology.pullbackId._rarg', error: unknown declaration 'CategoryTheory.GrothendieckTopology.pullback'

By writing homOfLE ... instead, lean is perfectly happy.