prove that perserving pullback also preserves pullback.map?

Stream: new members

[Shanghe Chen]

Hi recently in an exercise I frequently need to prove something related to different limits commute like:

import Mathlib.CategoryTheory.Limits.Preserves.Limits
import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
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

variable {C: Type u} [Category.{v} C] [HasLimits C]
variable {D: Type u'} [Category.{v'} D] [HasLimits D]
variable (F: C ⥤ D) [PreservesLimits F]

def preserve_pullback {X Y Z : C} (f: X ⟶ Z) (g : Y ⟶ Z) :
    F.obj (pullback f g) ≅ pullback (F.map f) (F.map g) := by
  simp only [pullback]
  let i := preservesLimitIso F (cospan f g)
  let a := cospanCompIso F f g
  let i' := conePointsIsoOfNatIso (limit.isLimit _) (limit.isLimit _) a
  simp at i i'; exact i ≪≫ i'

def coyoneda_pullback_iso_app_comp_map {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)  (g₁ : Y ⟶ T)
    (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
    (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) :
    F.map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ (preserve_pullback F g₁ g₂).hom =
    (preserve_pullback F f₁ f₂).hom ≫  (pullback.map _ _ _ _ (F.map i₁) (F.map i₂) (F.map i₃) (by rw [←F.map_comp, eq₁]; simp) (by rw [←F.map_comp, eq₂]; simp)) := by
  sorry

any easy way to do this?

[Andrew Yang]

The first is docs#CategoryTheory.Limits.PreservesPullback.iso

[Shanghe Chen]

Thank you! I am checking this

[Shanghe Chen]

And how about this?

def preserve_pullback_hom {X Y Z W : C} (f: X ⟶ Z) (g : Y ⟶ Z) (A : C)
    (p: W ⟶ X) (q: W ⟶ Y) (w: p ≫ f = q ≫ g) :
    F.map (pullback.lift p q w) ≫ (preserve_pullback F f g).hom
    = (pullback.lift (F.map p) (F.map q) (by rw [←F.map_comp, w]; simp)) := by
  -- TODO any way to deduplicate this?
  let a := cospanCompIso F f g
  -- P and Q are copied from the goal...
  let P := limit.isLimit ((cospan f g).comp F)
  let Q := limit.isLimit (cospan (F.map f) (F.map g))
  let r := F.mapCone (PullbackCone.mk _ _ w)
  let c : P.lift r ≫ (conePointsIsoOfNatIso P Q a).hom = Q.map r a.hom :=
    lift_comp_conePointsIsoOfNatIso_hom P Q a
  simp [a,P,Q,r] at c; rw [preserve_pullback]
  simp [pullback.lift]; rw [c, IsLimit.map, limit.lift];
  apply hom_ext; apply limit.isLimit
  rintro (_|_|_) <;> simp

[Shanghe Chen]

Is it contained in mathlib? I found that both loogle and moogle seem not quite helpful in finding theorem about category theory...

[Shanghe Chen]

Oh I find it now: docs#CategoryTheory.Limits.PreservesPullback.iso_hom

[Shanghe Chen]

Yeah... maybe I check the whole file first :tada:

[Andrew Yang]

example {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)  (g₁ : Y ⟶ T)
    (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
    (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) :
    F.map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ (PreservesPullback.iso F g₁ g₂).hom =
    (PreservesPullback.iso F f₁ f₂).hom ≫ (pullback.map _ _ _ _ (F.map i₁) (F.map i₂) (F.map i₃)
    (by rw [← F.map_comp, eq₁]; simp) (by rw [← F.map_comp, eq₂]; simp)) := by
  ext <;> simp only [assoc, limit.lift_π, id_eq, eq_mpr_eq_cast, mk_pt, mk_π_app]
  · rw [PreservesPullback.iso_hom_fst_assoc, PreservesPullback.iso_hom_fst,
      ← map_comp, pullback.lift_fst, map_comp]
  · rw [PreservesPullback.iso_hom_snd_assoc, PreservesPullback.iso_hom_snd,
      ← map_comp, pullback.lift_snd, map_comp]

[Shanghe Chen]

wow excellent! Never thought that here the proof can use ext

[Andrew Yang]

It calls docs#CategoryTheory.Limits.pullback.hom_ext

[Andrew Yang]

After #13321 the proof should be ext <;> simp

[Shanghe Chen]

Ah let me try to read this too. I used IsLimit.hom_ext before but did not saw pullback.hom_ext hhh

[Shanghe Chen]

Yeah ... proving this kind of commute diagrams is a little cubersome to me and usually omit in textbook...

[Andrew Yang]

Usually ext <;> simp should work. If not then it usually indicates a missing simp lemma.

[Shanghe Chen]

yeah I got another one too hhh, it's not that hard if found one already :tada:

example {X Y : C} (f: X ⟶ Y)  :
    F.map (pullback.diagonal f) ≫ (PreservesPullback.iso F f f).hom = pullback.diagonal (F.map f) := by
  ext <;> simp;
  · rw [PreservesPullback.iso_hom_fst, ← map_comp, pullback.diagonal];
    simp
  · rw [PreservesPullback.iso_hom_snd, ← map_comp, pullback.diagonal];
    simp

[Shanghe Chen]

Andrew Yang 发言道：

After #13321 the proof should be ext <;> simp

Hi I notice that this mr has been merged! Now just ext <;> simp is enough for the proof :tada:

[Shanghe Chen]

In a specific case I have to explicitly apply pullback.hom_ext for ext seems using another extension result though:

[Shanghe Chen]

import Mathlib.CategoryTheory.Limits.Yoneda
import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

noncomputable section
universe 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]
variable {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S)  (g₁ : Y ⟶ T)
    (g₂ : Z ⟶ T) (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T)
    (eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁) (eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂) (A : C)
local notation "F" => (coyoneda.obj (op A))
-- weird, it mush be wrap with parens
-- #check (F).map
def coyoneda_pullback_iso_app_comp_map  :
    (F).map (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂) ≫ (PreservesPullback.iso F g₁ g₂).hom =
        (PreservesPullback.iso F f₁ f₂).hom ≫ (pullback.map _ _ _ _ ((F).map i₁) ((F).map i₂) ((F).map i₃)
          (by rw [←(F).map_comp, eq₁]; simp) (by rw [←(F).map_comp, eq₂]; simp)) := by
  -- cannot write `ext` here, it will use other `ext` rules
  apply pullback.hom_ext <;> simp

[Kevin Buzzard]

Does ext1 work?

There is an art to ext lemmas. I learnt a lot about them from examining @Eric Wieser 's PhD thesis recently.

[Shanghe Chen]

Yeah indeed ext1 <;> simp works!

[Shanghe Chen]

Kevin Buzzard 发言道：

There is an art to ext lemmas. I learnt a lot about them from examining Eric Wieser 's PhD thesis recently.

Hi Kevin do you mind sharing the title of Eric's PhD thesis? I didnt find it, kind of interested in the ext lemmas too

[Eric Wieser]

I've extracted the ext section into a standalone paper, which I can share later today. My thesis is not yet searchable online, so knowing the name will not help you much!

[Shanghe Chen]

Ah I get it now. Thank you very much!

[Eric Wieser]

A little delayed, but here's that paper:
chaining-extensionality.pdf

[Shanghe Chen]

Thank you very much for sharing the paper!

[Shanghe Chen]

Btw it seems the unicode ℳ is not rendered in section A.2 theorem DirectSum.decompose_lhom_ext