create an element of product

Stream: general

[orlando]

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]

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]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Kevin Buzzard]

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

[orlando]

:confused:

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

Ok i understand :+1:

[Kevin Buzzard]

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]

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]

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]

That definitely needs a shortcut.

[Markus Himmel]

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]

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]

Automation is hard.

[orlando]

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]

Try cases j.

[orlando]

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

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]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kevin Buzzard]

rfl proves X=Y if X and Y have the same definition

[Kevin Buzzard]

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

[Kenny Lau]

defeq isn't transitive though

[Kenny Lau]

but yeah ok for practical purposes

[orlando]

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