Can two cones be proved equal?

Stream: new members

[Shanghe Chen]

Hi I reached a situation thinking if two cone can be proved equal or not similar to my last thread maybe:

import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

noncomputable section
universe v u v' u'

set_option autoImplicit false
-- set_option pp.all true

open CategoryTheory Functor Limits

variable {C: Type u} [Category.{v} C]
variable {D: Type u'} [Category.{v'} D]
variable [HasFiniteLimits D]
variable (F: C ⥤ D)
variable {X Y Z W: C} {f : X ⟶ Z} {g: Y ⟶ Z} (p : W ⟶ X) (q : W ⟶ Y) (w: p ≫ f = q ≫ g)

lemma cospanCompEq : (cospan f g) ⋙ F = (cospan (F.map f) (F.map g)) := by
  apply CategoryTheory.Functor.ext
  rintro (_|_|_) <;> rintro (_|_|_) <;> rintro f <;> cases f <;> simp
  rintro (_|_|_) <;> simp

def cone1 := (Cones.postcompose (eqToHom (cospanCompEq F))).obj (F.mapCone (PullbackCone.mk p q w))

def cone2 := (PullbackCone.mk (F.map p) (F.map q) (by repeat rw [←map_comp]; congr 1))

example : cone1 F p q w = cone2 F p q w := by
  sorry

example : limit.lift _ (cone1 F p q w) = limit.lift _ (cone2 F p q w) := by
  apply IsLimit.hom_ext
  apply limit.isLimit
  simp [cone1, cone2]
  rintro (_|_|_) <;> simp

Here I used CategoryTheory.Functor.ext proving that two cospans are equal, one F.map first and the other cospan first. And similarly I defined two cones. How to prove they are equal? I found no ext can be used.

[Shanghe Chen]

But their limit.lift can be proved equal using IsLimit.hom_ext. And I found that docs#CategoryTheory.Limits.Cone is not marked with @[ext]. Is it some hint for that cones should not be proved equal?

[Kevin Buzzard]

Equality of cones implies equality of objects in a category, which is evil. Mathematically do you really know that the points of those cones are equal? Or just isomorphic?

[Markus Himmel]

As Kevin suggests, it's usually easier to use natural isomorphism of functors instead of equality of functors and isomorphisms of cones instead of equality of cones:

def cospanCompEq : (cospan f g) ⋙ F ≅ (cospan (F.map f) (F.map g)) :=
  cospanCompIso _ _ _

def cone1 := (Cones.postcompose (cospanCompEq F).hom).obj (F.mapCone (PullbackCone.mk p q w))

def cone2 := (PullbackCone.mk (F.map p) (F.map q) (by repeat rw [←map_comp]; congr 1))

example : cone1 F p q w ≅ cone2 F p q w :=
  Cones.ext (Iso.refl _) (by rintro (_|_|_) <;> simp [cone1, cone2, cospanCompEq])

[Shanghe Chen]

Thank you for the suggestion! Yeah I am trying to switch to use isomorphism rather than equality too. It’s still quite hard to understand the "evil" part related to equalities. Though I get it that it could be hard to prove, but it seems using isomorphism rather than equality usually involves proving some related "hom equation"

[Shanghe Chen]

Kevin Buzzard said:

Equality of cones implies equality of objects in a category, which is evil. Mathematically do you really know that the points of those cones are equal? Or just isomorphic?

Yeah mathematically this issue is rarely shown up. In this specific case they do be equal though, since a diagram with shape $X \xrightarrow[]{f} Z \xleftarrow[]{g} Y$ (treated as a functor from $\bullet \rightarrow \bullet \leftarrow \bullet$) composing a functor $F$ same as $FX \xrightarrow[]{Ff} FZ \xleftarrow[]{Fg} FY$ is usually assumed implicitly in usual textbook. I am only realizing this is some different when writing it in Lean.

[Shanghe Chen]

For my original post, I found it can be proved equal if Cone.ext is supplied though (and it makes the limit is equal just using congr):

import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

noncomputable section
universe v u v' u'

set_option autoImplicit false
-- set_option pp.all true

open CategoryTheory Functor Limits

variable {C: Type u} [Category.{v} C]
variable {D: Type u'} [Category.{v'} D]
variable [HasFiniteLimits D]
variable (F: C ⥤ D)
variable {X Y Z W: C} {f : X ⟶ Z} {g: Y ⟶ Z} (p : W ⟶ X) (q : W ⟶ Y) (w: p ≫ f = q ≫ g)

lemma cospanCompEq : (cospan f g) ⋙ F = (cospan (F.map f) (F.map g)) := by
  apply CategoryTheory.Functor.ext
  rintro (_|_|_) <;> rintro (_|_|_) <;> rintro f <;> cases f <;> simp
  rintro (_|_|_) <;> simp

def cone1 := (Cones.postcompose (eqToHom (cospanCompEq F))).obj (F.mapCone (PullbackCone.mk p q w))

def cone2 := (PullbackCone.mk (F.map p) (F.map q) (by repeat rw [←map_comp]; congr 1))

attribute [ext] CategoryTheory.Limits.Cone
#print CategoryTheory.Limits.Cone.ext

lemma coneEq : cone1 F p q w = cone2 F p q w := by
  simp [cone1, cone2]
  ext
  -- prove that the vertexes are the same
  simp
  -- prove that the natural transformations from
  -- the vertex （treated as const functor） to the diagram
  -- are the same
  simp
  ext (_|_|_) <;> simp


example : limit.lift _ (cone1 F p q w) = limit.lift _ (cone2 F p q w) := by
  congr 1
  apply coneEq

[Dagur Asgeirsson]

(deleted) I didn't read enough above -- Markus already gave the solution I had in mind

[Shanghe Chen]

Dagur Asgeirsson said:

(deleted) I didn't read enough above -- Markus already gave the solution I had in mind

Oh it’s nice to see the solution using cospanCompIso for the limit part too. Could you please (re)post this?

[Dagur Asgeirsson]

Sure, adding

example : limit.lift _ (cone1 F p q w) = limit.lift _ (cone2 F p q w) := by
  dsimp [cone1, cone2]
  ext
  all_goals simp [cospanCompEq]

below what Markus wrote works

[Shanghe Chen]

Sure thank you! I will try this too later:tada: