The Yoneda lemma and the diagonal base change diagram

Stream: new members

[Shanghe Chen]

Hi I am trying to prove the diagonal base change diagram is cartesian for some exercises, following https://math.stackexchange.com/a/4648573/195865 but stuck at the very begining. The setup is:

import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.CommSq
import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Presheaf

noncomputable section
universe v u

set_option autoImplicit false

open CategoryTheory
open Category
open Limits

variable (C: Type u) [Category.{v} C] [HasFiniteLimits C]
variable (X₁ X₂ Y Z : C)
variable (f₁: X₁ ⟶ Y) (f₂: X₂ ⟶ Y) (g: Y ⟶ Z)

[Shanghe Chen]

Then I defined the diagram:

/--
 the morphism X₁ ×Y X₂ -> X₁ ×Z X₂
-/
local notation "p" => pullback.mapDesc f₁ f₂ g
/--
 the diagonal morphism Y -> Y ×Z Y
-/
local notation "d" => pullback.diagonal g
/--
 the morphism X₁ ×Y X₂ -> Y
 there are two choice for it, just pick up one
-/
local notation "h" => (pullback.fst ≫ f₁ : pullback f₁ f₂ ⟶ Y)
/--
the morphism X₁ ×Z X₂ -> Y ×Z Y
-/
local notation "q" => (pullback.map (f₁ ≫ g) (f₂ ≫ g) g g f₁ f₂ (𝟙 Z) (comp_id _) (comp_id _))

/--
 the diagonal base change diagram
   X₁ ×Y X₂ --> X₁ ×Z X₂
      | ⌟           |
      |             |
      v             v
      Y  ------> Y ×Z Y
  is cartesian
this will be proved via the Yoneda lemma.
see <https://math.stackexchange.com/a/4648573/195865>
-/
class DiagonalBaseChangeDiagram : Prop where
  isPullback : IsPullback p h q d

[Shanghe Chen]

But when I tried to apply an instance of it for presheaves on C like:

instance diagonalBaseChangeDiagramForPresheaf (X₁ X₂ Y Z : Cᵒᵖ ⥤ Type v)
     (f₁: X₁ ⟶ Y) (f₂: X₂ ⟶ Y) (g: Y ⟶ Z) :
  DiagonalBaseChangeDiagram (Cᵒᵖ ⥤ Type v) X₁ X₂ Y Z f₁ f₂ g := sorry

I got an error:

stuck at solving universe constraint
  v =?= max v ?u.23323
while trying to unify
  UnivLE.{max v ?u.23322, v}
with
  (α : ∀ (α : Type (max v ?u.23323)), Small.{max v ?u.23323, max v ?u.23323} α) →
    (∀ (α : Type (max v ?u.23323)), Small.{max v ?u.23323, max v ?u.23323} α) α

[Shanghe Chen]

I am quite confused in why there is some universe issue here. The following naive example does work:

import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.CommSq
import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Presheaf
open CategoryTheory
open Category
open Limits

universe v u

variable (C: Type u) [Category.{v} C]
variable {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z)

class IsPullBackClass : Prop where
  isPullback : IsPullback fst snd f g


#check IsPullBackClass C
#check IsPullBackClass (Cᵒᵖ ⥤ Type u)
#check IsPullBackClass (Cᵒᵖ ⥤ Type v)


instance isPullBackClassForPresheaf (P X Y Z : Cᵒᵖ ⥤ Type v)
     (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) :
  IsPullBackClass (Cᵒᵖ ⥤ Type v) fst snd f g := sorry

Thank you in advance :heart:

[Joël Riou]

I am not sure what is the problem, but first, I would suggest not using class (which has a different status in Lean as compared to structure), and prove a lemma rather than an instance. I would also replace variable (X₁ X₂ Y Z : C) by variable {X₁ X₂ Y Z : C} because the objects can be deduced from the types of the given morphisms.

[Shanghe Chen]

Yeah thank you for the advice. I am changing it to

lemma diagonalBaseChangeDiagramForType {X₁ X₂ Y Z : Type v}
     (f₁: X₁ ⟶ Y) (f₂: X₂ ⟶ Y) (g: Y ⟶ Z) :
  IsPullback p h q d := sorry

lemma diagonalBaseChangeDiagramForPresheaf {X₁ X₂ Y Z : Cᵒᵖ ⥤ Type v}
     (f₁: X₁ ⟶ Y) (f₂: X₂ ⟶ Y) (g: Y ⟶ Z) :
  IsPullback p h q d := sorry

/--
 the diagonal base change diagram

   X₁ ×Y X₂ --> X₁ ×Z X₂
      | ⌟           |
      |             |
      v             v
      Y  ------> Y ×Z Y
  is cartesian

this will be proved via the Yoneda lemma.
see <https://math.stackexchange.com/a/4648573/195865>
TODO prove this via diagonalBaseChangeDiagramForPresheaf,
     i.e., it suffices to check it's pullback in the category of sets
-/
lemma diagonalBaseChangeDiagram : IsPullback p h q d := sorry

and it reports no error :tada:

[Shanghe Chen]

Btw is this result contained in Mathlib?