English
A specialized equality for the pi-object comparison in the Yoneda setting, expressing functorial equivalence through product isomorphisms.
Русский
Специализированное равенство для сравнения π-объектов в контексте Yoneda, выражающее эквивалентность через изоморфизмы продукта.
LaTeX
$$$\\piComparison(\\text{yonedaPresheaf}'(Y), (X \\mapsto \\mathrm{op}(X))) = \\text{...}$$$
Lean4
theorem piComparison_fac {α : Type} (X : α → TopCat) :
piComparison (yonedaPresheaf'.{w, w'} Y) (fun x ↦ op (X x)) =
(yonedaPresheaf' Y).map ((opCoproductIsoProduct X).inv ≫ (TopCat.sigmaIsoSigma X).inv.op) ≫
(equivEquivIso (sigmaEquiv Y (fun x ↦ (X x).1))).inv ≫ (Types.productIso _).inv :=
by
rw [← Category.assoc, Iso.eq_comp_inv]
ext
simp only [yonedaPresheaf', unop_op, piComparison, types_comp_apply, Types.productIso_hom_comp_eval_apply,
Types.pi_lift_π_apply, comp_apply, TopCat.coe_of, unop_comp, Quiver.Hom.unop_op, sigmaEquiv, equivEquivIso_hom,
Equiv.toIso_inv, Equiv.coe_fn_symm_mk, comp_assoc, sigmaMk_apply, ← opCoproductIsoProduct_inv_comp_ι]
rfl
