category

Stream: maths

[orlando]

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 ?

[orlando]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Have you read https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/category_theory/intro.lean ?

[Scott Morrison]

It will explain how and why we use include here.

[Scott Morrison]

Also, a more general note --- really you want to define a group object in any monoidal category

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

(for one, you won't need to define the notation ⊗, because it will be there for you already!)

[Kevin Buzzard]

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 : ℕ → ℕ

[Scott Morrison]

(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 :-)

[Kevin Buzzard]

All your definitions after the include and before the omit will include (X : Type). So if you include $\mathcal{C}$ you shouldn't mention it explicitly in your definition.

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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 {}.

[orlando]

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

[orlando]

Scott: Ah, I didn't know the concept of a monoidal category! I just looked at the lean file! Thx !

[orlando]

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  !

[orlando]

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

[Kevin Buzzard]

Try one of Scott's category theory tactics?

[Kevin Buzzard]

Tidy?

[Kevin Buzzard]

Obviously?

[Kevin Buzzard]

Maybe you have to define the map?

[orlando]

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

[Kevin Buzzard]

I have no idea what these tactics do but maybe they are just for proofs. This is data.

[Kevin Buzzard]

Your lemma is not a lemma, I think?

[Kevin Buzzard]

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) :=
{! !}

[orlando]

@Kevin Buzzard i made a mistake ?

[Kevin Buzzard]

It is in Type, not in Prop

[Kevin Buzzard]

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' := _ }

[orlando]

hum !!! i try :slight_smile:

[Kevin Buzzard]

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

[Kevin Buzzard]

{ 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 :-)

[Kevin Buzzard]

{ hom := prod.lift
    (λ f, f ≫ category_theory.limits.prod.fst)
    (λ f, f ≫ category_theory.limits.prod.snd),

[Kevin Buzzard]

{ 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 }

[orlando]

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' := _ }

[orlando]

hum ! not the same !

[orlando]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

example (A B Y : C) :
  ((Y ⟶ A) ⨯ (Y ⟶ B) ⟶ (Y ⟶ A)) = ((Y ⟶ A) ⨯ (Y ⟶ B) → (Y ⟶ A)) := rfl -- fail :-(

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[orlando]

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

[Kevin Buzzard]

Nice!

[orlando]

i no ! there is ia mistake

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh it is a stupid issue with brackets :-/

[Kevin Buzzard]

example (A B Y : C) :
  ((Y ⟶ A) ⨯ (Y ⟶ B) ⟶ (Y ⟶ A)) = (((Y ⟶ A) ⨯ (Y ⟶ B)) → (Y ⟶ A)) := rfl -- succeeds

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

    (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)),

[Kevin Buzzard]

49 minutes so far :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

obviously just killed two goals at once!

[Kevin Buzzard]

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
}

[Kevin Buzzard]

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

[Kenny Lau]

Kevin Buzzard said:

obviously just killed two goals at once!

killing two goals with one tactic

[orlando]

it's toooooo complicated :scream:

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[orlando]

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)),

[Kevin Buzzard]

This is probably better, because the proof I can't do involves using the universal property of limit

[Kevin Buzzard]

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 ?

[Kevin Buzzard]

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

[Reid Barton]

Is the categorical product in Type v the ordinary product? What happens if you do cases x?

[Reid Barton]

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

[Kevin Buzzard]

annoyingly, it does something really annoying.

[Kevin Buzzard]

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

[Reid Barton]

oh

[Reid Barton]

how did you obtain x?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Reid Barton]

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

[Kevin Buzzard]

I thought that was obviously

[Reid Barton]

obviously is not the API

[Kevin Buzzard]

Rotten luck.

[Kevin Buzzard]

I tried to chase the definition of prod back but it was just defined as a limit.

[Reid Barton]

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

[Reid Barton]

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.

[Kevin Buzzard]

Right.

[Reid Barton]

Would that represent progress in your proof?

[Kevin Buzzard]

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

[Kevin Buzzard]

It's presumably explicitly there for limits

[Reid Barton]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[orlando]

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

[Reid Barton]

So I guess you want to apply limit.hom_ext and then use cases on the objects of walking_pair.

[Reid Barton]

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

[Reid Barton]

Obviously the library should already provide this for you

[Reid Barton]

https://github.com/b-mehta/topos/blob/master/src/binary_products.lean#L29
from the topos project

[Kevin Buzzard]

@orlando you found a hole :-)

[Kevin Buzzard]

Good spot Reid :-)

[Reid Barton]

I even gave the correct proof :innocent:

[Bhavik Mehta]

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

[Patrick Massot]

PR!

[orlando]

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

[Kevin Buzzard]

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) _

[Kevin Buzzard]

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:

[orlando]

@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 !

[Kevin Buzzard]

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.

[Markus Himmel]

erw limit.lift_π would most likely have worked

[Markus Himmel]

But I agree that these lemmas would be a nice addition

[Kevin Buzzard]

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

[Kevin Buzzard]

! even rw works!

[Markus Himmel]

In fact, in your code above, you can leave out the rw prod.lift_fst entirely and obviously will still handle it

[Markus Himmel]

You don't need the rw assoc either

[Kevin Buzzard]

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

[Scott Morrison]

I think we should add all those lemmas!

[Kevin Buzzard]

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

[Scott Morrison]

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.

[Scott Morrison]

Yes please!

[Scott Morrison]

We should check the other special shapes, too.

[Kevin Buzzard]

I never figured out how to convince Lean that X \crossproduct Y was X \times Y if X Y : Type.

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

But we can make it definitional.

[Scott Morrison]

(Note that in some ways this is dangerous --- it allows/encourages people to break through the API. :-)

[Kevin Buzzard]

I'm out of my depth here, but it did make me go on a wild goose chase with the question.

[Kevin Buzzard]

I assumed I'd need it; I hadn't realised I could prove what I wanted in a purely arrow-theoretic way

[Markus Himmel]

Scott Morrison said:

We should check the other special shapes, too.

The biproducts PR also does not have these lemmas

[Kevin Buzzard]

feat(category_theory/limits/shapes/binary_products):

"2 CHARACTERS OVER 50 IN CURRENT LINE"

:-/

[Kevin Buzzard]

#2396

[orlando]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

I can add this to the PR. The | notation is orlando's I think; it might be worth getting Scott's input on this.

[Bhavik Mehta]

I would find some sort of notation for prod.lift useful, no strong preference on what it is

[orlando]

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

[Kevin Buzzard]

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.

[orlando]

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 !

[orlando]

tidy work for some lemma !

[orlando]

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

[Kevin Buzzard]

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

[Markus Himmel]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

reassoc is the same kind of trick. It gives you a lemma which you can apply without having to use \l assoc.

[Kevin Buzzard]

Maybe you should look through the category theory library and see what kind of lemmas Scott and others are tagging with reassoc.

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

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.

[orlando]

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

[Kevin Buzzard]

Hey, I got it working :-)

[Kevin Buzzard]

@[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

[Kevin Buzzard]

reassoc creates a new lemma prod.lift_fst_assoc and then I also tag it with PRODUCT

[Kevin Buzzard]

@[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!

[Kevin Buzzard]

@[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

[Kevin Buzzard]

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

[orlando]

ohhh that nice :tada:

[Patrick Massot]

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

[Bhavik Mehta]

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

[orlando]

hum a question : what is this error ?

excessive memory consumption detected at 'parse_notation' (potential solution: increase memory consumption threshold)

[Kevin Buzzard]

It means you made a typo but instead of telling you the true problem, Lean just got confused.

[orlando]

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

[Kevin Buzzard]

hmm

[Kevin Buzzard]

Make a little project and push it to github?

[orlando]

i don't know how use github :confused:

[orlando]

but i thinck it's because i save my previous file in the directory of mathlib, sorry, my question is not well asked

[orlando]

Hum i try with here it's ok ?

[orlando]

in the file G i import the file groupk and the error is excessive memory ... perhaps something stupid :sweat_smile:

[Kevin Buzzard]

The problem is not the import. Put #exit just before namespace GROUP_OBJ and everything is OK.

[Kevin Buzzard]

The problem is the group_obj structure

[Kevin Buzzard]

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.

[orlando]

Not a good idea this notation :skull_and_crossbones:

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe the point is that they have something before the [

[orlando]

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

[orlando]

thx !

[Johan Commelin]

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

[orlando]

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

[orlando]

i love this Game :yum:

[orlando]

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 ?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Bryan Gin-ge Chen]

I didn't know those existed – we should add them to the main tactic docs and tactic.default.

[Scott Morrison]

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

[orlando]

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 $f$ know $A$ and $A$ know $C$ so it's ok for implicit parameter ?

[Markus Himmel]

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

[Kevin Buzzard]

Sorry orlando, that was probably my fault. I made the PR when we were talking about this the other day

[orlando]

Kevin it's cool because I'm starting to understand a little bit about how lean works :grinning_face_with_smiling_eyes:

[orlando]

Scott : The slice tatics is verrrrrrry cooooooool :+1: :+1: