fiberBinaryProductEquiv_symm_snd_apply

English

The second projection recovers the second component after applying the inverse equivalence.

Русский

Проекция snd восстанавливает вторую компоненту после применения обратной эквив.

LaTeX

$$$\\forall x:\\mathrm{F.obj}(X),\\forall y:\\mathrm{F.obj}(Y),\\forall h:\\mathrm{F.map}(f)x=\\mathrm{F.map}(g)y,\\; F.map (\\mathrm{pullback}.snd f g)( (\\mathrm{fiberBinaryProductEquiv}(F,X,Y))^{-1}\\langle x,y\\rangle ) = y$$$

Lean4

@[simp]
theorem fiberBinaryProductEquiv_symm_snd_apply {X Y : C} (x : F.obj X) (y : F.obj Y) :
    F.map prod.snd ((fiberBinaryProductEquiv F X Y).symm (x, y)) = y :=
  by
  simp only [fiberBinaryProductEquiv, comp_obj, FintypeCat.incl_obj, Iso.toEquiv_comp, Equiv.symm_trans_apply,
    Iso.toEquiv_symm_fun]
  change ((Types.binaryProductIso _ _).inv ≫ _ ≫ (F ⋙ FintypeCat.incl).map prod.snd) _ = _
  erw [PreservesLimitPair.iso_inv_snd, Types.binaryProductIso_inv_comp_snd]

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