fiberBinaryProductEquiv_symm_fst_apply

English

fiberBinaryProductEquiv F X Y equals a canonical comparison isomorphism.

Русский

fiberBinaryProductEquiv F X Y совпадает с каноническим сравнительным изоморфизмом.

LaTeX

$$$\\mathrm{Eq}(\\mathrm{fiberBinaryProductEquiv}(F,X,Y), (\\mathrm{PreservesLimitPair.iso}(F\\circ \\mathrm{incl}) X Y) \\trans (\\mathrm{Types.binaryProductIso}(F.obj X)(F.obj Y)).toEquiv)$$$

Lean4

@[simp]
theorem fiberBinaryProductEquiv_symm_fst_apply {X Y : C} (x : F.obj X) (y : F.obj Y) :
    F.map prod.fst ((fiberBinaryProductEquiv F X Y).symm (x, y)) = x :=
  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.fst) _ = _
  erw [PreservesLimitPair.iso_inv_fst, Types.binaryProductIso_inv_comp_fst]

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