English
The inclusion maps from fiber components to comapped fibers commute with comap operations; the equality g ≫ (sigmaIncl f a).op = (sigmaIncl f a).op ≫ (componentHom f g a).op holds.
Русский
Включения в сопряжённые фибры коммутируют с операциями comap; выполняется равенство, связывающее композицию и компоненту.
LaTeX
$$$g \; \gg \; (\sigmaIncl f a)^{\mathrm{op}} = (\sigmaIncl f a)^{\mathrm{op}} \; \gg \; (\mathrm{componentHom}\; f\; g\; a)^{\mathrm{op}}$$$
Lean4
/-- The counit is natural in `S : CompHausLike P` -/
@[simps!]
noncomputable def counitApp [HasExplicitFiniteCoproducts.{u} P] (Y : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w)
[PreservesFiniteProducts Y] : (functorToPresheaves.obj (Y.obj (op (CompHausLike.of P PUnit.{u + 1})))) ⟶ Y
where
app := fun ⟨S⟩ ↦ counitAppApp S Y
naturality := by
intro S T g
ext f
apply presheaf_ext (f.comap g.unop.hom)
intro a
simp only [op_unop, functorToPresheaves_obj_obj, types_comp_apply, functorToPresheaves_obj_map,
incl_of_counitAppApp, ← FunctorToTypes.map_comp_apply, incl_comap]
simp only [FunctorToTypes.map_comp_apply, incl_of_counitAppApp]
simp only [counitAppAppImage, ← FunctorToTypes.map_comp_apply, ← op_comp]
apply congrArg
exact image_eq_image_mk (g := g.unop) (a := a)
