sigmaComparison_eq_comp_isos — Mathlib

English

The sigma comparison map is equal to a certain composite of canonical isomorphisms involving finite coproducts and products.

Русский

Отображение сравнения по сигмами равно композиции канонических изоморфизмов, связанных с конечными coproduct и product.

LaTeX

$$$\\sigma\\text{Comparison} = X.mapIso(\\cdots) \\circ (\\text{PreservesProduct.iso } X) \\circ (\\text{Types.productIso } )$$$

Lean4

theorem sigmaComparison_eq_comp_isos :
    sigmaComparison X σ =
      (X.mapIso
            (opCoproductIsoProduct' (finiteCoproduct.isColimit.{u, u} (fun a ↦ of P (σ a)))
              (productIsProduct fun x ↦ Opposite.op (of P (σ x))))).hom ≫
        (PreservesProduct.iso X fun a ↦ ⟨of P (σ a)⟩).hom ≫
          (Types.productIso.{u, max u w} fun a ↦ X.obj ⟨of P (σ a)⟩).hom :=
  by
  ext x a
  simp only [Cofan.mk_pt, Fan.mk_pt, Functor.mapIso_hom, PreservesProduct.iso_hom, types_comp_apply,
    Types.productIso_hom_comp_eval_apply]
  have := congrFun (piComparison_comp_π X (fun a ↦ ⟨of P (σ a)⟩) a)
  simp only [types_comp_apply] at this
  rw [this, ← FunctorToTypes.map_comp_apply]
  simp only [sigmaComparison]
  apply congrFun
  congr 2
  rw [← opCoproductIsoProduct_inv_comp_ι]
  simp only [Opposite.unop_op, unop_comp, Quiver.Hom.unop_op, Category.assoc]
  simp only [opCoproductIsoProduct, ← unop_comp, opCoproductIsoProduct'_comp_self]
  erw [IsColimit.fac]
  rfl

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