How to establish mathematical equality in lean4

Stream: lean4

[Tammo Brinner]

Hey!
So i am working on a code about monads in lean4. For that (also to learn more about lean4) i decided to build the foundations of category theory myself. It all worked fine until i encountered the following problem: Suppose you have two Functors

$$F: C \rightarrow E, G: D\rightarrow E$$

and morphisms f and g in C and D respectively such that F(f)=G(g) mathematically. Then they do not have the type in Lean4. I would like to find a way to prove that they are in fact equal. How would one do that? Here are my Definitions of a Category and a Functor:

namespace mymon

/-- I should point out, that this is not the most general one can be. We could for example use Sort v and Sort u. That would allow our morphisms and objects to be Propositions etc as well. --/
structure Category (u v : Level) where
  Obj : Type u
  Hom : Obj → Obj → Type v
  id  : ∀ X, Hom X X
  /-- Given \(f : X \to Y\) and \(g : Y \to Z\), define \(g \circ f\) as `comp g f`. -/
  comp : ∀ {X Y Z}, Hom Y Z → Hom X Y → Hom X Z
  comp_assoc : ∀ {W X Y Z} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp h (comp g f) = comp (comp h g) f
  comp_id  : ∀ {X Y} (f : Hom X Y), comp f (id X) = f
  id_comp : ∀ {X Y} (f : Hom X Y), comp (id Y) f = f

/-- A functor between categories. -/
structure Functor {u₁ v₁ u₂ v₂ : Level} (C : Category u₁ v₁) (D : Category u₂ v₂) where
  obj : C.Obj → D.Obj
  map : ∀ {X Y : C.Obj}, C.Hom X Y → D.Hom (obj X) (obj Y)
  map_id  : ∀ (X : C.Obj), map (C.id X) = D.id (obj X)
  map_comp : ∀ {X Y Z : C.Obj} (g : C.Hom Y Z) (f : C.Hom X Y),
              map (C.comp g f) = D.comp (map g) (map f)

[Aaron Liu]

If you really need equality then you can use docs#HEq, but it is less well behaved than Eq.

[Kevin Buzzard]

"F(f)=G(g)" is an evil statement in general because it ultimately relies on equality of objects. Are you sure you don't want to instead state that a square commutes with the other two arrows being your chosen isomorphisms F(dom f) -> G(dom g) and F(cod f) -> G(cod g)? Category theory doesn't really have a concept of =, there is no mention of it in the axioms

[Edward van de Meent]

pretty sure there is equality of arrows in "composition is associative"

[Kevin Buzzard]

Aah indeed there is, but that's equality of morphisms in one fixed hom type so that's ok

[Kevin Buzzard]

Here we have two syntactically different hom types. It's equality of objects which is never mentioned (and for good reason, this concept is not preserved by equivalence of categories)

[Edward van de Meent]

btw, if your category is defined in a weird way, you might even have HEq f g for all arrows fand g, regardless of domain and codomain :upside_down:

[Edward van de Meent]

so it definitely is not the solution you should be looking for

[Tammo Brinner]

Kevin Buzzard schrieb:

Here we have two syntactically different hom types. It's equality of objects which is never mentioned (and for good reason, this concept is not preserved by equivalence of categories)

I see where you are getting at, but that is not what i mean right? In E these morphisms are actually equal and the Hom Types are also equal. Its just that lean does not regard them as equal because they have different types (in Lean). Mathematically, equality is actually what you see here.

[Eric Wieser]

Can you give a #mwe of the example that you tried which doesn't typecheck?

[Tammo Brinner]

Eric Wieser schrieb:

Can you give a #mwe of the example that you tried which doesn't typecheck?

Sure, that is not a problem, but it requires quite a bit of code.
I hope thats okay. If not I can think of a simpler example.

/-- I should point out, that this is not the most general one can be. We could for example use Sort v and Sort u. That would allow our morphisms and objects to be Propositions etc as well. --/

structure Category (u v : Level) where

  Obj : Type u

  Hom : Obj → Obj → Type v

  id  : ∀ X, Hom X X

  /-- Given \(f : X \to Y\) and \(g : Y \to Z\), define \(g \circ f\) as `comp g f`. -/

  comp : ∀ {X Y Z}, Hom Y Z → Hom X Y → Hom X Z

  comp_assoc : ∀ {W X Y Z} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),

    comp h (comp g f) = comp (comp h g) f

  comp_id  : ∀ {X Y} (f : Hom X Y), comp f (id X) = f

  id_comp : ∀ {X Y} (f : Hom X Y), comp (id Y) f = f

/-- A functor between categories. -/

structure Functor {u₁ v₁ u₂ v₂ : Level} (C : Category u₁ v₁) (D : Category u₂ v₂) where

  obj : C.Obj → D.Obj

  map : ∀ {X Y : C.Obj}, C.Hom X Y → D.Hom (obj X) (obj Y)

  map_id  : ∀ (X : C.Obj), map (C.id X) = D.id (obj X)

  map_comp : ∀ {X Y Z : C.Obj} (g : C.Hom Y Z) (f : C.Hom X Y),

              map (C.comp g f) = D.comp (map g) (map f)

/-- Composition of functors. -/

def Functor_comp {u₁ v₁ u₂ v₂ u₃ v₃ : Level}

  {C : Category u₁ v₁} {D : Category u₂ v₂} {E : Category u₃ v₃}

  (G : Functor D E) (F : Functor C D) : Functor C E :=

{

  obj := fun c ↦ G.obj (F.obj c)

  map := fun f ↦ G.map (F.map f)

  map_id := fun c ↦ by

    dsimp

    rw [F.map_id, G.map_id]

  map_comp := fun g f ↦ by

    dsimp

    rw [F.map_comp, G.map_comp]

}

/-- The identity functor. -/

def Id_Functor {u v : Level} (C : Category u v) : Functor C C :=

{

  obj := fun c ↦ c

  map := fun f ↦ f

  map_id := fun c ↦ by rfl

  map_comp := fun g f ↦ by rfl

}

/-- A natural transformation between functors. -/

structure NatTrafo {u₁ v₁ u₂ v₂ : Level}

  {C : Category u₁ v₁} {D : Category u₂ v₂}

  (F G : Functor C D) where

  obj : ∀ X : C.Obj, D.Hom (F.obj X) (G.obj X)

  is_nat : ∀ {X Y : C.Obj} (f : C.Hom X Y),

    D.comp (G.map f) (obj X) = D.comp (obj Y) (F.map f)

#check NatTrafo

/-- The identity natural transformation. -/

def Id_Trafo {u₁ v₁ u₂ v₂ : Level} {C : Category u₁ v₁} {D : Category u₂ v₂}

  (F : Functor C D) : NatTrafo F F :=

{

  obj := fun X ↦ D.id (F.obj X)

  is_nat := fun f ↦ by

    dsimp

    rw [D.comp_id, D.id_comp]

}

/-- Horizontal composition of natural transformations on the left. -/

def Trafo_comp_functor {u₁ v₁ u₂ v₂ u₃ v₃ : Level}

  {C : Category u₁ v₁} {D : Category u₂ v₂} {E : Category u₃ v₃}

  (H : Functor D E) {F G : Functor C D} (η : NatTrafo F G) :

  NatTrafo (Functor_comp H F) (Functor_comp H G) :=

  {

    obj := fun c ↦ H.map (η.obj c)

    is_nat := fun f ↦ by

      dsimp [Functor_comp]

      rw [←H.map_comp, ←H.map_comp, η.is_nat]

  }

/-- Horizontal composition of natural transformations on the right. -/

def Functor_comp_trafo {u₁ v₁ u₂ v₂ u₃ v₃ : Level}

  {C : Category u₁ v₁} {D : Category u₂ v₂} {E : Category u₃ v₃}

  {F G : Functor D E} (η : NatTrafo F G) (H : Functor C D) :

  NatTrafo (Functor_comp F H) (Functor_comp G H) :=

{

  obj := fun c ↦ η.obj (H.obj c)

  is_nat := fun f ↦ by

    dsimp [Functor_comp]

    rw [η.is_nat]

}

/-- Horizontal composition of natural transformations (both sides). -/

def horizontal_comp {u₁ v₁ u₂ v₂ u₃ v₃ : Level}

  {C : Category u₁ v₁} {D : Category u₂ v₂} {E : Category u₃ v₃}

  {J K : Functor D E} {F G : Functor C D}

  (ε : NatTrafo J K) (η : NatTrafo F G) :

  NatTrafo (Functor_comp J F) (Functor_comp K G) :=

{

  obj := fun c ↦ E.comp (ε.obj (G.obj c)) (J.map (η.obj c))

  is_nat := fun f ↦ by

    dsimp [Functor_comp]

    rw [E.comp_assoc, ε.is_nat, ←E.comp_assoc, ←J.map_comp, η.is_nat, J.map_comp, E.comp_assoc]

}

structure Monad {u v : Level} (C : Category u v) where

  m : Functor C C

  η : NatTrafo (Id_Functor C) m

  μ : NatTrafo (Functor_comp m m) m

  is_left_unit : sorry

  is_right_unit : sorry

  is_assoc  : sorry

variable {u v : Level} {C : Category u v} (M : Monad C) (X : C.Obj)

#check (horizontal_comp (Functor_comp_trafo M.η M.m) M.μ).obj X

#check (Id_Trafo M.m).obj X```
Right at the end, mathematically these are bot endomorphisms of m(X).
The left unit condition of a monad is that these are supposed to be equal
for all X, which is a sensible statement in mathematics.
But Lean complains there because the types of both sides are not equal.
I hope this made the problem more clear. I do think btw that there is an
elegant way of solving this. Some Extension Lemma which makes things
equal if they are equal in after really projecting to the category or something.
But thats above my paygrade i must admit...

[Eric Wieser]

Could you try to fix the double spacing there? "Ctrl + Shift + V" might prevent Zulip mangling it.

[Eric Wieser]

You also need a blank line after the ```

[Aaron Liu]

There is no such thing as Level. I would suggest putting set_option autoImplicit false at the top of you file in order to prevent having such errors. You can introduce new universes with the command universe u v.

[Tammo Brinner]

Eric Wieser schrieb:

Could you try to fix the double spacing there? "Ctrl + Shift + V" might prevent Zulip mangling it.

Sure I will do that later:)

[Tammo Brinner]

Aaron Liu schrieb:

There is no such thing as Level. I would suggest putting set_option autoImplicit false at the top of you file in order to prevent having such errors. You can introduce new universes with the command universe u v.

What do you mean? Of course there is such a thing. I mean the Type Level exists for sure.

[Aaron Liu]

-- unknown identifier 'Level'
#check Level

[Riccardo Brasca]

@Tammo Brinner when you write

structure Category (u v : Level) where

Lean does not know what Level is and it just just creates a new variable, called Level, to make sense of that line. This can be quite confusing (since later on you forget what Level really is). Putting set_option autoImplicit false you turn off this feature, and Lean will complain the first time you mention Level.

[Tammo Brinner]

Aaron Liu schrieb:

-- unknown identifier 'Level'
#check Level

Oh you are right...What did i even do then in the whole document and why does any of it work?

[Aaron Liu]

You wrote Level and Lean introduced it as a new free variable. It's the same machinery that makes

example (a : Fin n) (b : Fin m) : Fin (n + m) := sorry

work even though there is no mention of either n or m anywhere before they are used.

[Riccardo Brasca]

In practice it is as there was

variable {Level : Sort*}

before your first line.

[Aaron Liu]

Here's a solution to your original problem:

namespace mymon
set_option autoImplicit false

universe u v

/-- I should point out, that this is not the most general one can be. We could for example use Sort v and Sort u. That would allow our morphisms and objects to be Propositions etc as well. --/
structure Category where
  Obj : Type u
  Hom : Obj → Obj → Type v
  id : ∀ X, Hom X X
  /-- Given `f : X → Y` and `g : Y → Z`, define `g ∘ f` as `comp g f`. -/
  comp : ∀ {X Y Z}, Hom Y Z → Hom X Y → Hom X Z
  comp_assoc : ∀ {W X Y Z} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z),
    comp h (comp g f) = comp (comp h g) f
  comp_id  : ∀ {X Y} (f : Hom X Y), comp f (id X) = f
  id_comp : ∀ {X Y} (f : Hom X Y), comp (id Y) f = f

/-- A functor between categories. -/
structure Functor (C : Category) (D : Category) where
  obj : C.Obj → D.Obj
  map : ∀ {X Y : C.Obj}, C.Hom X Y → D.Hom (obj X) (obj Y)
  map_id  : ∀ (X : C.Obj), map (C.id X) = D.id (obj X)
  map_comp : ∀ {X Y Z : C.Obj} (g : C.Hom Y Z) (f : C.Hom X Y),
              map (C.comp g f) = D.comp (map g) (map f)

/-- Composition of functors. -/
def Functor.comp
    {C : Category} {D : Category} {E : Category}
    (G : Functor D E) (F : Functor C D) : Functor C E where
  obj := fun c ↦ G.obj (F.obj c)
  map := fun f ↦ G.map (F.map f)
  map_id := fun c ↦ by
    dsimp
    rw [F.map_id, G.map_id]
  map_comp := fun g f ↦ by
    dsimp
    rw [F.map_comp, G.map_comp]

/-- The identity functor. -/

def Functor.id (C : Category) : Functor C C where
  obj := fun c ↦ c
  map := fun f ↦ f
  map_id := fun c ↦ rfl
  map_comp := fun g f ↦ rfl


/-- A natural transformation between functors. -/

structure NatTrans
    {C : Category} {D : Category}
    (F G : Functor C D) where
  obj : ∀ X : C.Obj, D.Hom (F.obj X) (G.obj X)
  is_nat : ∀ {X Y : C.Obj} (f : C.Hom X Y),
    D.comp (G.map f) (obj X) = D.comp (obj Y) (F.map f)

#check NatTrans

/-- The identity natural transformation. -/

def NatTrans.id {C : Category} {D : Category}
    (F : Functor C D) : NatTrans F F where
  obj := fun X ↦ D.id (F.obj X)
  is_nat := fun f ↦ by
    dsimp
    rw [D.comp_id, D.id_comp]

/-- Horizontal composition of natural transformations on the left. -/
def NatTrans.hcompLeft
    {C : Category} {D : Category} {E : Category}
    (H : Functor D E) {F G : Functor C D} (η : NatTrans F G) :
    NatTrans (H.comp F) (H.comp G) where
  obj := fun c ↦ H.map (η.obj c)
  is_nat := fun f ↦ by
    dsimp [Functor.comp]
    rw [← H.map_comp, ← H.map_comp, η.is_nat]

/-- Horizontal composition of natural transformations on the right. -/
def NatTrans.hcompRight
    {C : Category} {D : Category} {E : Category}
    {F G : Functor D E} (η : NatTrans F G) (H : Functor C D) :
    NatTrans (F.comp H) (G.comp H) where
  obj := fun c ↦ η.obj (H.obj c)
  is_nat := fun f ↦ by
    dsimp [Functor.comp]
    rw [η.is_nat]

/-- Horizontal composition of natural transformations (both sides). -/
def NatTrans.hcomp
    {C : Category} {D : Category} {E : Category}
    {J K : Functor D E} {F G : Functor C D}
    (ε : NatTrans J K) (η : NatTrans F G) :
    NatTrans (J.comp F) (K.comp G) where
  obj := fun c ↦ E.comp (ε.obj (G.obj c)) (J.map (η.obj c))
  is_nat := fun f ↦ by
    dsimp [Functor.comp]
    rw [E.comp_assoc, ε.is_nat, ← E.comp_assoc, ← J.map_comp, η.is_nat, J.map_comp, E.comp_assoc]

/-- Vertical composition of natural transformations. -/
def NatTrans.vcomp
  {C : Category} {D : Category}
  {F G H : Functor C D}
  (ε : NatTrans G H) (η : NatTrans F G) :
  NatTrans F H where
  obj c := D.comp (ε.obj c) (η.obj c)
  is_nat f := by
    rw [D.comp_assoc, ε.is_nat, ← D.comp_assoc, η.is_nat, D.comp_assoc]

structure Monad (C : Category) where
  m : Functor C C
  η : NatTrans (.id C) m
  μ : NatTrans (m.comp m) m
  is_left_unit : μ.vcomp (η.hcompRight m) = .id m
  is_right_unit : μ.vcomp (η.hcompLeft m) = .id m
  is_assoc : μ.vcomp (μ.hcompLeft m) = μ.vcomp (μ.hcompRight m)

[Aaron Liu]

The problem was, you used horizontal composition when you should have used vertical composition.

[Tammo Brinner]

Ahh thank you so much. I just really am still a beginner haha. Do you mind if i ask you another question?

[Aaron Liu]

Ask away!

[Tammo Brinner]

Aaron Liu schrieb:

Ask away!

This might seem a bit specific, but after spending a lot of time on the code, i ended up with the following fact, i desperately need:

theorem pi_congr {α : Sort u} {β γ : α → Sort v}
  (h_pointwise : ∀ x, β x = γ x) :
  ((x : α) → β x) = ((x : α) → γ x) :=
  congr_arg (fun T => (x : α) → T x) (funext h_pointwise)


theorem cast_fun_eq {α : Sort u} {β γ : α → Sort v}
  (f : ∀ x, β x) (h_pointwise : ∀ x, β x = γ x) :
  (fun x => cast (h_pointwise x) (f x)) = cast (pi_congr h_pointwise) f :=

So i need to know that casting a function along a type equality in the target is the same as doing the same thing pointwise. Of course this is completly clear mathematically but i just dont now how to deal with this in lean4. It almost seems like this should be definitionally true, but apparantly its not. Thank you so much for your help!

[Aaron Liu]

You should probably not be using cast, but writing a special cast function for whatever application you are using, so that more definitional equalities can hold. An example of this pattern would be docs#Fin.cast.

import Mathlib

-- defined in Init.SimpLemmas
recall pi_congr {α : Sort u} {β γ : α → Sort v}
    (h_pointwise : ∀ x, β x = γ x) :
    ((x : α) → β x) = ((x : α) → γ x) :=
  congr_arg (fun T => (x : α) → T x) (funext h_pointwise)


theorem cast_fun_eq {α : Sort u} {β γ : α → Sort v}
    (f : ∀ x, β x) (h_pointwise : ∀ x, β x = γ x) :
    (fun x => cast (h_pointwise x) (f x)) = cast (pi_congr h_pointwise) f := by
  have h : β = γ := funext h_pointwise
  subst h
  rfl

[Tammo Brinner]

Aaron Liu schrieb:

You should probably not be using cast, but writing a special cast function for whatever application you are using, so that more definitional equalities can hold. An example of this pattern would be docs#Fin.cast.

import Mathlib

-- defined in Init.SimpLemmas
recall pi_congr {α : Sort u} {β γ : α → Sort v}
    (h_pointwise : ∀ x, β x = γ x) :
    ((x : α) → β x) = ((x : α) → γ x) :=
  congr_arg (fun T => (x : α) → T x) (funext h_pointwise)


theorem cast_fun_eq {α : Sort u} {β γ : α → Sort v}
    (f : ∀ x, β x) (h_pointwise : ∀ x, β x = γ x) :
    (fun x => cast (h_pointwise x) (f x)) = cast (pi_congr h_pointwise) f := by
  have h : β = γ := funext h_pointwise
  subst h
  rfl

I feel like i dont have a choice but to cast if terms are equal mathematicall but not of the same type definitionally but only propositionally. But thanks for your help this worked!