reindex_hom_π — Mathlib

English

The hom component of the reindexed product interacts with projections as expected.

Русский

Гом-компонента реиндексации произведения взаимодействует с проекциями как следует.

LaTeX

$$$(\Pi\text{reindex }\varepsilon f)^{\mathrm{hom}} \circ \Pi f (\varepsilon b) = \Pi (f\circ \varepsilon) b$$$

Lean4

@[reassoc (attr := simp)]
theorem reindex_hom_π (b : β) : (Pi.reindex ε f).hom ≫ Pi.π f (ε b) = Pi.π (f ∘ ε) b :=
  by
  dsimp [Pi.reindex]
  simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj, Function.comp_apply,
    Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj, Discrete.natIso_inv_app, Iso.refl_inv,
    Category.id_comp]
  exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

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