Zulip Chat Archive

Stream: general

Topic: create an element of product


view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Apr 16 2020 at 00:25):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 00:27):

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

view this post on Zulip orlando (Apr 16 2020 at 00:29):

:confused:

view this post on Zulip Reid Barton (Apr 16 2020 at 00:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip orlando (Apr 16 2020 at 00:37):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip orlando (Apr 16 2020 at 00:41):

Ok i understand :+1:

view this post on Zulip 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]

view this post on Zulip orlando (Apr 16 2020 at 01:07):

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

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

view this post on Zulip 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 _))

view this post on Zulip Scott Morrison (Apr 16 2020 at 07:52):

That definitely needs a shortcut.

view this post on Zulip 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 _)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:11):

Automation is hard.

view this post on Zulip 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

view this post on Zulip Markus Himmel (Apr 16 2020 at 11:39):

Try cases j.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip orlando (Apr 16 2020 at 21:25):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 22:06):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 22:07):

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

view this post on Zulip Kenny Lau (Apr 16 2020 at 22:07):

defeq isn't transitive though

view this post on Zulip Kenny Lau (Apr 16 2020 at 22:07):

but yeah ok for practical purposes

view this post on Zulip 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