product of categories

Stream: lean4

[Kind Bubble]

Hi all!

I've moved my question over here to the lean4 stream to see if it could get an answer. Right now CatPrdId1B is giving me trouble and I can't figure out why.

import Init.Data.ToString.Basic
universe u
universe v

-- Construction of the category of categories

structure Cat where
  Obj : Type u
  Hom : ∀(_:Obj),∀(_:Obj), Type v
  Idn : ∀(X:Obj),Hom X X
  Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
  Id2 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X X Y) (Idn X) f = f
  Ass : ∀(W:Obj),∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(f:Hom W X),∀(g:Hom X Y),∀(h:Hom Y Z),(Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h
def Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

def Hom {C : Cat} (X : C.Obj) (Y : C.Obj) := C.Hom X Y
def Idn {C : Cat} (X : C.Obj) := C.Idn X

structure Fun (C : Cat) (D : Cat) where
   Obj : ∀(_ : C.Obj),D.Obj
   Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Mor X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),D.Cmp (Obj X) (Obj Y) (Obj Z) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g))

def CatIdn (C : Cat) : Fun C C :=
{Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>Eq.refl (C.Cmp X Y Z f g)}

def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):=
{Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>((Eq.trans) (G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))}

def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) := Eq.refl (CatCmp B C E F (CatCmp C D E G H))

def Cats : Cat := {Obj := Cat,Hom := Fun,Idn := CatIdn,Cmp := CatCmp,Id1 := CatId1,Id2 := CatId2,Ass := CatAss}

-- Construction of the product of categories

def CatPrdObj (C : Cat) (D : Cat) := C.Obj × D.Obj

def CatPrdHom (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) := (Hom X.1 Y.1) × (Hom X.2 Y.2)

def CatPrdIdn (C : Cat) (D : Cat) (P : CatPrdObj C D) := (C.Idn P.1, D.Idn P.2)

def CatPrdCmp (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (Z : CatPrdObj C D) (f : CatPrdHom C D X Y) (g : CatPrdHom C D Y Z) := (C.Cmp X.1 Y.1 Z.1 f.1 g.1, D.Cmp X.2 Y.2 Z.2 f.2 g.2)
theorem CatPrdId1A (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (CatPrdCmp C D X Y Y f (CatPrdIdn C D Y) = (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))) := Eq.refl (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))

theorem CatPrdId1B (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2)) = (f.1, f.2) := (C.Id1 X.1 Y.1 f.1) ▸ (D.Id1 X.2 Y.2 f.2)
--def CatPrd (C : Cat) (D : Cat) : Cat2 := {Obj := CatPrdObj C D, Hom := CatPrdHom C D, Idn := CatPrdIdn C D, Cmp := CatPrdCmp C D, Id1 := CatPrdId1A C D}

I figured out that this ▸ isn't doing what I want. I just need a simple F which takes in p : a = b and q : c = d and gives F p q : (a, c) = (b, d). But congr and ▸ aren't working for me.

[Kind Bubble]

Kind Bubble said:

Hi all!

I've moved my question over here to the lean4 stream to see if it could get an answer. Right now CatPrdId1B is giving me trouble and I can't figure out why.

import Init.Data.ToString.Basic
universe u
universe v

-- Construction of the category of categories

structure Cat where
  Obj : Type u
  Hom : ∀(_:Obj),∀(_:Obj), Type v
  Idn : ∀(X:Obj),Hom X X
  Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
  Id2 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X X Y) (Idn X) f = f
  Ass : ∀(W:Obj),∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(f:Hom W X),∀(g:Hom X Y),∀(h:Hom Y Z),(Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h
def Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

def Hom {C : Cat} (X : C.Obj) (Y : C.Obj) := C.Hom X Y
def Idn {C : Cat} (X : C.Obj) := C.Idn X

structure Fun (C : Cat) (D : Cat) where
   Obj : ∀(_ : C.Obj),D.Obj
   Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Mor X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),D.Cmp (Obj X) (Obj Y) (Obj Z) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g))

def CatIdn (C : Cat) : Fun C C :=
{Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>Eq.refl (C.Cmp X Y Z f g)}

def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):=
{Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(Z : C.Obj)=>fun(f : C.Hom X Y)=>fun(g : C.Hom Y Z)=>((Eq.trans) (G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))}

def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) := Eq.refl (CatCmp B C E F (CatCmp C D E G H))

def Cats : Cat := {Obj := Cat,Hom := Fun,Idn := CatIdn,Cmp := CatCmp,Id1 := CatId1,Id2 := CatId2,Ass := CatAss}

-- Construction of the product of categories

def CatPrdObj (C : Cat) (D : Cat) := C.Obj × D.Obj

def CatPrdHom (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) := (Hom X.1 Y.1) × (Hom X.2 Y.2)

def CatPrdIdn (C : Cat) (D : Cat) (P : CatPrdObj C D) := (C.Idn P.1, D.Idn P.2)

def CatPrdCmp (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (Z : CatPrdObj C D) (f : CatPrdHom C D X Y) (g : CatPrdHom C D Y Z) := (C.Cmp X.1 Y.1 Z.1 f.1 g.1, D.Cmp X.2 Y.2 Z.2 f.2 g.2)
theorem CatPrdId1A (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (CatPrdCmp C D X Y Y f (CatPrdIdn C D Y) = (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))) := Eq.refl (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2))

theorem CatPrdId1B (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) : (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2)) = (f.1, f.2) := (C.Id1 X.1 Y.1 f.1) ▸ (D.Id1 X.2 Y.2 f.2)
--def CatPrd (C : Cat) (D : Cat) : Cat2 := {Obj := CatPrdObj C D, Hom := CatPrdHom C D, Idn := CatPrdIdn C D, Cmp := CatPrdCmp C D, Id1 := CatPrdId1A C D}

I figured out that this ▸ isn't doing what I want. I just need a simple F which takes in p : a = b and q : c = d and gives F p q : (a, c) = (b, d). But congr and ▸ aren't working for me. Here's the reply that makes me think this:

Main.lean:91:215: error: type mismatch
  Cat.Id1 D X.snd Y.snd f.snd
has type
  Cat.Cmp D X.snd Y.snd Y.snd f.snd (Cat.Idn D Y.snd) = f.snd : Prop
but is expected to have type
  (Cat.Cmp C X.fst Y.fst Y.fst (Cat.Cmp C X.fst Y.fst Y.fst f.fst (Cat.Idn C Y.fst)) (Cat.Idn C Y.fst),
      Cat.Cmp D X.snd Y.snd Y.snd f.snd (Cat.Idn D Y.snd)) =
    (Cat.Cmp C X.fst Y.fst Y.fst f.fst (Cat.Idn C Y.fst), f.snd) : Prop

[Kind Bubble]

Aha! ok here's a much simpler problem:

def p : (1+0, 1+1) = (1, 2) := Eq.refl 1 ▸ Eq.refl 2

gives

Main.lean:89:51: error: failed to synthesize instance
  OfNat (Nat × Nat) 2
Main.lean:93:215: error: type mismatch
  Cat.Id1 D X.snd Y.snd f.snd
has type
  Cat.Cmp D X.snd Y.snd Y.snd f.snd (Cat.Idn D Y.snd) = f.snd : Prop
but is expected to have type
  (Cat.Cmp C X.fst Y.fst Y.fst (Cat.Cmp C X.fst Y.fst Y.fst f.fst (Cat.Idn C Y.fst)) (Cat.Idn C Y.fst),
      Cat.Cmp D X.snd Y.snd Y.snd f.snd (Cat.Idn D Y.snd)) =
    (Cat.Cmp C X.fst Y.fst Y.fst f.fst (Cat.Idn C Y.fst), f.snd) : Prop
f + 1 : Nat

[Kind Bubble]

can anyone solve my puzzle exactly?

Here it is:

universe u
universe v
def F {A : u} {B : u} {a1 : A} {a2 : A} {b1 : B} {b2 : B} (p : a1 = b1) (q : a2 = b2) : (a1, a2) = (b1, b2) := sorry

[Adam Topaz]

theorem CatPrdId1B (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) :
  (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2)) = (f.1, f.2) :=
  by rw [show (f.fst, f.snd) = _ by rw [← C.Id1 X.1 Y.1 f.1, ← D.Id1 X.2 Y.2 f.2]]

I must say, it took me a while to figure out what's going on only because your code is hard to read. Your lines are so long that they don't nearly fit in my editor (the longest one has 481 characters). Also a lot of code is missing spaces in the natural places.

[Adam Topaz]

If you insist of a proof with triangles:

theorem CatPrdId1B (C : Cat) (D : Cat) (X : CatPrdObj C D) (Y : CatPrdObj C D) (f : CatPrdHom C D X Y) :
  (C.Cmp X.1 Y.1 Y.1 f.1 (C.Idn Y.1), D.Cmp X.2 Y.2 Y.2 f.2 (D.Idn Y.2)) = (f.1, f.2) :=
  (C.Id1 X.1 Y.1 f.1).symm ▸ (D.Id1 X.2 Y.2 f.2).symm ▸ rfl

The issue with the original proof was that f.fst and f.snd appear on both sides of the equality, and both get rewritten. If you rewrite backward, you only end up rewriting on one side, so you can make progress.

[Kind Bubble]

Thanks so much for your help Adam!

Your feedback is much appreciated since I'm new here.

"Your lines are so long that they don't nearly fit in my editor (the longest one has 481 characters)."

What's a good limit, like 100 or less?

[Adam Topaz]

100 is the standard I think

[Kind Bubble]

ok thanks a ton!

[Adam Topaz]

no problem! I might also recommend that you take a look at how category was set up in mathlib.

[Kind Bubble]

Oh definitely. Possibly you know a link?

[Adam Topaz]

https://leanprover-community.github.io/mathlib_docs/ and navigate to the category_theory folder on the LHS

[Adam Topaz]

If you want the category of categories specifically, here it is docs#category_theory.Cat

[Kind Bubble]

Thanks Adam!

Before you go, could you explain a bit about this triangle? And more importantly, I actually don't care for this triangle and want to know how you would have done it otherwise.

Also, here's a more general situation that is going to arise a lot for me:

universe u
def F {A : u} {B : u} {a1 : A} {a2 : A} {b1 : B} {b2 : B} (p : a1 = b1) (q : a2 = b2) : (a1, a2) = (b1, b2) := sorry

What is the ideal way here?