map_pullback — Mathlib

English

Under pullbacks, the map object commutes with pullback up to isomorphism in a square diagram.

Русский

При вытягиваниях по диагонали отображения, map и pullback упорядочиваются до изоморфизма.

LaTeX

$$$\text{map pullback commute: } (map\ g) (\mathrm{pullback}\ f) = (\mathrm{pullback}\ k) (\mathrm{map}\ h)$$$

Lean4

theorem map_pullback [HasPullbacks C] {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {k : Z ⟶ W} [Mono h] [Mono g]
    (comm : f ≫ h = g ≫ k) (t : IsLimit (PullbackCone.mk f g comm)) (p : Subobject Y) :
    (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p) :=
  by
  revert p
  apply Quotient.ind'
  intro a
  apply Quotient.sound
  apply ThinSkeleton.equiv_of_both_ways
  · refine MonoOver.homMk (pullback.lift (pullback.fst _ _) _ ?_) (pullback.lift_snd _ _ _)
    change _ ≫ a.arrow ≫ h = (pullback.snd _ _ ≫ g) ≫ _
    rw [assoc, ← comm, pullback.condition_assoc]
  · refine
      MonoOver.homMk
        (pullback.lift (pullback.fst _ _)
          (PullbackCone.IsLimit.lift t (pullback.fst _ _ ≫ a.arrow) (pullback.snd _ _) _)
          (PullbackCone.IsLimit.lift_fst _ _ _ ?_).symm)
        ?_
    · rw [← pullback.condition, assoc]
      rfl
    · dsimp
      rw [pullback.lift_snd_assoc]
      apply PullbackCone.IsLimit.lift_snd

Похожие утверждения