fiberEqualizerEquiv_symm_ι_apply

English

Applying the inverse of the equalizer-projection map to a fiber element recovers the original element.

Русский

Обратный к проекции равнозазначающего возвращает исходный элемент фибры.

LaTeX

$$$F.map(\\mathrm{equalizer.}\\!\\mathrm{ι} f g)\\left((\\mathrm{fiberEqualizerEquiv}(F,f,g))^{-1}\\langle x,h\\rangle\\right) = x$$$

Lean4

@[simp]
theorem fiberEqualizerEquiv_symm_ι_apply {X Y : C} {f g : X ⟶ Y} (x : F.obj X) (h : F.map f x = F.map g x) :
    F.map (equalizer.ι f g) ((fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x :=
  by
  simp [fiberEqualizerEquiv]
  change ((Types.equalizerIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map (equalizer.ι f g)) _ = _
  erw [PreservesEqualizer.iso_inv_ι, Types.equalizerIso_inv_comp_ι]

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