topCatAdjunctionUnit — Mathlib

Lean4
/-- The unit of the adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet` -/
@[simps val_app val_app_apply]
noncomputable def topCatAdjunctionUnit (X : LightCondSet.{u}) : X ⟶ X.toTopCat.toLightCondSet where
  val :=
    { app := fun S x ↦
        { toFun := fun s ↦ X.val.map ((of PUnit.{u + 1}).const s).op x
          continuous_toFun :=
            by
            suffices
              ∀ (i : (T : LightProfinite.{u}) × X.val.obj ⟨T⟩), Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩)
              from this ⟨_, _⟩
            rw [← continuous_sigma_iff]
            apply continuous_coinduced_rng }
      naturality := fun _ _ _ ↦ by
        ext
        simp only [TopCat.toSheafCompHausLike_val_obj, Opposite.op_unop, types_comp_apply,
          TopCat.toSheafCompHausLike_val_map, ← FunctorToTypes.map_comp_apply]
        rfl }
Похожие утверждения