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

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

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