# Zulip Chat Archive

## 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. reference : Douady : Algebre et thΓ©ories galoisiennes page 45 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 `T`C :20 := (terminal C) notation `T`X : 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 `include`

d π above, you're going to end up with two copies of the category argument

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

Have you read https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/category_theory/intro.lean ?

#### 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:01):

It's also really confusing for anyone reading your definition.

#### 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. reference : Douady : Algebre et thΓ©ories galoisiennes page 45 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 `T`C :20 := (terminal C) notation `T`X : 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?

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

Tidy?

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

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

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

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)))

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

oh

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

how did you obtain `x`

?

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

The goal was this:

β’ (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

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

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.

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

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

#### Patrick Massot (Apr 11 2020 at 22:08):

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

:tada:

#### 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 `abbreviation`

s. 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):

Yes please!

#### 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"

:-/

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

#### 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}] run_cmd add_interactive [`PRODUCT_CAT] 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 `T`C :20 := (terminal C) notation `T`X : 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) := by simp [add_comm, add_left_comm] /- 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) := by simp [add_comm, add_left_comm, add_assoc] /- 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"

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

ohhh that nice :tada:

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

orlando said:

Ohhhh

`set_option trace.simplify.rewrite true`

is very Gooooood !

This messages suggests you should read https://github.com/leanprover-community/mathlib/blob/master/docs/extras/simp.md If you still want to learn more about simp then you can read the relevant sections in https://lean-forward.github.io/mathlib-maintenance/paper.pdf

#### 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.

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

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 !

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

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.

#### Kevin Buzzard (Apr 15 2020 at 08:13):

Sorry orlando, that was probably my fault. I made the PR when we were talking about this the other day

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

Kevin it's cool because I'm starting to understand a little bit about how lean works :grinning_face_with_smiling_eyes:

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

Scott : The slice tatics is verrrrrrry cooooooool :+1: :+1:

Last updated: May 10 2021 at 07:15 UTC