smart composition of natural transformations

Stream: general

[Dean Young]

I am thinking about how to design a smart composition of natural transformations.

It would be nice if Lean 4 could prove that two natural transformations are eligible for composition on its own, in the background, and that is what this example is about.

See the mwe.txt that I've attached, specifically "MAIN EXAMPLE".

mwe.txt

Does anyone know the correct kind of elaboration to use? ("MAIN EXAMPLE" should be made to work).

Note that this example is minimal since it needs both product and hom of categories in the full definition of •_Cat and ∘_Cat.

[Kyle Miller]

If I'm not mistaken, you're looking for some kind of composition up to coherence. You could take a look at parts of the monoidal category coherence tactic. One part of it is a typeclass-based solution to automatically find isomorphisms between different monoidal expressions that are isomorphic: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/CategoryTheory/Coherence.lean#L163

This is used to make a smart ⊗≫ operator that inserts this isomorphism.

[Dean Young]

Could you explain for me what lift does in this line of thought?

[Dean Young]

oh I see it creates a free structure, and then ...hmm...

[Dean Young]

This is really helpful Kyle thanks.

[Dean Young]

Also, what does a [t : T] do when there is no t : and just the type [T]?
e.g.

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

instance LiftHom_comp {X Y Z : C} [LiftObj X] [LiftObj Y] [LiftObj Z] (f : X ⟶ Y) (g : Y ⟶ Z)
    [LiftHom f] [LiftHom g] : LiftHom (f ≫ g) where
  lift := LiftHom.lift f ≫ LiftHom.lift g

[Dean Young]

I can't tell why it's necessary

[Eric Wieser]

[T] just means [_inst_<some_generated_name> : T]

[Kyle Miller]

If you want a reference that'll help you learn some basic notions like using typeclasses, recently Mathematics in Lean has been updated for Lean 4.

[Dean Young]

Right now with this I get

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  category.Cmp C ?m.32817 ?m.32818 ?m.32820 ?m.32821 (category.Cmp C ?m.32818 ?m.32819 ?m.32820 ?m.32822 ?m.32823)
C: category
WXYZ: C.Obj
f: category.Hom C W X
g: category.Hom C X Y
h: category.Hom C Y Z
⊢ (h∘_(C)g∘_(C)f∘_(C)𝟙_(C) W) = (h∘_(C)𝟙_(C) Y∘_(C)g)∘_(C)f

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact C.Idn X

def Ass (C : category) {W:C.Obj} {X:C.Obj} {Y:C.Obj} {Z:C.Obj} {f:C.Hom W X} {g:C.Hom X Y} {h:C.Hom Y Z}  :=
    C.Ass W X Y Z f g h

def Id₁ (C : category) {X:C.Obj} {Y:C.Obj} {f:C.Hom X Y} :=
    (C.Id₁ X Y f)

def Id₂ (C : category) {X:C.Obj} {Y:C.Obj} {f :C.Hom X Y} :=
    Eq.symm (C.Id₂ X Y f)

variable {C : category}
variable {W : C.Obj}
variable {X : C.Obj}
variable {Y : C.Obj}
variable {Z : C.Obj}
variable {f : C.Hom W X}
variable {g : C.Hom X Y}
variable {h : C.Hom Y Z}

def same : (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) ) = (h ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by
(rw [Ass C])
--(rw [Id₁ C])
--repeat (rw [Id₂ C])

Can anyone help me to fix my tactic?

[Notification Bot]

A message was moved here from #mathlib4 > splitting field discussion @ porting meeting by Eric Wieser.

[Eric Wieser]

@Kind Bubble, was this where you meant to post that message?

[Dean Young]

no sorry... I make that mistake often : (

[Dean Young]

@Eric Wieser does this have any sort of simple solution that you see? I want to design a tactic that finds all possible matches for the associativity relation and applies them, so as to right associate the whole thing.

[Scott Morrison]

@Kind Bubble, it's a little hard to see what it is that you want to do. Could you explain the spec of your proposed tactic a bit? And perhaps why you want to work with objects as a structure field for the category rather than a parameter? It might be easier to get help thinking about tactics if you were just using the mathlib setup for category theory rather than rolling your own.

[Dean Young]

@Scott Morrison it would right associate both sides and remove the identity maps involved. I thought that where would be something simple for it since it's not a very complex tactic. I kind of want it to brute force search for all the times it could right associate something in the tree. It's probably a pretty common tactic in algebra ... to do with how an associative initial operation doesn't need parentheses. And then there's one for commutative operations as well.

By learning how to brute force apply the associativity equation I think I could learn lot else, like how to get lean to apply all rewrites of a certain form.

You can take a look at the attached mwe.txt for the "MAIN EXAMPLE" that I want to work. There, I want to use the same trick: remove all identities from a categorical expression involving ∘ and 𝟙 and right associate both, then try reflexivity.

The tricky part seems to be that it doesn't know to apply the rewrite-using-associativity-equation until I supply the full detail of the particular equation (i.e. which objects and morphisms are involved). Maybe you know a way around this already.

So in more detail, I want it to find particular expressions of the form (- ∘_(C) -) ∘_(C) - and switch them all for - ∘_(C) (- ∘_(C) -). Surely there's a simple way to do this

It would be nice to eventually have a vertical composition which "just works".

The monoidal closed category example seems to be a good one but maybe unnecessarily complex for a tactic I consider so basic.

[Mario Carneiro]

rw [foo_assoc] should do that, but perhaps the issue is that the relation here is not equality?

[Dean Young]

I don't understand foo_assoc - it has implicit arguments involved?

[Mario Carneiro]

no, rw takes an unapplied lemma and puts _ for all the missing arguments

[Dean Young]

Here's a closer view of the error I'm trying to fix:

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Id₁ (C : category) {X:C.Obj} {Y:C.Obj} {f:C.Hom X Y} :=
    (C.Id₁ X Y f)

def Id₂ (C : category) {X:C.Obj} {Y:C.Obj} {f :C.Hom X Y} :=
    Eq.symm (C.Id₂ X Y f)

def Ass (C : category) (W:C.Obj)  (X:C.Obj) (Y:C.Obj) (Z:C.Obj) (f:C.Hom W X) (g:C.Hom X Y) (h:C.Hom Y Z)  : Prop :=
    (h ∘_(C) (g ∘_(C) f)) = ((h ∘_(C) g) ∘_(C) f)

def same {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}:
  (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) ) = (h ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) :=
by
rw [←(Ass C)]


/-
tactic 'rewrite' failed, equality or iff proof expected
  Prop
C: category
WXYZ: C.Obj
f: category.Hom C W X
g: category.Hom C X Y
h: category.Hom C Y Z
⊢ (h∘_(C)g∘_(C)f∘_(C)𝟙_(C) W) = (h∘_(C)𝟙_(C) Y∘_(C)g)∘_(C)f
-- can you fix my proof given that it has this error?
-/

[Dean Young]

I got it with your help Mario!

thanks

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g


theorem rewrite_rule₂ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem rewrite_rule₁ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem rewrite_rule₃ {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  (h ∘_(C) (g ∘_(C) f)) = ((h ∘_(C) g) ∘_(C) f) := Eq.symm (C.Ass W X Y Z f g h)

-- The proof of `same` can be completed using these lemmas:
def same {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
  (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) )) = ((i ∘_(C) h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by
  repeat (rw [rewrite_rule₁])

[Dean Young]

does notation work for tactics somehow?

[Dean Young]

Here it is!!!

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g


theorem Id₁ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)

-- The proof of `same` can be completed using these lemmas:
def same {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {A : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z A}:
  (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) )) = ((i ∘_(C) h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by
  repeat (rw [Id₁])
  repeat (rw [Id₂])
  repeat (rw [Ass])

seems so simple but I was just trying to figure out this the whole time... sorry for such a basic question.

[Dean Young]

is it clear to anyone how the above could be made into a "smart composition" for C →_Cat D?

[Scott Morrison]

You can also use simp only [...] to repeatedly apply a lemma. (With some caveats about cases where rw works and simp doesn't, or vice versa.)

[Scott Morrison]

You could certainly define a version of ⊗≫ that instead let you compose natural transformations between compositions of functors that weren't quite associated "correctly". In fact this would be a specialisation of a generalisation (from monoidal categories to bicategories, and then to the bicategory of categories/functors/transformations). You should look to see how ⊗≫ works!

[Joël Riou]

I have just ported part of file where ⊗≫ is defined !4#4610 but I am unable to process the few lines of meta code which appear at the end of CategoryTheory.Bicategory.CoherenceTactic.

[Scott Morrison]

@Joël Riou, if you just leave that commented out I will try to get to it soon. I think nothing downstream actually uses the bicategory tactic, and we've already ported the monoidal one.