counit — Mathlib

English

The unit of the adjunction between LocallyConstant functor and the forgetful functor from Condensed LocallyConstant is an isomorphism.

Русский

Единица адъюнкции между локально-константным функтором и забывающим функтором является изоморфизмом.

LaTeX

$$$\text{unitIso} : \mathbf{1} \cong (\text{LocallyConstant functor})$$$

Lean4

/-- The counit is natural in both `S : CompHausLike P` and
`Y : Sheaf (coherentTopology (CompHausLike P)) (Type (max u w))` -/
@[simps]
noncomputable def counit [HasExplicitFiniteCoproducts.{u} P] :
    haveI := CompHausLike.preregular hs
    (sheafSections _ _).obj ⟨CompHausLike.of P PUnit.{u + 1}⟩ ⋙ functor.{u, w} P hs ⟶
      𝟭 (Sheaf (coherentTopology (CompHausLike.{u} P)) (Type (max u w)))
    where
  app
    X :=
    haveI := CompHausLike.preregular hs
    ⟨counitApp X.val⟩
  naturality X Y
    g := by
    have := CompHausLike.preregular hs
    apply Sheaf.hom_ext
    simp only [functor, Functor.comp_obj, Functor.flip_obj_obj, sheafToPresheaf_obj, Functor.id_obj, Functor.comp_map,
      Functor.flip_obj_map, sheafToPresheaf_map, Sheaf.comp_val, Functor.id_map]
    ext S (f : LocallyConstant _ _)
    simp only [FunctorToTypes.comp, counitApp_app]
    apply presheaf_ext (f.map (g.val.app (op (CompHausLike.of P PUnit.{u + 1}))))
    intro a
    simp only [op_unop, functorToPresheaves_map_app, incl_of_counitAppApp]
    apply presheaf_ext (f.comap (sigmaIncl _ _).hom)
    intro b
    simp only [counitAppAppImage, ← FunctorToTypes.map_comp_apply, ← op_comp, map_apply, IsTerminal.comp_from,
      ← map_preimage_eq_image_map]
    change (_ ≫ Y.val.map _) _ = (_ ≫ Y.val.map _) _
    simp only [← g.val.naturality]
    rw [show
        sigmaIncl (f.comap (sigmaIncl (f.map _) a).hom) b ≫ sigmaIncl (f.map _) a =
          CompHausLike.ofHom P (X := fiber _ b) (sigmaInclIncl f _ a b) ≫ sigmaIncl f (Fiber.mk f _)
        by ext; rfl]
    simp only [op_comp, Functor.map_comp, types_comp_apply, incl_of_counitAppApp]
    simp only [counitAppAppImage, ← FunctorToTypes.map_comp_apply, ← op_comp]
    rw [mk_image]
    change (X.val.map _ ≫ _) _ = (X.val.map _ ≫ _) _
    simp only [g.val.naturality]
    simp only [types_comp_apply]
    have := map_preimage_eq_image (f := g.val.app _ ∘ f) (a := a)
    simp only [Function.comp_apply] at this
    rw [this]
    apply congrArg
    symm
    convert (b.preimage).prop
    exact (mem_iff_eq_image (g.val.app _ ∘ f) _ _).symm

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