Help for reviewing and improving a code for coyoneda and ...

Stream: new members

[Shanghe Chen]

Hi for some exercises in category theory I wrote the following code for proving the following second diagram is commute, where h is some homset functor Hom(A,-)
1378F096-8FE7-48C7-A056-380C3FA3D0EF.jpg

[Shanghe Chen]

import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Iso
import Mathlib.CategoryTheory.Equivalence
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.NatIso
import Mathlib.CategoryTheory.Yoneda
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
import Mathlib.CategoryTheory.Limits.Shapes.CommSq
import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Limits.Shapes.Types
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.FunctorCategory
import Mathlib.CategoryTheory.Limits.Preserves.Limits
import Mathlib.CategoryTheory.Limits.IsLimit
import Mathlib.CategoryTheory.Limits.Cones
import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Yoneda
import Mathlib.CategoryTheory.Limits.Presheaf
import Mathlib.CategoryTheory.Limits.Preserves.Limits


noncomputable section
universe v u v' u'

set_option autoImplicit false
-- set_option pp.all true

open CategoryTheory Category Functor Limits IsLimit Cone Opposite PullbackCone Types

variable {C: Type u} [Category.{v} C] [HasFiniteLimits C]

-- graph for f
def Γ {X Y S: C} {u : X ⟶ S} {v : Y ⟶ S} (f : X ⟶ Y) (w : f ≫ v = u) : X ⟶ pullback u v := by
  apply pullback.lift
  case h => exact 𝟙 X
  case k => exact f
  case w => aesop_cat

/-- cones factor theough pullback -/
def pullback.homIso {X Y S: C} (u : X ⟶ S) (v: Y ⟶ S) (Z : C) :
    (Z ⟶ pullback u v) ≃ {x: (Z ⟶ X) × (Z ⟶ Y) // x.1 ≫ u = x.2 ≫ v} where
  toFun k := ⟨⟨k ≫ pullback.fst, k ≫ pullback.snd⟩, by simp; congr 1; simp [pullback.fst, pullback.snd, cospan]⟩
  invFun := by rintro ⟨⟨x, y⟩, p⟩; exact pullback.lift x y p
  left_inv x := by apply pullback.hom_ext <;>
    simp only [limit.lift_π, id_eq, eq_mpr_eq_cast, mk_pt, mk_π_app]
  right_inv := by
    rintro ⟨⟨x, y⟩, p⟩
    apply Subtype.ext
    simp only [limit.lift_π, mk_pt, mk_π_app]

local notation "h" => fun (A: C) => coyoneda.obj (op A)

-- coyoneda commutes with pullback
def coyoneda_pullback_iso_app {X Y S A: C} (u : X ⟶ S) (v : Y ⟶ S):
    (h A).obj (pullback u v) ≅ pullback ((h A).map u) ((h A).map v) :=
  (equivEquivIso.toFun (pullback.homIso _ _ _)) ≪≫ (Types.pullbackIsoPullback (. ≫ _) (. ≫ _)).symm

-- in types cone commutes with two limit
-- one from choice and one from construction
lemma pullbackIsoPullback_lift_comp {W X Y S : Type u} (u : X ⟶ S) (v : Y ⟶ S) (f: W ⟶ X) (g: W ⟶ Y) (e: f ≫ u = g ≫ v)
  : (Types.pullbackLimitCone u v).isLimit.lift (PullbackCone.mk _ _ e) ≫ (Types.pullbackIsoPullback u v).inv =
    pullback.lift f g e:=
  lift_comp_conePointUniqueUpToIso_hom (Types.pullbackLimitCone u v).isLimit (limit.isLimit (cospan u v))

/--
-- graph/coyoned/pullback commute
This is slow
-/
def coyoneda_Γ_iso_app_comm {X Y S A : C} (u : X ⟶ S) (v : Y ⟶ S) (f : X ⟶ Y) (w : f ≫ v = u) :
    (h A).map (Γ f w) ≫ (coyoneda_pullback_iso_app u v).hom = Γ ((h A).map f) (by aesop_cat) := by
  rw [coyoneda_pullback_iso_app, Iso.trans_hom, Iso.symm_hom]
  have comp := pullbackIsoPullback_lift_comp ((h A).map u) ((h A).map v) (𝟙 (h A).obj X) ((h A).map f)
      (by simp [coyoneda]; aesop_cat)
  conv_rhs at comp => simp [coyoneda]
  conv_rhs => rw [Γ]; simp [coyoneda]; rw [←comp]
  clear comp; simp [coyoneda]; ext x; all_goals
  rw [Γ, pullback.homIso]; simp
  conv_rhs => rw [PullbackCone.isLimitAux]; simp

[Shanghe Chen]

Any advice for the code here, especially the last? It’s quite slow. And I want to use more established results in mathlib:blush:

[Shanghe Chen]

Btw there is also some code about the equalizer very similar to the above want some advice too, for showing h(Eq(f,g)) → Eq(h(f), h(g)) → h(X) same as h(Eq(f,g)) → h(X) that is applying h=Hom(A,-)

/--
 This is the composition of two isomorphism
-/
def coyoneda_equalizer_iso_app {X Y A : C} (f: X ⟶ Y) (g : X ⟶ Y) :
    (h A).obj (equalizer f g) ≅ equalizer ((h A).map f) ((h A).map g) :=
    (equivEquivIso.toFun (Fork.IsLimit.homIso (limit.isLimit _) _)) ≪≫ ((Types.equalizerIso _ _).symm)


def coyoneda_equalizer_iso_app_comm {X Y A : C} (f: X ⟶ Y) (g : X ⟶ Y) :
    (coyoneda_equalizer_iso_app f g).hom ≫ (equalizer.ι ((h A).map f) ((h A).map g)) = (h A).map (equalizer.ι f g) := by
  rw [coyoneda_equalizer_iso_app, Iso.trans_hom, Iso.symm_hom]
  slice_lhs 2 3 => simp [coyoneda, Types.equalizerIso_inv_comp_ι]
  simp; ext x; simp [homIso_hom]
  conv_lhs => simp [Fork.IsLimit.homIso]

[Shanghe Chen]

Hi I now realise that it may be easier to use directly the fact that $Hom(A, -)$ preserves limit. I got the obj iso part from the related thread

def coyoneda_equalizer_iso_app' {X Y A : C} (f: X ⟶ Y) (g : X ⟶ Y) :
    (coyoneda.obj (op A)).obj (equalizer f g) ≅ equalizer ((coyoneda.obj (op A)).map f) ((coyoneda.obj (op A)).map g) := by
  simp only [equalizer, coyoneda]
  let i := preservesLimitIso (coyoneda.obj (op A)) (parallelPair f g)
  let a := diagramIsoParallelPair ((parallelPair f g) ⋙ (coyoneda.obj (op A)))
  let i' := conePointsIsoOfNatIso (limit.isLimit _) (limit.isLimit _) a
  simp at i i'
  exact i ≪≫ i'

def coyoneda_equalizer_iso_app_comm' {X Y A : C} (f: X ⟶ Y) (g : X ⟶ Y) :
    (coyoneda_equalizer_iso_app' f g).hom ≫ (equalizer.ι ((coyoneda.obj (op A)).map f) ((coyoneda.obj (op A)).map g)) = (coyoneda.obj (op A)).map (equalizer.ι f g) := by
  let c := preservesLimitsIso_hom_π (coyoneda.obj (op A)) (parallelPair f g)
       WalkingParallelPair.zero
  simp only [coyoneda]
  ext x
  sorry

But not the morphism commute part for the equalizer case. Any idea please?

[Shanghe Chen]

Btw simp at c results in c: True. Kind of werid