English
For f : Y → F(1) and g : X → Y, the inverse component satisfies (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f).
Русский
Для f : Y → F(1) и g : X → Y, обратный компонент удовлетворяет (isoFinYonedaComponents F X).inv (f ∘ g) = F.map g.op ((isoFinYonedaComponents F Y).inv f).
LaTeX
$$$(\text{isoFinYonedaComponents } F X)^{-1}(f \circ g) = F.map\,g^{\mathrm{op}}\big((\text{isoFinYonedaComponents } F Y)^{-1} f\big)$$$
Lean4
theorem isoFinYonedaComponents_inv_comp {X Y : LightProfinite.{u}} [Finite X] [Finite Y]
(f : Y → F.obj ⟨LightProfinite.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]
