## Stream: maths

### Topic: category

#### orlando (Apr 11 2020 at 11:50):

Hello, I'm training on category and i have a problem :sweat_smile:

import category_theory.comma
import category_theory.limits.limits
import category_theory.limits.shapes
import category_theory.yoneda

universes v u
open category_theory
open category_theory.limits
open category_theory.category

variables {C : Type u}
variables [π : category.{v} C]
variables {C} [has_binary_products.{v} C][has_terminal.{v} C]   ---
include π                        ---- what is ? include ?

/
The goal is define group obj in a category.
exemple : in the category of presheaf.
in Ring ? Idem  Agl  etc
context  : π terminal + finite product !
-/
notation f  β :20 g :20 := category_theory.limits.prod.map f g
notation  TC :20 := (terminal C)
notation   TX : 20 := (terminal.from X)
notation f  | :20 g :20 :=  prod.lift f g
structure group_obj {C : Type u}[π : category.{v} C][has_binary_products.{v} C][has_terminal.{v} C] :=  -- I don't understand if i have to write here   {C : Type u}[π : category.{v} C][has_binary_products.{v} C][has_terminal.{v} C]  ?
(X : C)
(ΞΌ : X β¨― X βΆ X)
(inv : X βΆ X)
(Ξ΅ :  T C βΆ X)
(hyp_one_mul  :  (T X | π X) β« (Ξ΅ β π X) β«  ΞΌ  = π X)
(hyp_mul_one  :  (π X | T X) β« ( π X β Ξ΅) β« ΞΌ  = π X)
(hyp_mul_inv  :  (π X | inv) β«  ΞΌ = (T X) β« Ξ΅ )
(hyp_assoc    :  (ΞΌ β π X) β« (ΞΌ) = (prod.associator X X X).hom β« (π X β ΞΌ)  β« ΞΌ )   -- (a *b) * c = (a * (b * c))

variables (G : group_obj C) --- ?    I cant  have i variables of type G : group_obj on C ?
--  (G : group_obj π)(Y : C) :      ?    what is the syntax ?  In fact i don't understand variables with { } [] or () i thinck it's the -- problem ?


#### orlando (Apr 11 2020 at 11:51):

the problem is i cant write  G : group_obj  or  G : group_obj C  or  G : group_obj π) the three possibility give me an error :D

#### Scott Morrison (Apr 11 2020 at 11:53):

You've made the C argument of group_obj implicit, by putting it in curly braces.

#### Mario Carneiro (Apr 11 2020 at 11:53):

You declared all variables as implicit in group_obj, but lean can't infer C

#### Scott Morrison (Apr 11 2020 at 11:53):

You want structure group_obj (C : Type u)[π : category.{v} C]

#### Scott Morrison (Apr 11 2020 at 11:53):

also, since you've included π above, you're going to end up with two copies of the category argument

#### Scott Morrison (Apr 11 2020 at 11:54):

It will explain how and why we use include here.

#### Scott Morrison (Apr 11 2020 at 11:55):

Also, a more general note --- really you want to define a group object in any monoidal category

#### Scott Morrison (Apr 11 2020 at 11:55):

not just in a category equipped with the monoidal structure coming from binary products.

#### Scott Morrison (Apr 11 2020 at 11:55):

I don't promise, but it may actually be _easier_ there.

#### Scott Morrison (Apr 11 2020 at 11:56):

(for one, you won't need to define the notation β, because it will be there for you already!)

#### Kevin Buzzard (Apr 11 2020 at 11:56):

Here's what include does:

variable (X : Type)

def f : β β β := Ξ» x, x + 1

include X

def g : β β β := Ξ» x, x + 1

omit X

def h : β β β := Ξ» x, x + 1

#check f -- f : β β β
#check g -- g : Type β β β β
#check h -- h : β β β


#### Scott Morrison (Apr 11 2020 at 11:56):

(and generally, since the API surface area is smaller for monoidal categories than for monoidal-categories-built-in-this-way, there are fewer ways you can do wrong things :-)

#### Kevin Buzzard (Apr 11 2020 at 11:57):

All your definitions after the include and before the omit will include (X : Type). So if you include $\mathcal{C}$ you shouldn't mention it explicitly in your definition.

#### Kevin Buzzard (Apr 11 2020 at 12:01):

My impression is that when defining new structures you should not rely on variables or include at all, and just spell everything out. It is often the case that for new structures you want the brackets to be different anyway; for example when defining group homs you would want def group_hom (G : Type) [group G] (H : Type) [group H] := ... but then the moment you start proving lemmas about group homs you will want (f : group_hom G H) but {G : Type} {H : Type}.

#### Scott Morrison (Apr 11 2020 at 12:02):

Variables are great once you're off and running and proving a million lemmas.

#### Scott Morrison (Apr 11 2020 at 12:02):

But for defining new structures and new types, please put the hypotheses inline!

#### Kevin Buzzard (Apr 11 2020 at 12:02):

Finally note that in

variables {C : Type u}
variables [π : category.{v} C]
variables {C}


the last variables doesn't do anything. This just means "change the default brackets for variable C to {}" -- but they were already {}.

#### orlando (Apr 11 2020 at 12:04):

thx, Kevin Mario and Scott, i read Slowly ! (i use google traductor to understand :grinning: )

#### orlando (Apr 11 2020 at 12:28):

Scott: Ah, I didn't know the concept of a monoidal category! I just looked at the lean file! Thx !

#### orlando (Apr 11 2020 at 12:29):

I thinck i understand :

import category_theory.comma
import category_theory.limits.limits
import category_theory.limits.shapes
import category_theory.yoneda

universes v u
open category_theory
open category_theory.limits
open category_theory.category

/-
The goal is define group obj in a category.
exemple : in the category of presheaf.
in Ring ? Idem ?
contexte : π a un objet final et a les produit finis !
Pour coder ΞΌ X Γ X βΆ X  We see that has X βΆ T cospan f f)

-/
notation f  β :20 g :20 := category_theory.limits.prod.map f g
notation  TC :20 := (terminal C)
notation   TX : 20 := (terminal.from X)
notation f  | :20 g :20 :=  prod.lift f g
structure group_obj (C : Type u)[π : category.{v} C][has_binary_products.{v} C][has_terminal.{v} C] :=
(X : C)
(ΞΌ : X β¨― X βΆ X)
(inv : X βΆ X)
(Ξ΅ :  T C βΆ X)
(hyp_one_mul  :  (T X | π X) β« (Ξ΅ β π X) β«  ΞΌ  = π X)
(hyp_mul_one  :  (π X | T X) β« ( π X β Ξ΅) β« ΞΌ  = π X)
(hyp_mul_inv  :  (π X | inv) β«  ΞΌ = (T X) β« Ξ΅ )
(hyp_assoc    :  (ΞΌ β π X) β« (ΞΌ) = (prod.associator X X X).hom β« (π X β ΞΌ)  β« ΞΌ )   -- (a *b) * c = (a * (b * c))

-- question 1.
-- Let X : C
variables (C : Type u)
variables [π : category.{v} C]
variables  [has_binary_products.{v} C][has_terminal.{v} C]
include π
instance coee : has_coe (group_obj C) C := β¨Ξ» F, F.Xβ©
variables (G : group_obj C)
include G
def Test_1  := yoneda.obj (G : C)
#check Test_1
omit G
def Test_2 (G : group_obj C) := yoneda.obj (G : C)
#check Test_2
theorem  one_eq_two  :  Test_1  = Test_2 := rfl  !


#### orlando (Apr 11 2020 at 16:18):

The exercice is too difficult for the moment ! It was, to show that for all group objet G et for all  X : C  the set (Yoneda.obj G).obj X)  is a group !

A question : is it complicated to show that Yoneda preserve product ?
:laughing:

import category_theory.comma
import category_theory.limits.limits
import category_theory.limits.shapes
import category_theory.yoneda
import category_theory.opposites
import category_theory.types
import category_theory.limits.shapes
import category_theory.limits.types

universes v u
open category_theory
open category_theory.limits
open category_theory.category
open opposite
namespace TEST
variables {C : Type u}
variables [π : category.{v} C]
variables  [has_binary_products.{v} C][has_terminal.{v} C]
include π
lemma Yoneda_preserve_product (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj( op Y) β  (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y) :=
begin
-- Use unicity of limits ?
-- cone_point_unique_up_to_iso ?
sorry, --- i thinck !
end
end TEST


#### Kevin Buzzard (Apr 11 2020 at 16:41):

Try one of Scott's category theory tactics?

Tidy?

Obviously?

#### Kevin Buzzard (Apr 11 2020 at 16:42):

Maybe you have to define the map?

#### orlando (Apr 11 2020 at 16:44):

Tidy give me :

3 goals
C : Type u,
π : category C,
_inst_1 : has_binary_products C,
_inst_2 : has_terminal C,
B A Y : C,
a : Y βΆ A β¨― B,
j : discrete walking_pair
β’ (pair (Y βΆ A) (Y βΆ B)).obj j

C : Type u,
π : category C,
_inst_1 : has_binary_products C,
_inst_2 : has_terminal C,
Y A B : C,
x : Y βΆ A β¨― B,
j : discrete walking_pair
β’ ?m_1 Y A B β¨Ξ» (j : discrete walking_pair), ?m_2[Y, A, B, x, j], _β© β« limit.Ο (pair A B) j =
x β« limit.Ο (pair A B) j

C : Type u,
π : category C,
_inst_1 : has_binary_products C,
_inst_2 : has_terminal C,
Y A B : C,
x_val : Ξ  (j : discrete walking_pair), (pair (Y βΆ A) (Y βΆ B)).obj j,
x_property : x_val β functor.sections (pair (Y βΆ A) (Y βΆ B)),
x : discrete walking_pair
β’ ?m_2[Y, A, B, ?m_1 Y A B β¨x_val, x_propertyβ©, x] = x_val x


#### Kevin Buzzard (Apr 11 2020 at 16:47):

I have no idea what these tactics do but maybe they are just for proofs. This is data.

#### Kevin Buzzard (Apr 11 2020 at 16:48):

Your lemma is not a lemma, I think?

#### Kevin Buzzard (Apr 11 2020 at 16:48):

def Yoneda_preserve_product (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj( op Y) β  (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y) :=
{! !}


#### orlando (Apr 11 2020 at 16:48):

@Kevin Buzzard i made a mistake ?

#### Kevin Buzzard (Apr 11 2020 at 16:49):

It is in Type, not in Prop

#### Kevin Buzzard (Apr 11 2020 at 16:53):

def Yoneda_preserve_product (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj( op Y) β  (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y) :=
{ hom := prod.lift _ _,
inv := _,
hom_inv_id' := _,
inv_hom_id' := _ }


#### orlando (Apr 11 2020 at 16:58):

hum !!! i try :slight_smile:

#### Kevin Buzzard (Apr 11 2020 at 17:01):

example (A B Y : C) : (yoneda.obj (A β¨― B)).obj (op Y) = (Y βΆ A β¨― B) := rfl

#### Kevin Buzzard (Apr 11 2020 at 17:04):

{ hom := prod.lift
(Ξ» f, f β« category_theory.limits.prod.fst : (Y βΆ A β¨― B) βΆ (Y βΆ A))
(Ξ» f, f β« category_theory.limits.prod.snd : (Y βΆ A β¨― B) βΆ (Y βΆ B)),


Writing category theory Lean for me is about as slow as writing normal Lean was for me in 2017 :-)

#### Kevin Buzzard (Apr 11 2020 at 17:04):

{ hom := prod.lift
(Ξ» f, f β« category_theory.limits.prod.fst)
(Ξ» f, f β« category_theory.limits.prod.snd),


#### Kevin Buzzard (Apr 11 2020 at 17:10):

{ hom := prod.lift
(Ξ» f, f β« category_theory.limits.prod.fst)
(Ξ» f, f β« category_theory.limits.prod.snd),
inv := Ξ» f : (Y βΆ A) β¨― (Y βΆ B), (sorry : Y βΆ (A β¨― B)),
hom_inv_id' := sorry,
inv_hom_id' := sorry }


#### orlando (Apr 11 2020 at 17:17):

Kevin, i make the same with my notation $\mid$

exact  { hom := Ξ» Ο,((Ο β« (category_theory.limits.prod.fst)) |  (Ο β« (category_theory.limits.prod.snd)),
inv := sorry,
hom_inv_id' := _,
inv_hom_id' := _ }


#### orlando (Apr 11 2020 at 17:18):

hum ! not the same !

#### orlando (Apr 11 2020 at 17:19):

normaly it's an obvious thing this Yoneda preserve product :sweat_smile:

#### Kevin Buzzard (Apr 11 2020 at 17:21):

in 2017 I thought it was obvious that $\sqrt{2}\not\in\mathbb{Q}$ :laughing:

#### Kevin Buzzard (Apr 11 2020 at 17:24):

I am looking forward to proving the snake lemma :laughing:

#### Kevin Buzzard (Apr 11 2020 at 17:31):

example (A B Y : C) :
((Y βΆ A) β¨― (Y βΆ B) βΆ (Y βΆ A)) = ((Y βΆ A) β¨― (Y βΆ B) β (Y βΆ A)) := rfl -- fail :-(


#### Kevin Buzzard (Apr 11 2020 at 17:31):

$Hom(Y,A)$ has type Type*, right?

#### Kevin Buzzard (Apr 11 2020 at 17:33):

I have f : (Y βΆ A) β¨― (Y βΆ B) and I want to apply category_theory.limits.prod.fst to get g : Y βΆ A but I can't figure out how to do it :-(

#### orlando (Apr 11 2020 at 17:33):

lemma Yoneda_preserve_produc (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj( op Y) β  (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y) :=
begin
let P := Aβ¨― B,
let Q := (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y),
exact  { hom := (Ξ» Ο, Ο β« (category_theory.limits.prod.fst)) | (Ξ» Ο,(Ο β« (category_theory.limits.prod.snd))),
inv := Ξ» f , prod.lift ( fβ«  category_theory.limits.prod.fst ) (fβ«  category_theory.limits.prod.snd),
hom_inv_id' := _,
inv_hom_id' := _ }
end


Nice!

#### orlando (Apr 11 2020 at 17:34):

i no ! there is ia mistake

#### Kevin Buzzard (Apr 11 2020 at 17:36):

In category_theory.types there is this: @[simp] lemma types_hom {Ξ± Ξ² : Type u} : (Ξ± βΆ Ξ²) = (Ξ± β Ξ²) := rfl

#### Kevin Buzzard (Apr 11 2020 at 17:36):

So I am a bit surprised that my rfl above is failing

#### Kevin Buzzard (Apr 11 2020 at 17:37):

Oh it is a stupid issue with brackets :-/

#### Kevin Buzzard (Apr 11 2020 at 17:37):

example (A B Y : C) :
((Y βΆ A) β¨― (Y βΆ B) βΆ (Y βΆ A)) = (((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ A)) := rfl -- succeeds


#### Kevin Buzzard (Apr 11 2020 at 17:38):

I still don't have the confidence with category theory. With Lean in general, when something doesn't work I usually know why. With category theory I am still not sure.

#### Kevin Buzzard (Apr 11 2020 at 17:41):

OK now I can do it with @ and filling in implicit arguments

#### Kevin Buzzard (Apr 11 2020 at 17:42):

    (prod.lift
((@category_theory.limits.prod.fst _ _ (Y βΆ A) _ _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ A)) f : Y βΆ A)
((@category_theory.limits.prod.snd _ _ (Y βΆ A) _ _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ B)) f : Y βΆ B)),


#### Kevin Buzzard (Apr 11 2020 at 17:42):

49 minutes so far :-)

#### Kevin Buzzard (Apr 11 2020 at 17:43):

gaaargh by obviously doesn't work for the proofs :-/

#### Kevin Buzzard (Apr 11 2020 at 17:49):

  hom_inv_id' := begin
ext f,
cases j,
obviously,
end,


#### Kevin Buzzard (Apr 11 2020 at 17:49):

obviously just killed two goals at once!

#### Kevin Buzzard (Apr 11 2020 at 17:54):

def Yoneda_preserve_product (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj (op Y) β (yoneda.obj A).obj (op Y) β¨― (yoneda.obj B).obj (op Y) :=
{ hom := prod.lift
(Ξ» f, f β« category_theory.limits.prod.fst)
(Ξ» f, f β« category_theory.limits.prod.snd),
inv := Ξ» f : (Y βΆ A) β¨― (Y βΆ B),
(prod.lift
((@category_theory.limits.prod.fst _ _ (Y βΆ A) (Y βΆ B) _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ A)) f)
((@category_theory.limits.prod.snd _ _ (Y βΆ A) _ _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ B)) f : Y βΆ B)),
hom_inv_id' := begin
ext f,
cases j,
{ simp, refl},
{ simp, refl}
end,
inv_hom_id' := begin
ext j,
cases j,
{ sorry},
{ sorry}
end
}


#### Kevin Buzzard (Apr 11 2020 at 17:56):

I think there might be some way of training tidy to solve the first proof.

#### Kenny Lau (Apr 11 2020 at 17:57):

Kevin Buzzard said:

obviously just killed two goals at once!

killing two goals with one tactic

#### orlando (Apr 11 2020 at 18:00):

it's toooooo complicated :scream:

#### Kevin Buzzard (Apr 11 2020 at 18:01):

The category theory library is complicated precisely because not enough people use it, and so @Scott Morrison doesn't have enough data about how to make it better. But it will be better one day.

#### Kevin Buzzard (Apr 11 2020 at 18:05):

But we need to make abelian categories, so we can do homological algebra, so people (e.g. me) are going to have to learn how to use it.

#### orlando (Apr 11 2020 at 18:26):

for hom

lemma Yoneda_preserve_produc (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj( op Y) β  (yoneda.obj A).obj(op Y)  β¨― (yoneda.obj B).obj (op Y) :=
begin
exact  { hom := category_theory.limits.prod.lift
((yoneda.map (category_theory.limits.prod.fst)).app (op Y))   --- app cause it's natural transformation !
((yoneda.map (category_theory.limits.prod.snd)).app (op Y)),


#### Kevin Buzzard (Apr 11 2020 at 18:39):

This is probably better, because the proof I can't do involves using the universal property of limit

#### Kevin Buzzard (Apr 11 2020 at 19:21):

So I can't do it. My goal is

1 goal
C : Type u,
π : category C,
_inst_1 : has_binary_products C,
_inst_2 : has_terminal C,
Y A B : C,
x : (yoneda.obj A).obj (op Y) β¨― (yoneda.obj B).obj (op Y)
β’ prod.lift (Ξ» (f : (yoneda.obj (A β¨― B)).obj (op Y)), f β« prod.fst)
(Ξ» (f : (yoneda.obj (A β¨― B)).obj (op Y)), f β« prod.snd)
(prod.lift (prod.fst x) (prod.snd x)) =
x


and the x is \crossproduct i.e. categorical product, and the prod.lift is the category theory one as well. However these products are occurring in the category Type v so one can check them on components. This is what I don't know how to do using category theory. @Reid Barton ?

#### Kevin Buzzard (Apr 11 2020 at 19:22):

(yoneda.obj A).obj (op Y) is just Y \h A

#### Reid Barton (Apr 11 2020 at 19:26):

Is the categorical product in Type v the ordinary product? What happens if you do cases x?

#### Reid Barton (Apr 11 2020 at 19:26):

It looks like it must be otherwise I can't make sense out of this goal

#### Kevin Buzzard (Apr 11 2020 at 19:26):

annoyingly, it does something really annoying.

#### Kevin Buzzard (Apr 11 2020 at 19:27):

x_val : Ξ  (j : discrete walking_pair), (pair ((yoneda.obj A).obj (op Y)) ((yoneda.obj B).obj (op Y))).obj j,
x_property : x_val β functor.sections (pair ((yoneda.obj A).obj (op Y)) ((yoneda.obj B).obj (op Y)))


oh

#### Reid Barton (Apr 11 2020 at 19:27):

how did you obtain x?

#### Kevin Buzzard (Apr 11 2020 at 19:27):

β’ (prod.lift (Ξ» (f : (yoneda.obj (A β¨― B)).obj (op Y)), f β« prod.fst)
(Ξ» (f : (yoneda.obj (A β¨― B)).obj (op Y)), f β« prod.snd) β
Ξ» (f : (Y βΆ A) β¨― (Y βΆ B)), prod.lift (prod.fst f) (prod.snd f)) =
id


and I went for funext x

#### Kevin Buzzard (Apr 11 2020 at 19:28):

I'm trying to prove that some natural map Hom(Y,A) x Hom(Y,B) -> Hom(Y,A) x Hom(Y,B) is id

#### Reid Barton (Apr 11 2020 at 19:29):

Kevin Buzzard said:

I'm trying to prove that some natural map Hom(Y,A) x Hom(Y,B) -> Hom(Y,A) x Hom(Y,B) is id

If you want to prove that two maps into a category-theory product are equal then you should probably use the API for that

#### Kevin Buzzard (Apr 11 2020 at 19:29):

The map is this: first use the universal property to get Hom(Y,A) x Hom(Y,B) -> Hom(Y,A x B) and then use composition with pr1 and pr2 to get a map the other way. Yes, the products other than A x B are in Type v.

#### Reid Barton (Apr 11 2020 at 19:29):

because that's ultimately the only thing that the API gives you

#### Kevin Buzzard (Apr 11 2020 at 19:29):

I thought that was obviously

#### Reid Barton (Apr 11 2020 at 19:29):

obviously is not the API

Rotten luck.

#### Kevin Buzzard (Apr 11 2020 at 19:30):

I tried to chase the definition of prod back but it was just defined as a limit.

#### Reid Barton (Apr 11 2020 at 19:31):

Hmm does the API for this not actually exist...?

#### Reid Barton (Apr 11 2020 at 19:32):

I just mean the uniqueness part of the universal property. Two maps into X x Y agree if their compositions with X x Y -> X and X x Y -> Y both agree. I haven't used the mathlib products ever, I think.

Right.

#### Reid Barton (Apr 11 2020 at 19:32):

Would that represent progress in your proof?

#### Kevin Buzzard (Apr 11 2020 at 19:33):

I'm hoping it's exactly what I need to finish the proof.

#### Kevin Buzzard (Apr 11 2020 at 19:33):

It's presumably explicitly there for limits

#### Reid Barton (Apr 11 2020 at 19:33):

You built the map using the universal property, so yeah you know when you compose with the map to Hom(Y, A) that it recovers the map you put in, which is (id composed with) the projection.

#### Kevin Buzzard (Apr 11 2020 at 19:34):

I was trying to formalise the math argument involving checking on components, which is OK because everything is in Type so the category product is actually the product. But I'm now not at all sure how equal these things are.

#### Kevin Buzzard (Apr 11 2020 at 19:34):

And if they're just isomorphic then I will never get anywhere without the universal property.

#### orlando (Apr 11 2020 at 19:35):

Ried i don't see the result you mention : " two maps into X x Y agree if their compositions with X x Y -> X and X x Y -> Y both agree. "

#### Reid Barton (Apr 11 2020 at 19:35):

So I guess you want to apply limit.hom_ext and then use cases on the objects of walking_pair.

#### Reid Barton (Apr 11 2020 at 19:35):

orlando said:

Ried i don't see the result you mention : " two maps into X x Y agree if their compositions with X x Y -> X and X x Y -> Y both agree. "

I agree it seems to be missing

#### Reid Barton (Apr 11 2020 at 19:35):

Obviously the library should already provide this for you

#### Reid Barton (Apr 11 2020 at 19:36):

https://github.com/b-mehta/topos/blob/master/src/binary_products.lean#L29
from the topos project

#### Kevin Buzzard (Apr 11 2020 at 19:36):

@orlando you found a hole :-)

#### Kevin Buzzard (Apr 11 2020 at 19:37):

Good spot Reid :-)

#### Reid Barton (Apr 11 2020 at 19:41):

I even gave the correct proof :innocent:

#### Bhavik Mehta (Apr 11 2020 at 22:06):

Ah yeah this is a super useful result! It is pretty much the same thing as apply limit.hom_ext, cases j but it's nice to have a name for it like we did

PR!

#### orlando (Apr 12 2020 at 08:49):

Kevin Buzzard said:

Your lemma is not a lemma, I think?

Ok @Kevin Buzzard I just understood now your remark :joy: 12 hours later ! I really slow !!!

#### Kevin Buzzard (Apr 12 2020 at 10:18):

lemma prod.lift_fst {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.fst = f :=
limit.lift_Ο (binary_fan.mk f g) _

lemma prod.lift_snd {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.snd = g :=
limit.lift_Ο (binary_fan.mk f g) _


#### Kevin Buzzard (Apr 12 2020 at 10:23):

import category_theory.comma
import category_theory.limits.limits
import category_theory.limits.shapes
import category_theory.yoneda
import category_theory.opposites
import category_theory.types
import category_theory.limits.shapes
import category_theory.limits.types

universes v u
open category_theory
open category_theory.limits
open category_theory.category
open opposite
namespace TEST
variables {C : Type u}
variables [π : category.{v} C]
variables  [has_binary_products.{v} C][has_terminal.{v} C]
include π

lemma prod.hom_ext {Y A B : C} {a b : Y βΆ A β¨― B} (h1 : a β« limits.prod.fst = b β« limits.prod.fst) (h2 : a β« limits.prod.snd = b β« limits.prod.snd) : a = b :=
begin
apply limit.hom_ext,
rintros (_ | _),
simpa,
simpa
end

lemma prod.lift_fst {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.fst = f :=
limit.lift_Ο (binary_fan.mk f g) _

lemma prod.lift_snd {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.snd = g :=
limit.lift_Ο (binary_fan.mk f g) _

def Yoneda_preserve_product (Y : C)(A B : C) :
(yoneda.obj (A β¨― B)).obj (op Y) β (yoneda.obj A).obj (op Y) β¨― (yoneda.obj B).obj (op Y) :=
{ hom := prod.lift
(Ξ» f, f β« category_theory.limits.prod.fst)
(Ξ» f, f β« category_theory.limits.prod.snd),
inv := Ξ» f : (Y βΆ A) β¨― (Y βΆ B),
(prod.lift
((@category_theory.limits.prod.fst _ _ (Y βΆ A) (Y βΆ B) _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ A)) f)
((@category_theory.limits.prod.snd _ _ (Y βΆ A) _ _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ B)) f : Y βΆ B)),
hom_inv_id' := begin
ext f,
cases j,
{ simp, refl},
{ simp, refl}
end,
inv_hom_id' := begin
apply prod.hom_ext,
{ rw assoc, rw prod.lift_fst, obviously},
{ rw assoc, rw prod.lift_snd, obviously}
end
}

end TEST


#### orlando (Apr 12 2020 at 10:25):

@Kevin Buzzard : your lemmas is exactly what i need !!!! I was asking me where is the lemma :

 lemma prod.first (A B X : C)(f :X βΆ A)(g : X βΆ B) : limits.prod.lift f g  β« limits.prod.fst = f := begin
obviously,
sorry,
end


If think it's good !

#### Kevin Buzzard (Apr 12 2020 at 10:26):

prod.hom_ext and prod.lift_fst and prod.lift_snd were all missing from the API, although no doubt the experts will say not to put in prod.lift_fst because "it is in there already" (as limit.lift_Ο). I am not so sure though. First, I needed to rewrite with it (which I can't do with limit.lift_\pi) and secondly it might require the user of prod to know about binary_fan.mk which I feel is not something which an end user needs to know about.

#### Markus Himmel (Apr 12 2020 at 10:31):

erw limit.lift_Ο would most likely have worked

#### Markus Himmel (Apr 12 2020 at 10:32):

But I agree that these lemmas would be a nice addition

#### Kevin Buzzard (Apr 12 2020 at 10:35):

prod and prod.fst etc are all defined as abbreviations. It says that erewrite unfolds semireducible definitions. It also unfolds abbreviations?

#### Kevin Buzzard (Apr 12 2020 at 10:35):

! even rw works!

#### Markus Himmel (Apr 12 2020 at 10:37):

In fact, in your code above, you can leave out the rw prod.lift_fst entirely and obviously will still handle it

#### Markus Himmel (Apr 12 2020 at 10:38):

You don't need the rw assoc either

#### Kevin Buzzard (Apr 12 2020 at 10:41):

as long as you have about 5 minutes to spare! You're right!

#### Scott Morrison (Apr 12 2020 at 10:49):

I think we should add all those lemmas!

#### Kevin Buzzard (Apr 12 2020 at 10:50):

I'm making a PR. You want all three?

#### Scott Morrison (Apr 12 2020 at 10:50):

Also, we should add more specific instances for has_products and has_binary_products for all the concrete categories (including Type), which give you want you would definitionally expect.

#### Scott Morrison (Apr 12 2020 at 10:50):

We should check the other special shapes, too.

#### Kevin Buzzard (Apr 12 2020 at 10:50):

I never figured out how to convince Lean that X \crossproduct Y was X \times Y if X Y : Type.

#### Scott Morrison (Apr 12 2020 at 10:50):

But if however far you get with the initial PR, we can look for those later.

#### Scott Morrison (Apr 12 2020 at 10:51):

Well, at the moment it isn't, definitionally.

#### Kevin Buzzard (Apr 12 2020 at 10:51):

Indeed, I half-suspect it's not true, or hard, or whatever

#### Scott Morrison (Apr 12 2020 at 10:51):

Or rather, it only is up to an equiv at the moment.

#### Scott Morrison (Apr 12 2020 at 10:51):

But we can make it definitional.

#### Scott Morrison (Apr 12 2020 at 10:51):

(Note that in some ways this is dangerous --- it allows/encourages people to break through the API. :-)

#### Kevin Buzzard (Apr 12 2020 at 10:51):

I'm out of my depth here, but it did make me go on a wild goose chase with the question.

#### Kevin Buzzard (Apr 12 2020 at 10:52):

I assumed I'd need it; I hadn't realised I could prove what I wanted in a purely arrow-theoretic way

#### Markus Himmel (Apr 12 2020 at 10:52):

Scott Morrison said:

We should check the other special shapes, too.

The biproducts PR also does not have these lemmas

#### Kevin Buzzard (Apr 12 2020 at 11:13):

feat(category_theory/limits/shapes/binary_products):


"2 CHARACTERS OVER 50 IN CURRENT LINE"

:-/

#2396

#### orlando (Apr 12 2020 at 14:53):

hum i don't know if it's somewhere but we have :

lemma prod.lift_comp{Z' Z A B : C}(h : Z' βΆ Z)(f : Z βΆ A)(g : Z βΆ B)  : (h β« (f | g) ) = ((h β« f) | h β« g) := begin
apply prod.hom_ext,
rw assoc,
rw prod.lift_fst,
rw prod.lift_fst,
rw prod.lift_snd,
rw assoc,
rw prod.lift_snd,
end


#### Bhavik Mehta (Apr 12 2020 at 15:10):

This isn't there, I think it should be! (and similar on the other side)

#### Kevin Buzzard (Apr 12 2020 at 15:39):

I can add this to the PR. The | notation is orlando's I think; it might be worth getting Scott's input on this.

#### Bhavik Mehta (Apr 12 2020 at 18:31):

I would find some sort of notation for prod.lift useful, no strong preference on what it is

#### orlando (Apr 13 2020 at 12:34):

Hello, i make a tatic for product but i have a problem it's seem to bug when there is a  rw β  The code is a little long !

import category_theory.limits.limits
import category_theory.limits.shapes
import category_theory.yoneda
import category_theory.opposites
import category_theory.types
import category_theory.limits.types

run_cmd mk_simp_attr PRODUCT    -----  BOF BOF
meta def PRODUCT_CAT  : tactic unit :=
[  try {simp only with PRODUCT}]

universes v u
open category_theory
open category_theory.limits
open category_theory.category
open opposite
namespace lem
variables {C : Type u}
variables [π : category.{v} C]
variables  [has_binary_products.{v} C][has_terminal.{v} C]
include π
attribute [PRODUCT] category.assoc category.id_comp category.comp_id
@[PRODUCT] lemma prod_left_def {X Y : C} : limit.Ο (pair X Y) walking_pair.left = limits.prod.fst := rfl
@[PRODUCT] lemma prod_right_def {X Y : C} : limit.Ο (pair X Y) walking_pair.right = limits.prod.snd := rfl
lemma prod.hom_ext {A X Y : C} {a b : A βΆ X β¨― Y} (h1 : a β« limits.prod.fst = b β« limits.prod.fst) (h2 : a β« limits.prod.snd = b β« limits.prod.snd) : a = b :=
begin
apply limit.hom_ext,
rintros (_ | _),
rw prod_left_def,
exact h1,
rw prod_right_def,
exact h2,
end
@[PRODUCT]lemma prod.lift_fst {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.fst = f :=
limit.lift_Ο (binary_fan.mk f g) _

@[PRODUCT]lemma prod.lift_snd {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.snd = g :=
limit.lift_Ο (binary_fan.mk f g) _
end lem

notation f  β :20 g :20 := category_theory.limits.prod.map f g  ---- 20
notation  TC :20 := (terminal C)
notation   TX : 20 := (terminal.from X)
notation f  | :20 g :20 :=  prod.lift f g
notation Ο1 := limits.prod.fst
notation Ο2 := limits.prod.snd

variables {C : Type u}
variables [π : category.{v} C]
variables [has_binary_products.{v} C][has_terminal.{v} C]
include π
variables (X :C)
open lem
/-
Ο notation for projection
-/
@[PRODUCT]lemma ex_1 {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : ( f | g) β« Ο1 = f  :=   prod.lift_fst f g
/-
we can type Ο : A β¨― B βΆ B if we need
-/
@[PRODUCT]lemma ex_2 {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : ( f | g) β« (Ο2 : A β¨― B βΆ B) = g := prod.lift_snd f g

@[PRODUCT]lemma ex_3 {A X Y : C} {a b : A βΆ X β¨― Y} (h1 : a β« Ο1  = b β« Ο1 ) (h2 : a β« Ο2  = b β« Ο2)  : a = b :=  prod.hom_ext h1 h2

@[PRODUCT]lemma prod.left_composition{Z' Z A B : C}(h : Z' βΆ Z)(f : Z βΆ A)(g : Z βΆ B)  :
h β« (f | g)  = (h β« f | h β« g) :=
begin
apply prod.hom_ext,   --- Le right member is of the form ( | )  composition Ο1 Ο2
PRODUCT_CAT,  PRODUCT_CAT,  --- here assoc
-- rw assoc,
-- rw prod.lift_fst,
-- rw prod.lift_fst,
-- rw prod.lift_snd,
-- rw assoc,
-- rw prod.lift_snd,
end

@[PRODUCT]lemma prod.map_first{X Y Z W : C}(f  : X βΆ Y)(g  : Z βΆ W) :  (f β g) β« (Ο1 : Y β¨― W βΆ Y) = Ο1  β« f :=  begin
exact limit.map_Ο (map_pair f g) walking_pair.left,
end
@[PRODUCT]lemma prod.map_second{X Y Z W : C}(f  : X βΆ Y)(g  : Z βΆ W) :  (f β g) β« Ο2 = Ο2 β« g :=  begin
exact limit.map_Ο (map_pair f g) walking_pair.right,
end
@[PRODUCT]lemma  prod.otimes_is_prod {X Y Z W : C}(f  : X βΆ Y)(g  : Z βΆ W) : (f β g) = ( Ο1  β« f | Ο2 β« g ) := begin
apply prod.hom_ext,
PRODUCT_CAT, PRODUCT_CAT,
-- rw prod.lift_fst,
-- rw prod.map_first,
-- rw prod.lift_snd,
-- rw prod.map_second,
end
-- notation Ο1(X x Y) := (limits.prod.fst : Xβ¨―Y βΆ X)
@[PRODUCT]lemma prod.map_ext{X Y Z W : C}(f1 f2  : X βΆ Y)(g1 g2  : Z βΆ W) :  (f1 β g1) = (f2 β g2) β
(Ο1 : X β¨― Z βΆ X) β« f1 = (Ο1 : X β¨― Z βΆ X)  β« f2 := Ξ» certif, begin
iterate 2 {rw prod.otimes_is_prod at certif},
rw β prod.map_first ( f1)  (g1),
rw β prod.map_first ( f2)  (g2),
iterate 2 {rw prod.otimes_is_prod},
rw certif,
end
@[PRODUCT]lemma destruction {X Y Z : C} (f :  Y βΆ X) (g : X βΆ Z ) :
(f | π Y) β« (g β (π Y)) = (f β« g | π Y) := begin
apply prod.hom_ext,
-- PRODUCT_CAT,PRODUCT_CAT,     ---------------------- PROBLEME With the tatict HEEEEEEERRRRRRE
rw [prod.lift_fst],
rw  assoc,
rw prod.map_first,
rw β assoc,               ----- β assoc here  Problem ?
rw prod.lift_fst,
tidy, -- super - power tidy
end

def Y (R : C)(A :C) := (yoneda.obj A).obj (op R)
def Y_ (R : C) {A B : C}(Ο : A βΆ B) := ((yoneda.map Ο).app (op R) : Y R A βΆ Y R B)
-- Good notation for yoneda stuff :
-- We fix V : C and we denote by
-- R[X] := yoneda.obj X).obj (op R) and Ο : A  βΆ B (in C) R β¦  Ο β§   : R[A] β R[B]  in type v
notation R[A]:20 := Y R A  -- notation ??
notation R<Ο> :20   := Y_ R Ο  --
def Yoneda_preserve_product (Y : C)(A B : C) :
Y[A β¨― B] β Y[A] β¨― Y[B] :=
{ hom := prod.lift
(Ξ» f, f β« Ο1)
(Ξ» f, f β« Ο2),
inv := Ξ» f : (Y βΆ A) β¨― (Y βΆ B),
(prod.lift
((@category_theory.limits.prod.fst _ _ (Y βΆ A) (Y βΆ B) _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ A)) f)
((@category_theory.limits.prod.snd _ _ (Y βΆ A) _ _ : ((Y βΆ A) β¨― (Y βΆ B)) β (Y βΆ B)) f : Y βΆ B)),
hom_inv_id' := begin
ext f,
cases j,
{ simp, refl},
{ simp, refl}
end,
inv_hom_id' := begin
apply lem.prod.hom_ext,
{ rw assoc, rw lem.prod.lift_fst, obviously},
{ rw assoc, rw lem.prod.lift_snd, obviously}
end
}

--- Here it just sugar
@[PRODUCT]lemma yoneda_sugar.composition (R : C) {X Y Z : C} (f : X βΆ Y) (g : Y βΆ Z) : R < f β« g > =( R< f >) β« (R < g >)
:=  begin
unfold Y_,
simp,
end
def yoneda_sugar.conv {R : C}{A : C}(g : R[A]) : R βΆ A := g
def yoneda_sugar.prod (R : C)(A B : C) : R[A β¨― B] β R[A] β¨― R[B] := begin
exact Yoneda_preserve_product R A B,
end
@[PRODUCT]lemma yoneda_sugar.prod.hom (R : C)(A B : C) :
(yoneda_sugar.prod R A B).hom =  (R < (limits.prod.fst : A β¨― B βΆ A) > | R < (limits.prod.snd : A β¨― B βΆ B)> ) := rfl

@[PRODUCT]lemma yoneda_sugar.prod.first (R : C)(A B : C) :
(yoneda_sugar.prod R A B).hom β« limits.prod.fst = (R < limits.prod.fst >) :=
begin
exact rfl,
end
@[PRODUCT]lemma yoneda_sugar.prod.hom_inv (R : C)(A B : C) :
(yoneda_sugar.prod R A B).hom β« (yoneda_sugar.prod R A B).inv = π (R[ A β¨― B]) :=
(Yoneda_preserve_product R A B).hom_inv_id'
@[PRODUCT]lemma yoneda_sugar.prod.inv_hom (R : C)(A B : C) :
(yoneda_sugar.prod R A B).inv β« (yoneda_sugar.prod R A B).hom = π ( R [A]  β¨― R[B]) :=
(Yoneda_preserve_product R A B).inv_hom_id'
@[PRODUCT]lemma yoneda_sugar.prod.second (R : C)(A B : C) :
(yoneda_sugar.prod R A B).hom β« limits.prod.snd = (R < limits.prod.snd >) := rfl

@[PRODUCT]lemma yoneda_sugar.id (R : C)(A : C) : R < π A > = π ( R [A] ) := begin
funext,
exact comp_id C g,
-- have T : ((yoneda.map (π A)).app (op R)) g = (g β« (π A)),
end
lemma yoneda_sugar_prod (R : C)(A B : C)(X :C)(f : X βΆ A)(g : X βΆ B) :
R < (f | g) > β« (yoneda_sugar.prod R A B).hom  =  (R < f > | R < g > ) :=  -- the  β«  is  :/
begin
PRODUCT_CAT,
-- rw  yoneda_sugar.prod.hom R A B,
-- rw prod.left_composition,
iterate 2 {rw β yoneda_sugar.composition},   -- rw β is the problem ?
rw lem.prod.lift_fst,
rw lem.prod.lift_snd,
end
@[PRODUCT]lemma yoneda_sugar_prod_inv (R : C)(A B : C)(X :C)(f : X βΆ A)(g : X βΆ B) :
R < (f | g) >   =  (R < f > | R < g > ) β« (yoneda_sugar.prod R A B).inv :=
begin
PRODUCT_CAT,  -- noting   HERE PROBLEM the tatic do nothing
rw β yoneda_sugar_prod,
rw assoc,
rw yoneda_sugar.prod.hom_inv,
exact rfl,
end
@[PRODUCT]lemma  yoneda_sugar.otimes (R : C){Y Z K :C}(f : X βΆ Y )(g : Z βΆ K) :
( R < (f β g) > ) = (yoneda_sugar.prod  _ _ _).hom β« ((R<f>) β R<g>) β« (yoneda_sugar.prod _ _ _ ).inv := begin
PRODUCT_CAT,
-- iterate 2 {rw prod.otimes_is_prod},
-- rw  yoneda_sugar.prod.hom,
-- iterate 1 {rw yoneda_sugar_prod_inv},
rw β assoc,
rw prod.left_composition,
rw β assoc,
rw prod.lift_fst,
rw β assoc,
rw prod.lift_snd,
-- rw yoneda_sugar.composition,
-- rw yoneda_sugar.composition,
end
@[PRODUCT]lemma yonega_sugar.one_otimes (R :C)(X Y Z: C) (f : X βΆ Y) :
(((yoneda_sugar.prod R Z X).inv) β« (R <(π Z β f ) > ) β« (yoneda_sugar.prod R Z Y).hom) = (π (R[Z]) β R < f >) := begin
rw yoneda_sugar.otimes,
iterate 3 {rw β assoc},
rw yoneda_sugar.prod.inv_hom,
rw id_comp,
rw assoc,
rw yoneda_sugar.prod.inv_hom,
rw β yoneda_sugar.id,
simp,
end
lemma yonega_sugar.one_otimes' (R :C)(X Y Z: C) (f : X βΆ Y) :
( (R <(π Z β f ) > ) β« (yoneda_sugar.prod R Z Y).hom) = ((yoneda_sugar.prod R Z X).hom) β« (π (R[Z]) β R < f >) := begin
iterate 2{ rw yoneda_sugar.prod.hom},
rw prod.left_composition,
iterate 2{ rw β yoneda_sugar.composition},
rw prod.map_first,
rw prod.map_second,
rw comp_id,
rw prod.otimes_is_prod,rw prod.left_composition,rw β assoc,
rw prod.lift_fst,rw β  assoc,rw prod.lift_snd,rw comp_id,
rw yoneda_sugar.composition,
end


#### Kevin Buzzard (Apr 13 2020 at 12:42):

I think you're right about \l assoc. If you run your tactic then the goal turns into precisely the step where you want to rewrite associativity backwards. I think @Scott Morrison will have some ideas. The problem is that you cannot just tell simp to try rw assoc and rw \l assoc because then it will loop. Maybe this is something to do with his rewrite_search tactic? I think that this is not quite finished, but I don't know if he has already written enough stuff to make it possible to do what you want to do.

#### orlando (Apr 13 2020 at 12:46):

I understand @Kevin Buzzard : if we tell  rw assoc  and rw \l assoc  i saw the problem !!! lean don't unterstand i what direction to go !

#### orlando (Apr 13 2020 at 12:47):

tidy work for some lemma !

#### orlando (Apr 13 2020 at 12:48):

In fact the tatic i need is something like : ' rewrite up to assoc ' !

#### Kevin Buzzard (Apr 13 2020 at 12:50):

This is why I tagged Scott -- he will know the state of the art.

#### Markus Himmel (Apr 13 2020 at 13:05):

Maybe the reassoc attribute is already enough. See here. There is also a reassoc_of tactic for use together with rw but I don't know how well it works. I don't think it is actually used anywhere in mathlib.

#### Kevin Buzzard (Apr 13 2020 at 13:11):

@orlando here is how simp proves (a+b)+(c+d)=d+((c+b)+a): first it applies associativity as many times as possible, to get a+(b+(c+d))=d+(c+(b+a)), and then it wants to swap around variables. Clearly you can swap c and d in a+(b+(c+d)) using add_comm. But how to swap a and b? The trick is a lemma called add_left_comm which says a+(b+c)=b+(a+c). You can prove a+(b+(c+d))=d+(c+(b+a)) using just add_left_comm and add_comm, because these will let you swap any two adjacent variables, so you can run some kind of sorting function.

#### Kevin Buzzard (Apr 13 2020 at 13:12):

reassoc is the same kind of trick. It gives you a lemma which you can apply without having to use \l assoc.

#### Kevin Buzzard (Apr 13 2020 at 13:14):

Maybe you should look through the category theory library and see what kind of lemmas Scott and others are tagging with reassoc.

#### Kenny Lau (Apr 13 2020 at 13:14):

set_option trace.simplify.rewrite true
example (a b c d : β€) : (a+b)+(c+d)=d+((c+b)+a) :=
/-
0. [simplify.rewrite] [add_left_comm]: a + b + (c + d) ==> c + (a + b + d)
0. [simplify.rewrite] [add_comm]: a + b + d ==> d + (a + b)
0. [simplify.rewrite] [add_left_comm]: d + (a + b) ==> a + (d + b)
0. [simplify.rewrite] [add_comm]: d + b ==> b + d
0. [simplify.rewrite] [add_left_comm]: c + (a + (b + d)) ==> a + (c + (b + d))
0. [simplify.rewrite] [add_left_comm]: c + (b + d) ==> b + (c + d)
0. [simplify.rewrite] [add_comm]: c + b ==> b + c
0. [simplify.rewrite] [add_comm]: b + c + a ==> a + (b + c)
0. [simplify.rewrite] [add_left_comm]: d + (a + (b + c)) ==> a + (d + (b + c))
0. [simplify.rewrite] [add_left_comm]: d + (b + c) ==> b + (d + c)
0. [simplify.rewrite] [add_comm]: d + c ==> c + d
0. [simplify.rewrite] [eq_self_iff_true]: a + (b + (c + d)) = a + (b + (c + d)) ==> true
-/


#### Kenny Lau (Apr 13 2020 at 13:16):

set_option trace.simplify.rewrite true
example (a b c d : β€) : (a+b)+(c+d)=d+((c+b)+a) :=
/-
0. [simplify.rewrite] [add_assoc]: a + b + (c + d) ==> a + (b + (c + d))
0. [simplify.rewrite] [add_comm]: c + b ==> b + c
0. [simplify.rewrite] [add_assoc]: b + c + a ==> b + (c + a)
0. [simplify.rewrite] [add_comm]: c + a ==> a + c
0. [simplify.rewrite] [add_left_comm]: b + (a + c) ==> a + (b + c)
0. [simplify.rewrite] [add_left_comm]: d + (a + (b + c)) ==> a + (d + (b + c))
0. [simplify.rewrite] [add_left_comm]: d + (b + c) ==> b + (d + c)
0. [simplify.rewrite] [add_comm]: d + c ==> c + d
0. [simplify.rewrite] [eq_self_iff_true]: a + (b + (c + d)) = a + (b + (c + d)) ==> true
-/


#### Kevin Buzzard (Apr 13 2020 at 13:19):

In fact orlando, we see from my PR that Scott tagged prod.lift_fst with reassoc and it this creates precisely the corresponding lemma which would finish your proof without the \l assoc.

#### orlando (Apr 13 2020 at 13:20):

Ohhhh  set_option trace.simplify.rewrite true  is very Gooooood !

#### Kevin Buzzard (Apr 13 2020 at 13:22):

Hey, I got it working :-)

#### Kevin Buzzard (Apr 13 2020 at 13:22):

@[PRODUCT, reassoc] lemma prod.lift_fst {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : prod.lift f g β« category_theory.limits.prod.fst = f :=
limit.lift_Ο (binary_fan.mk f g) _

attribute [PRODUCT] prod.lift_fst_assoc


#### Kevin Buzzard (Apr 13 2020 at 13:22):

reassoc creates a new lemma prod.lift_fst_assoc and then I also tag it with PRODUCT

#### Kevin Buzzard (Apr 13 2020 at 13:23):

@[PRODUCT]lemma destruction {X Y Z : C} (f :  Y βΆ X) (g : X βΆ Z ) :
(f | π Y) β« (g β (π Y)) = (f β« g | π Y) := begin
apply prod.hom_ext,
PRODUCT_CAT,


closes the first goal!

#### Kevin Buzzard (Apr 13 2020 at 13:24):

@[PRODUCT]lemma destruction {X Y Z : C} (f :  Y βΆ X) (g : X βΆ Z ) :
(f | π Y) β« (g β (π Y)) = (f β« g | π Y) := begin
apply prod.hom_ext;PRODUCT_CAT
end


#### Kevin Buzzard (Apr 13 2020 at 13:24):

; means "apply the next tactic to all of the goals"

#### Patrick Massot (Apr 13 2020 at 13:37):

orlando said:

Ohhhh  set_option trace.simplify.rewrite true  is very Gooooood !

#### Bhavik Mehta (Apr 13 2020 at 15:02):

You might also like to use Scott's slice_lhs or slice_rhs tactics

#### orlando (Apr 13 2020 at 16:19):

hum a question : what is this error ?

excessive memory consumption detected at 'parse_notation' (potential solution: increase memory consumption threshold)


#### Kevin Buzzard (Apr 13 2020 at 16:20):

It means you made a typo but instead of telling you the true problem, Lean just got confused.

#### orlando (Apr 13 2020 at 16:20):

I have just import the previous file in a other file.

hmm

#### Kevin Buzzard (Apr 13 2020 at 16:26):

Make a little project and push it to github?

#### orlando (Apr 13 2020 at 16:32):

i don't know how use github :confused:

#### orlando (Apr 13 2020 at 16:33):

but i thinck it's because i save my previous file in the directory of mathlib, sorry, my question is not well asked

#### orlando (Apr 13 2020 at 17:08):

Hum i try with here it's ok ?

#### orlando (Apr 13 2020 at 17:10):

in the file  G  i import the file  groupk  and the error is excessive memory ... perhaps something stupid :sweat_smile:

#### Kevin Buzzard (Apr 13 2020 at 17:12):

The problem is not the import. Put #exit just before namespace GROUP_OBJ and everything is OK.

#### Kevin Buzzard (Apr 13 2020 at 17:13):

The problem is the group_obj structure

#### Kevin Buzzard (Apr 13 2020 at 17:20):

My guess is that the issue is maybe with the notation [ ... ] which you define in groupk. Lean doesn't seem to like the definition of group_obj. The notation [...] is already used to mean something else. I think Lean thinks [π : category.{v} C] is R and has_binary_products.{v} C is A.

#### orlando (Apr 13 2020 at 17:24):

Not a good idea this notation :skull_and_crossbones:

#### Kevin Buzzard (Apr 13 2020 at 17:38):

Well, they use [R] in the definition of module homomorphism: see here

#### Kevin Buzzard (Apr 13 2020 at 17:38):

But somehow they are more careful. I don't know anything about parsing.

#### Kevin Buzzard (Apr 13 2020 at 17:39):

Maybe the point is that they have something before the [

#### orlando (Apr 13 2020 at 17:42):

Okay Kevin, so it's very dangerous to play with notation !

thx !

#### Johan Commelin (Apr 13 2020 at 17:43):

In Lean 4 notation will be several orders of magnitude more powerful

#### orlando (Apr 13 2020 at 18:46):

this is really beautiful ! quasi automatic proof : i'm really impress ! i

lemma prod.map_eq {X Y Z W : C}(f1 f2  : X βΆ Y)(g1 g2  : Z βΆ W) :
((Ο1 : X β¨― Z βΆ X) β« f1 = (Ο1 : X β¨― Z βΆ X)  β« f2) β
((Ο2 : X β¨― Z βΆ Z) β« g1 = (Ο2 : X β¨― Z βΆ Z)  β« g2) β ((f1 β g1) = (f2 β g2)) := Ξ» certif1 certif2, begin
PRODUCT_CAT,
rw certif1, rw certif2,
end


#### orlando (Apr 13 2020 at 18:47):

i love this Game :yum:

#### orlando (Apr 13 2020 at 18:54):

Bhavik Mehta said:

You might also like to use Scott's slice_lhs or slice_rhs tactics

Do you have an exemple of what the tatic do ?

#### Scott Morrison (Apr 14 2020 at 05:47):

https://leanprover-community.github.io/mathlib_docs/tactic/slice.html#tactic.interactive.slice_lhs

#### Scott Morrison (Apr 14 2020 at 05:47):

(They've been observed to have some bugs: please report them if you find some!)

#### Scott Morrison (Apr 14 2020 at 05:48):

Essentially, slice_lhs 2 4 { ... } will reassociate as necessary, and show you just the 2nd, 3rd, and 4th morphisms in a long composite. You can then rewrite or simplifying just those, and when you exit the { ... } it will put everything back together again.

#### Scott Morrison (Apr 14 2020 at 05:49):

This, in combination with the @[reassoc] tags on all your simp lemmas, takes away a fair chunk of the pain of working with associativity in categories.

#### Bryan Gin-ge Chen (Apr 14 2020 at 05:54):

I didn't know those existed β we should add them to the main tactic docs and tactic.default.

#### Scott Morrison (Apr 14 2020 at 06:14):

Ideally they would work with any associative structure, not just a category! :-) But they don't.

#### orlando (Apr 15 2020 at 08:04):

Hello @Scott Morrison :
I see the lemma like  prod.lift_fst  are in the library, thx :+1:

A question : is it normal that you force to mention the category for the product ?

example  {Y A B : C} (f : Y βΆ A) (g : Y βΆ B) : ( f | g) β« Ο1 = f  :=  prod.lift_fst C f g


I can't just write  prod.lift_fst f g ` : if i understand $f$ know $A$ and $A$ know $C$ so it's ok for implicit parameter ?

#### Markus Himmel (Apr 15 2020 at 08:11):

I have already fixed this and it will probably land in mathlib soon.