English
The canonical map from the coproduct of fibers to the base fiber is an isomorphism in CompHausLike.LocallyConstant. It is the map sigmaIso.
Русский
Каноническая карта от coproduct-фибр к базовой фибре является изоморфизмом в CompHausLike.LocallyConstant; это карта sigmaIso.
LaTeX
$$$\sigma\mathrm{Iso} : (\mathrm{finiteCoproduct}(\mathrm{fiber}\ r)) \cong Q$$$
Lean4
/-- The counit is defined as follows: given a locally constant map `f : S → Y(*)`, let
`S = S₁ ⊔ ⋯ ⊔ Sₙ` be the corresponding decomposition of `S` into the fibers. We need to provide an
element of `Y(S)`. It suffices to provide an element of `Y(Sᵢ)` for all `i`. Let `yᵢ ∈ Y(*)` denote
the value of `f` on `Sᵢ`. Our desired element is the image of `yᵢ` under the canonical map
`Y(*) → Y(Sᵢ)`.
-/
noncomputable def counitAppApp (S : CompHausLike.{u} P) (Y : (CompHausLike.{u} P)ᵒᵖ ⥤ Type max u w)
[PreservesFiniteProducts Y] [HasExplicitFiniteCoproducts.{u} P] :
LocallyConstant S (Y.obj (op (CompHausLike.of P PUnit.{u + 1}))) ⟶ Y.obj ⟨S⟩ := fun r ↦
((inv (sigmaComparison Y (fun a ↦ (fiber r a).1))) ≫ (Y.mapIso (sigmaIso r).op).inv)
(counitAppAppImage r)
-- This is the key lemma to prove naturality of the counit:
