Zulip Chat Archive

Stream: maths

Topic: category


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

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:53):

You've made the C argument of group_obj implicit, by putting it in curly braces.

view this post on Zulip Mario Carneiro (Apr 11 2020 at 11:53):

You declared all variables as implicit in group_obj, but lean can't infer C

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:53):

You want structure group_obj (C : Type u)[𝒞 : category.{v} C]

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:53):

also, since you've included 𝒞 above, you're going to end up with two copies of the category argument

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:54):

It will explain how and why we use include here.

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:55):

not just in a category equipped with the monoidal structure coming from binary products.

view this post on Zulip Scott Morrison (Apr 11 2020 at 11:55):

I don't promise, but it may actually be _easier_ there.

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

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

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

view this post on Zulip 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 C\mathcal{C} you shouldn't mention it explicitly in your definition.

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:01):

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

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:02):

Variables are great once you're off and running and proving a million lemmas.

view this post on Zulip Scott Morrison (Apr 11 2020 at 12:02):

But for defining new structures and new types, please put the hypotheses inline!

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

view this post on Zulip orlando (Apr 11 2020 at 12:04):

thx, Kevin Mario and Scott, i read Slowly ! (i use google traductor to understand :grinning: )

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

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

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

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

Try one of Scott's category theory tactics?

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

Tidy?

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

Obviously?

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

Maybe you have to define the map?

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

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

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

Your lemma is not a lemma, I think?

view this post on Zulip 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) :=
{! !}

view this post on Zulip orlando (Apr 11 2020 at 16:48):

@Kevin Buzzard i made a mistake ?

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

It is in Type, not in Prop

view this post on Zulip 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' := _ }

view this post on Zulip orlando (Apr 11 2020 at 16:58):

hum !!! i try :slight_smile:

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:01):

example (A B Y : C) : (yoneda.obj (A ⨯ B)).obj (op Y) = (Y ⟶ A ⨯ B) := rfl

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

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

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

view this post on Zulip 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' := _ }

view this post on Zulip orlando (Apr 11 2020 at 17:18):

hum ! not the same !

view this post on Zulip orlando (Apr 11 2020 at 17:19):

normaly it's an obvious thing this Yoneda preserve product :sweat_smile:

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:21):

in 2017 I thought it was obvious that 2∉Q\sqrt{2}\not\in\mathbb{Q} :laughing:

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:24):

I am looking forward to proving the snake lemma :laughing:

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:31):

Hom(Y,A)Hom(Y,A) has type Type*, right?

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:33):

Nice!

view this post on Zulip orlando (Apr 11 2020 at 17:34):

i no ! there is ia mistake

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:36):

In category_theory.types there is this: @[simp] lemma types_hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:36):

So I am a bit surprised that my rfl above is failing

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:37):

Oh it is a stupid issue with brackets :-/

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:41):

OK now I can do it with @ and filling in implicit arguments

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:42):

49 minutes so far :-)

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:43):

gaaargh by obviously doesn't work for the proofs :-/

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:49):

  hom_inv_id' := begin
    ext f,
    cases j,
    obviously,
  end,

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:49):

obviously just killed two goals at once!

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 17:56):

I think there might be some way of training tidy to solve the first proof.

view this post on Zulip Kenny Lau (Apr 11 2020 at 17:57):

Kevin Buzzard said:

obviously just killed two goals at once!

killing two goals with one tactic

view this post on Zulip orlando (Apr 11 2020 at 18:00):

it's toooooo complicated :scream:

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:22):

(yoneda.obj A).obj (op Y) is just Y \h A

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

view this post on Zulip Reid Barton (Apr 11 2020 at 19:26):

It looks like it must be otherwise I can't make sense out of this goal

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:26):

annoyingly, it does something really annoying.

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

view this post on Zulip Reid Barton (Apr 11 2020 at 19:27):

oh

view this post on Zulip Reid Barton (Apr 11 2020 at 19:27):

how did you obtain x?

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

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

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

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

view this post on Zulip Reid Barton (Apr 11 2020 at 19:29):

because that's ultimately the only thing that the API gives you

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:29):

I thought that was obviously

view this post on Zulip Reid Barton (Apr 11 2020 at 19:29):

obviously is not the API

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:29):

Rotten luck.

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

view this post on Zulip Reid Barton (Apr 11 2020 at 19:31):

Hmm does the API for this not actually exist...?

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:32):

Right.

view this post on Zulip Reid Barton (Apr 11 2020 at 19:32):

Would that represent progress in your proof?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:33):

I'm hoping it's exactly what I need to finish the proof.

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:33):

It's presumably explicitly there for limits

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

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:34):

And if they're just isomorphic then I will never get anywhere without the universal property.

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

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

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

view this post on Zulip Reid Barton (Apr 11 2020 at 19:35):

Obviously the library should already provide this for you

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:36):

@orlando you found a hole :-)

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 19:37):

Good spot Reid :-)

view this post on Zulip Reid Barton (Apr 11 2020 at 19:41):

I even gave the correct proof :innocent:

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

view this post on Zulip Patrick Massot (Apr 11 2020 at 22:08):

PR!

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

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

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

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

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 10:31):

erw limit.lift_π would most likely have worked

view this post on Zulip Markus Himmel (Apr 12 2020 at 10:32):

But I agree that these lemmas would be a nice addition

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 10:35):

prod and prod.fst etc are all defined as abbreviations. It says that erewrite unfolds semireducible definitions. It also unfolds abbreviations?

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 10:35):

! even rw works!

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

view this post on Zulip Markus Himmel (Apr 12 2020 at 10:38):

You don't need the rw assoc either

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 10:41):

as long as you have about 5 minutes to spare! You're right!

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:49):

I think we should add all those lemmas!

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 10:50):

I'm making a PR. You want all three?

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

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:50):

Yes please!

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:50):

We should check the other special shapes, too.

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

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:50):

But if however far you get with the initial PR, we can look for those later.

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:51):

Well, at the moment it isn't, definitionally.

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 10:51):

Indeed, I half-suspect it's not true, or hard, or whatever

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:51):

Or rather, it only is up to an equiv at the moment.

view this post on Zulip Scott Morrison (Apr 12 2020 at 10:51):

But we can make it definitional.

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 11:13):

feat(category_theory/limits/shapes/binary_products):

"2 CHARACTERS OVER 50 IN CURRENT LINE"

:-/

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 11:18):

#2396

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

view this post on Zulip Bhavik Mehta (Apr 12 2020 at 15:10):

This isn't there, I think it should be! (and similar on the other side)

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

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

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

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

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

view this post on Zulip orlando (Apr 13 2020 at 12:47):

tidy work for some lemma !

view this post on Zulip orlando (Apr 13 2020 at 12:48):

In fact the tatic i need is something like : ' rewrite up to assoc ' !

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 12:50):

This is why I tagged Scott -- he will know the state of the art.

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

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

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

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

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

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

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

view this post on Zulip orlando (Apr 13 2020 at 13:20):

Ohhhh set_option trace.simplify.rewrite true is very Gooooood !

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

Hey, I got it working :-)

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

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

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

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

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 13:24):

; means "apply the next tactic to all of the goals"

view this post on Zulip orlando (Apr 13 2020 at 13:27):

ohhh that nice :tada:

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

view this post on Zulip Bhavik Mehta (Apr 13 2020 at 15:02):

You might also like to use Scott's slice_lhs or slice_rhs tactics

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

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

view this post on Zulip orlando (Apr 13 2020 at 16:20):

I have just import the previous file in a other file.

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 16:26):

hmm

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 16:26):

Make a little project and push it to github?

view this post on Zulip orlando (Apr 13 2020 at 16:32):

i don't know how use github :confused:

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

view this post on Zulip orlando (Apr 13 2020 at 17:08):

Hum i try with here it's ok ?

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

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

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 17:13):

The problem is the group_obj structure

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

view this post on Zulip orlando (Apr 13 2020 at 17:24):

Not a good idea this notation :skull_and_crossbones:

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 17:38):

Well, they use [R] in the definition of module homomorphism: see here

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 17:38):

But somehow they are more careful. I don't know anything about parsing.

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 17:39):

Maybe the point is that they have something before the [

view this post on Zulip orlando (Apr 13 2020 at 17:42):

Okay Kevin, so it's very dangerous to play with notation !

view this post on Zulip orlando (Apr 13 2020 at 17:43):

thx !

view this post on Zulip Johan Commelin (Apr 13 2020 at 17:43):

In Lean 4 notation will be several orders of magnitude more powerful

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

view this post on Zulip orlando (Apr 13 2020 at 18:47):

i love this Game :yum:

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

view this post on Zulip Scott Morrison (Apr 14 2020 at 05:47):

https://leanprover-community.github.io/mathlib_docs/tactic/slice.html#tactic.interactive.slice_lhs

view this post on Zulip Scott Morrison (Apr 14 2020 at 05:47):

(They've been observed to have some bugs: please report them if you find some!)

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

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

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

view this post on Zulip Scott Morrison (Apr 14 2020 at 06:14):

Ideally they would work with any associative structure, not just a category! :-) But they don't.

view this post on Zulip 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 ff know AA and AA know CC so it's ok for implicit parameter ?

view this post on Zulip Markus Himmel (Apr 15 2020 at 08:11):

I have already fixed this and it will probably land in mathlib soon.

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

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

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