toTopCatMap — Mathlib

Lean4
/-- The map part of the functor `LightCondSet ⥤ TopCat` -/
@[simps!]
def toTopCatMap : X.toTopCat ⟶ Y.toTopCat :=
  TopCat.ofHom
    { toFun := f.val.app ⟨LightProfinite.of PUnit⟩
      continuous_toFun := by
        rw [continuous_coinduced_dom]
        apply continuous_sigma
        intro ⟨S, x⟩
        simp only [Function.comp_apply, coinducingCoprod]
        rw [show (fun (a : S) ↦ f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u + 1}).const a).op x)) = _ from
            funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u + 1}).const a).op x]
        exact continuous_coinducingCoprod _ _ }
Похожие утверждения