Documentation

Mathlib.Topology.Category.CompHaus.Frm

The forgetful functor from TopCatᵒᵖ to Frm.

source
def topCatOpToFrm :
CategoryTheory.Functor TopCatᵒᵖ Frm

The forgetful functor from TopCatᵒᵖ to Frm.

Equations
    Instances For
      source
      @[simp]
      theorem topCatOpToFrm_map {X✝ Y✝ : TopCatᵒᵖ} (f : X✝ ⟶ Y✝) :
      topCatOpToFrm.map f = Frm.ofHom (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.unop))
      source
      @[simp]
      theorem topCatOpToFrm_obj_coe (X : TopCatᵒᵖ) :
      ↑(topCatOpToFrm.obj X) = TopologicalSpace.Opens ↑(Opposite.unop X)
      source
      instance CompHausOpToFrame.faithful :
      (compHausToTop.op.comp topCatOpToFrm).Faithful