English
The inverse component respects composition: composing maps and then applying the inverse equals mapping the inverse along the composition.
Русский
Обратный компонент сохраняет композицию: применение обратной части к композиции равняется композиции после применения обратного к компонентам.
LaTeX
$$$(\\text{isoFinYonedaComponents } F X).inv (f \\circ g) = F.map g^{op} ((\\text{isoFinYonedaComponents } F Y).inv f).$$$
Lean4
theorem isoFinYonedaComponents_inv_comp {X Y : Profinite.{u}} [Finite X] [Finite Y] (f : Y → F.obj ⟨Profinite.of PUnit⟩)
(g : X ⟶ Y) : (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f) :=
by
apply injective_of_mono (isoFinYonedaComponents F X).hom
simp only [CategoryTheory.inv_hom_id_apply]
ext x
rw [isoFinYonedaComponents_hom_apply]
simp only [← FunctorToTypes.map_comp_apply, ← op_comp, CompHausLike.const_comp, ← isoFinYonedaComponents_hom_apply,
CategoryTheory.inv_hom_id_apply, Function.comp_apply]
