Not equalizer

Stream: new members

[Noah Anderson]

How can I state "something is not an equalizer" in Lean?

For example, in RingCat, the injection $\mathbb{Z}$ into $\mathbb{Q}$ is not the equalizer of any two homomorphisms starting from $\mathbb{Q}$

open CategoryTheory

def Z : RingCat := RingCat.of ℤ

def Q : RingCat := RingCat.of ℚ

def i : Z ⟶ Q := RingCat.ofHom (Int.castRingHom ℚ)

variable {C : RingCat} (f g : Q ⟶ C)

[Noah Anderson]

Cause I noticed that CategoryTheory.Limits.equalizer directly returns an object in RingCat, so I can't write Limits.equalizer f g ≠ i

[Jihoon Hyun]

(deleted)

[Markus Himmel]

You could state it like this:

import Mathlib
open CategoryTheory Limits

def Z : RingCat := RingCat.of ℤ

def Q : RingCat := RingCat.of ℚ

def i : Z ⟶ Q := RingCat.ofHom (Int.castRingHom ℚ)

variable {C : RingCat} (f g : Q ⟶ C)

example (h₀ : i ≫ f = i ≫ g) (h : IsLimit (Fork.ofι i h₀)) : False := sorry

This constructs an explicit equalizer diagram Fork.ofι i h₀ and claims that there is a contradiction if this diagram is limiting.

[Markus Himmel]

Mathlib also contains "being an equalizer of something" as docs#CategoryTheory.RegularMono, so another way of packaging it is

import Mathlib
open CategoryTheory Limits

def Z : RingCat := RingCat.of ℤ

def Q : RingCat := RingCat.of ℚ

def i : Z ⟶ Q := RingCat.ofHom (Int.castRingHom ℚ)

example [RegularMono i] : False := sorry

[Noah Anderson]

fantastic, thanks!

[Noah Anderson]

Sorry, a follow-up question, I failed to fill in the conditions for Limits.Types.unique_of_type_equalizer in the code below:

example [regular : RegularMono i] : False := by
  have comp := regular.w
  have isLimit := regular.isLimit
  have := @Limits.Types.unique_of_type_equalizer Z Q (regular.Z) i (regular.left) (regular.right)

  sorry

The problem is that, it asks for a

⇑(ConcreteCategory.hom i) ≫ ⇑(ConcreteCategory.hom RegularMono.left) =
      ⇑(ConcreteCategory.hom i) ≫ ⇑(ConcreteCategory.hom RegularMono.right)

whereas I only have

i ≫ RegularMono.left = i ≫ RegularMono.right

how can I convert it to the form it demands? (or perhaps can anyone explain the difference?) Thanks!

[Noah Anderson]

and it also asks for

Limits.IsLimit (Limits.Fork.ofι (⇑(ConcreteCategory.hom i)) (⇑(ConcreteCategory.hom i) ≫ ⇑(ConcreteCategory.hom RegularMono.left) =
      ⇑(ConcreteCategory.hom i) ≫ ⇑(ConcreteCategory.hom RegularMono.right)))

but I got only

Limits.IsLimit (Limits.Fork.ofι i (i ≫ RegularMono.left = i ≫ RegularMono.right))

[Markus Himmel]

The statement you're trying to invoke is about the category of types (i.e., what would be called the category of sets in pen-and-paper mathematics), but your other statements live in the category of rings. So to massage comp into the right form you could do apply_fun (forget Ring).map comp (to say "if two ring homomorphisms are equal, then they are equal as functions between sets"). To get the right IsLimit statement, you'll somehow need to use that the forgetful functor preserves limits. Mathlib knows that (docs#RingCat.forget_preservesLimits), and the magic incantation is docs#CategoryTheory.Limits.isLimitForkMapOfIsLimit, so here is how you could make progress:

import Mathlib
open CategoryTheory Limits

def Z : RingCat := RingCat.of ℤ

def Q : RingCat := RingCat.of ℚ

def i : Z ⟶ Q := RingCat.ofHom (Int.castRingHom ℚ)

example [regular: RegularMono i] : False := by
  have comp := regular.w
  have isLimit := regular.isLimit
  have := @Limits.Types.unique_of_type_equalizer Z Q (regular.Z) i (regular.left) (regular.right)
  apply_fun (forget RingCat).map at comp
  have := this comp (isLimitForkMapOfIsLimit (forget RingCat) regular.w regular.isLimit)

Many nice statements about limits in the category of types like unique_of_type_equalizer are stated more generally for concrete categories where the forgetful functor preserves the relevant limits, but unfortunately the relevant result correponding to unique_of_type_equalizer seems to be missing.

[Noah Anderson]

thank you so much! its indeed a magic to me

[Kevin Buzzard]

Lean does not do magic :-) (but this Zulip has some people that can do magic)