# Zulip Chat Archive

## Stream: general

### Topic: create an element of product

#### orlando (Apr 16 2020 at 00:07):

Hello, i have i little problem :slight_smile:

import category_theory.limits.limits import category_theory.limits.shapes import category_theory.yoneda import category_theory.opposites import category_theory.types ----- i import all, i don't understand :D import category_theory.limits.types open category_theory open category_theory.limits open category_theory.category open opposite universe u lemma test (U V W Z: Type u) (u0 : U) (v0 : V) (f : W ⟶ U)(g : W ⟶ V) (φ : U ⨯ V ⟶ Z) : true --- not too difficult goal :D := begin let eu := hom_of_element u0, let ev := hom_of_element v0, let c := binary_fan.mk eu ev, --- i thinck it's ok ? let θ := limit.lift (pair U V) c, have R : θ ≫ φ = hom_of_element (φ ( (u0,v0) : U ⨯ V )) --- PROBLEM cross vs time trivial, --- how to create (u0,v0) ∈ U ⨯ V ? end

#### Reid Barton (Apr 16 2020 at 00:12):

The only thing you know about `U ⨯ V`

is that it is some product of `U`

and `V`

in the category of types, so the only reasonable way to construct "`(u, v)`

" is what you already have on the left-hand side of the equation `R`

(though there should be a more convenient way to build this already).

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

I'm ok Reid, but for an abstract category. For set we have a canonical choise for the product ` U \times V `

with the projection.

#### orlando (Apr 16 2020 at 00:22):

i mean it's a theorem such that set as product not an assumption ! So there is a construction.

#### Reid Barton (Apr 16 2020 at 00:23):

But there isn't a theorem that says the thing denoted by `U ⨯ V`

is actually *equal to* the product type, and in fact it isn't.

#### Reid Barton (Apr 16 2020 at 00:23):

You can define an isomorphism, and that's essentially what you're in the process of doing

#### Reid Barton (Apr 16 2020 at 00:25):

`U ⨯ V`

is actually defined as the limit over this `walking_pair`

index category that's related to `binary_fan`

. Otherwise I guess the `limit.lift ... (binary_fan.mk ...)`

stuff wouldn't work.

#### Reid Barton (Apr 16 2020 at 00:25):

It might not be the correct design, but it is the current one.

#### Kevin Buzzard (Apr 16 2020 at 00:27):

For set there is a canonical choice -- but Lean makes another choice ;-)

#### orlando (Apr 16 2020 at 00:29):

:confused:

#### Reid Barton (Apr 16 2020 at 00:29):

Well, it's the library's choice, not Lean's.

#### Reid Barton (Apr 16 2020 at 00:30):

You don't get to believe all the following simultaneously.

- A limit in Set is produced by [such and such general construction].
- A product in Set is produced by the product type.
- Products are limits over the category
`walking_pair`

.

#### Reid Barton (Apr 16 2020 at 00:31):

You might say you don't really care what the general construction of limits is, which is true, but whatever it is, there's no way it will reduce to the product of types when the index category is `walking_pair`

.

#### Reid Barton (Apr 16 2020 at 00:34):

It's possible it might be better to abandon the third item on that list instead, or maybe there's some other design we haven't come up with which would be superior.

#### Kevin Buzzard (Apr 16 2020 at 00:37):

You can't fix the problem that there is more than one construction of a limit; even if you magically got products to be the product type, then you can't get triple products to be A x (B x C) and (A x B) x C. There will have to be some sort of infrastructure which moves between isomorphic objects that satisfy the universal property and perhaps binary products is a great place to test it out.

#### orlando (Apr 16 2020 at 00:37):

it's difficult to understand, i have to think a little about this ! Thx

#### Kevin Buzzard (Apr 16 2020 at 00:38):

Orlando, surely your job is to prove that the product A x B satisfies the universal property and then to use that to construct the fixed isomorphism between A x B and whatever mathlib's product is.

#### Kevin Buzzard (Apr 16 2020 at 00:39):

And theorems should never be formalised about the product, but only about an object which satisfies the universal property which the product satisfies, I guess.

#### Reid Barton (Apr 16 2020 at 00:40):

If you prove it satisfies the universal property then there should be a way in the library to extract the isomorphism from that (though maybe it's easier to build it directly by hand)

#### orlando (Apr 16 2020 at 00:41):

Ok i understand :+1:

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

This was the mistake we originally made in the schemes project: we proved theorems about R[1/f], but we should have proved theorems about all R-algebras which satisfied the universal property of R[1/f]

#### orlando (Apr 16 2020 at 01:07):

I'm ok ! i thick i do that. For example, if i take the ring $\mathbb{Z}[X,Y] / (x^2+3xy )$, i never proof fact about this ring but i start with Let $R$ be a ring and $a, b \in R$ s.t $a^2+3ab = 0$ and i show stuff (doing calculus :grinning_face_with_smiling_eyes: ) and at the end i can tell ok i choice $\mathbb{Z}[X,Y] / (x^2+3xy)$ with $x,y$ as $a,b$ so my calculus show some stuff about this last ring.

I understand .... tomorow for the product :D

#### Markus Himmel (Apr 16 2020 at 06:08):

Reid Barton said:

If you prove it satisfies the universal property then there should be a way in the library to extract the isomorphism from that (though maybe it's easier to build it directly by hand)

Here is how to get the isomorphism:

import category_theory.limits.shapes.binary_products open category_theory open category_theory.limits universes v u variables {C : Type u} [𝒞 : category.{v} C] include 𝒞 variables [has_binary_products.{v} C] example {X Y P : C} (f : P ⟶ X) (g : P ⟶ Y) (h : is_limit (binary_fan.mk f g)) : P ≅ X ⨯ Y := functor.map_iso (cones.forget _) (is_limit.unique_up_to_iso h (limit.is_limit _))

#### Scott Morrison (Apr 16 2020 at 07:52):

That definitely needs a shortcut.

#### Markus Himmel (Apr 16 2020 at 08:00):

Oh, I just noticed that there already is a shortcut:

example {X Y P : C} (f : P ⟶ X) (g : P ⟶ Y) (h : is_limit (binary_fan.mk f g)) : P ≅ X ⨯ Y := h.cone_point_unique_up_to_iso (limit.is_limit _)

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

Tidy doesn 't work ! :sweat_smile:

import category_theory.limits.limits import category_theory.limits.shapes import category_theory.yoneda import category_theory.opposites import category_theory.types ----- i import all, i don't understand :D import category_theory.limits.types import category_theory.limits.shapes.finite_products import category_theory.limits.shapes.terminal import category_theory.discrete_category open category_theory open category_theory.limits open category_theory.category open opposite universe u def Cartesian_prod (U V : Type u) : binary_fan U V := begin let P := U × V, let π_1 := (prod.fst : P ⟶ U), let π_2 := (prod.snd : P ⟶ V), let Fan := binary_fan.mk (as_hom π_1) (as_hom π_2), exact Fan, end lemma Cartesian_prod_is_prod (U V : Type u) : is_limit (Cartesian_prod U V) := begin exact {lift := begin intros, exact λ x : s.X,((s.π).app walking_pair.left x,(s.π).app walking_pair.right x), -- is there is some helper ? it's i little complicated end}, end

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

Automation is hard.

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

I don't understand nothing :innocent:

The tatic state at HERE is

1 goal U V : Type u, s : cone (pair U V), j : discrete walking_pair, x : s.X ⊢ (Cartesian_prod U V).π.app j (s.π.app walking_pair.left x, s.π.app walking_pair.right x) = s.π.app j x

Can i split the goal with ` j = left and j = right `

or something like this ?

import category_theory.limits.limits import category_theory.limits.shapes import category_theory.yoneda import category_theory.opposites import category_theory.types ----- i import all, i don't understand :D import category_theory.limits.types import category_theory.limits.shapes.finite_products import category_theory.limits.shapes.terminal import category_theory.discrete_category open category_theory open category_theory.limits open category_theory.category open opposite universe u def Cartesian_prod (U V : Type u) : binary_fan U V := binary_fan.mk (as_hom (prod.fst : U × V ⟶ U)) (as_hom (prod.snd : U × V ⟶ V)) @[simp]lemma Cartesian_prod.left (U V : Type u) (u : U )(v : V) : ((Cartesian_prod U V).π).app walking_pair.left = prod.fst := rfl @[simp]lemma Cartesian_prod.right (U V : Type u) (u : U )(v : V) : ((Cartesian_prod U V).π).app walking_pair.right =prod.snd := rfl -- @[simp] lemma binary_fan.mk_π_app_left {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : -- (binary_fan.mk π₁ π₂).π.app walking_pair.left = π₁ := rfl -- binary_fan.mk c'est le constructor de binary_fan : it a cone ! #print is_limit lemma Cartesian_prod_is_prod (U V : Type u) : is_limit (Cartesian_prod U V) := begin exact {lift := begin intros, exact λ x, ((s.π).app walking_pair.left x, (s.π).app walking_pair.right x), end, fac' := begin intros, tidy, --- HERE sorry, end, uniq' := sorry, }, end

#### Markus Himmel (Apr 16 2020 at 11:39):

Try `cases j`

.

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

:grinning_face_with_smiling_eyes:

lemma Cartesian_prod_is_prod (U V : Type u) : is_limit (Cartesian_prod U V) := begin exact {lift := begin intros, exact λ x, ((s.π).app walking_pair.left x, (s.π).app walking_pair.right x), end, fac' := begin intros, cases j , exact rfl,exact rfl, end, uniq' := begin intros, funext, ext, specialize w (walking_pair.left),rw ← w, rw types_comp_apply, exact rfl, specialize w (walking_pair.right), rw ← w, rw types_comp_apply,exact rfl, end }, end

#### orlando (Apr 16 2020 at 21:22):

Hello, another funny stuff :joy:

oups the code not work sorry i update it's ok ! but :confused:

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 import category_theory.limits.shapes.finite_products import category_theory.discrete_category universes v v1 u u1 open category_theory open category_theory.limits open category_theory.limits.walking_pair open category_theory.category open opposite open category_theory.limits namespace TEST variables {C : Type u} variables [𝒞 : category.{v} C] include 𝒞 lemma rfl_of_rlf {X1 Y1 X2 Y2 : C}(h : X1 = X2) (h' : Y1 = Y2 ) : (X1 ⟶ Y1) → (X2 ⟶ Y2) := begin intro f,tidy,exact f, --- super tidy end lemma jouer1 (X1 X2 Y1 Y2 : C) (fX : X1 ⟶ X2)(fY : Y1 ⟶ Y2) : true := begin let F1 := pair X1 Y1, let F2 := pair X2 Y2, have hx : X1 = F1.obj left, exact rfl, have hx' : X2 = F2.obj left, exact rfl, have hy : Y1 = F1.obj right, exact rfl, have hy' : Y2 = F2.obj right, exact rfl, -- let ψ := map_pair fX fY, --- not work is it posssible to make this work ? wihout rfl_of_rfl ? let φ := map_pair (rfl_of_rlf hx hx' fX) (rfl_of_rlf hy hy' fY), trivial, end end TEST

#### orlando (Apr 16 2020 at 21:25):

An other question : is there is documentation that explain ` rfl `

?

#### Johan Commelin (Apr 16 2020 at 21:29):

That's almost the same thing as asking what *definitional equality* is. The best resource is probably Mario's thesis.

#### Kenny Lau (Apr 16 2020 at 22:02):

I put this under the "you will pick it up as you use it and ask a million questions about it" file

#### Kevin Buzzard (Apr 16 2020 at 22:06):

`rfl`

proves `X=Y`

if X and Y have the same definition

#### Kevin Buzzard (Apr 16 2020 at 22:07):

Like it would prove `n+0=n`

but it would not prove `0+n=n`

#### Kenny Lau (Apr 16 2020 at 22:07):

defeq isn't transitive though

#### Kenny Lau (Apr 16 2020 at 22:07):

but yeah ok for practical purposes

#### orlando (Apr 16 2020 at 22:10):

In my example : tidy do ` induction h', induction h `

!

Last updated: May 14 2021 at 03:27 UTC