fiberPullbackEquiv_symm_snd_apply

English

Equivalence relates fiberPullbackEquiv to an explicit pullback isomorphism.

Русский

Эквивалентность связывает fiberPullbackEquiv с явным изоморфизмом pullback.

LaTeX

$$$\\mathrm{fiberPullbackEquiv}(F,f,g) = (\\mathrm{PreservesPullback.iso}(F \\circ \\mathrm{incl}) f g) \\trans (\\mathrm{Types.pullbackIsoPullback}(F.map f)(F.map g))$$$

Lean4

@[simp]
theorem fiberPullbackEquiv_symm_snd_apply {X A B : C} {f : A ⟶ X} {g : B ⟶ X} (a : F.obj A) (b : F.obj B)
    (h : F.map f a = F.map g b) : F.map (pullback.snd f g) ((fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b :=
  by
  simp [fiberPullbackEquiv]
  change ((Types.pullbackIsoPullback _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (pullback.snd f g)) _ = _
  erw [PreservesPullback.iso_inv_snd, Types.pullbackIsoPullback_inv_snd]

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