pullback_map_eq_pullbackFstFstIso_inv

English

Let X, Y, S and X', Y', S' be objects in a category with pullbacks. Given f : X → S, g : Y → S, f' : X' → S', g' : Y' → S', arrows i1 : X → X', i2 : Y → Y', i3 : S → S' and commuting data e1 : f ≫ i3 = i1 ≫ f' and e2 : g ≫ i3 = i2 ≫ g' with i3 monomorphic, the canonical pullback map from the pullback of (f,g) to the pullback of (f',g') is the inverse of a canonical isomorphism, followed by the projection of the pullback (snd) and then the projection (fst).

Русский

Пусть в категории существуют волокна (pullback). Пусть данные f,g и f',g', i1,i2,i3, e1,e2 удовлетворяют необходимым commuting условиям и i3 моно. Тогда каноническое отображение pullback(f,g) → pullback(f',g') равно композиции инверсии канонического изоморфизма pullbackFstFstIso с проекция pullback.snd и затем pullback.fst.

LaTeX

$$$\\displaystyle pullback.map\\ f\\ g\\ f'\\ g'\\ i_1\\ i_2\\ i_3\\ e_1\\ e_2 = (pullbackFstFstIso\\ f\\ g\\ f'\\ g'\\ i_1\\ i_2\\ i_3\\ e_1\\ e_2).inv \\; \\circ\\; pullback.snd\\ _\\ _ \\; \\circ\\; pullback.fst\\ _\\ _ $$$

Lean4

theorem pullback_map_eq_pullbackFstFstIso_inv {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S')
    (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [Mono i₃] :
    pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ =
      (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ :=
  by simp only [pullbackFstFstIso_inv, lift_snd_assoc, lift_fst]

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