old/new structures

Stream: mathlib4

[Kevin Buzzard]

I'm not very good at old / new structures, so advice would be appreciated on this issue showing up in CategoryTheory.Bicategory.Functor.

Lean 3:

set_option old_structure_cmd true

namespace category_theory
...
structure prelax_functor
  (B : Type u₁) [quiver.{v₁+1} B] [∀ a b : B, quiver.{w₁+1} (a ⟶ b)]
  (C : Type u₂) [quiver.{v₂+1} C] [∀ a b : C, quiver.{w₂+1} (a ⟶ b)] extends prefunctor B C :=
(map₂ {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g))

#check category_theory.prelax_functor.map -- a thing

Lean 4:

namespace CategoryTheory

structure PrelaxFunctor (B : Type u₁) [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)]
  (C : Type u₂) [Quiver.{v₂ + 1} C] [∀ a b : C, Quiver.{w₂ + 1} (a ⟶ b)] extends
  Prefunctor B C where
  zipWith {a b : B} {f g : a ⟶ b} : (f ⟶ g) → (map f ⟶ map g)

#check PrelaxFunctor.toPrefunctor -- a thing
#check Prefunctor.map -- a thing
-- #check PrelaxFunctor.map -- not a thing

There are lemmas in the file using PrelaxFunctor.map -- do I just add it and align, or is there a good reason why it's not there?

[Kevin Buzzard]

#check PrelaxFunctor.map -- unknown constant

def PrelaxFunctor.map := 37 -- invalid declaration name: structure 'PrelaxFunctor' has field 'map'

:cry:

[Kevin Buzzard]

Is PrelaxFunctor.map there or not??

[Johan Commelin]

I don't completely understand how Lean works here. But if you have F : PrelaxFunctor B C, then F.map is Prefunctor.map F.

[Johan Commelin]

So it sorta inherits Prefunctor.map, for some practical purposes, but as you noticed, it doesn't become an actual declaration or name.

[Kevin Buzzard]

Ha! I just managed to get to_prefunctor_map {X Y : B} : @Prefunctor.map B _ C _ F X Y = F.map compiling, and now I discover it's a syntactic tautology! So PrelaxFunctor.map is now somehow inaccessible. Are we using these tricks with the ring_hom_class set-up?

[Johan Commelin]

I'm still terribly confused about how funlike is supposed to work in Lean 4.

[Johan Commelin]

I wouldn't be surprised if we'll have to rethink several parts of the algebraic hierarchy in a fundamental way after the port is done

[Kevin Buzzard]

Oh! mathlib3port has changed the name of the structure field prelax_functor.map₂ to PrelaxFunctor.zipWith! Was this intentional?

[Rémy Degenne]

I also saw map₂ changed to zipWith in !4#2269 (Topology.UniformSpace.Completion) for cpkg.map₂. I changed it back to map₂ to make it work.

[Reid Barton]

I mean mathport is a program, so I guess it doesn't do things unintentionally

[Johan Commelin]

On the other hand, the authors of mathport probably didn't intend this...

[Johan Commelin]

rg "#align.*map₂.*zip" gives

Mathlib/Init/Data/List/Lemmas.lean
21:#align list.length_map₂ List.length_zipWith

Mathlib/Init/Data/List/Basic.lean
45:#align list.map₂ List.zipWith

Mathlib/Data/List/Basic.lean
1947:#align list.nil_map₂ List.nil_zipWith
1950:#align list.map₂_nil List.zipWith_nil
1960:#align list.map₂_flip List.zipWith_flip
4441:#align list.map₂_left_eq_map₂ List.map₂Left_eq_zipWith
4480:#align list.map₂_right_eq_map₂ List.map₂Right_eq_zipWith

[Kevin Buzzard]

I'll change zipWith back to map2 for this field.

[Johan Commelin]

I'll look into those #misaligns and PR a fix

[Johan Commelin]

Hmm, those aren't actually misaligned.

[Johan Commelin]

@Reid Barton I guess this is fixed by the upcoming changes to mathport? Is the current version still doing some wacky name-suffix juggling?

[Mario Carneiro]

The reason it does this is because of the heuristic it is currently using to guess what dot-notation fields could be referring to. It sees (bla bla).map₂ and it says "I don't know what something.map₂ is being referenced, but I do know that list.map₂ exists and was renamed to List.zipWith so maybe it's that"

[Mario Carneiro]

The best way to fix this is the more accurate dot-notation name resolution that @Reid Barton was working on