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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem topCatOpToFrm_map {X✝ Y✝ : TopCatᵒᵖ} (f : X✝ ⟶ Y✝) :
    topCatOpToFrm.map f = TopologicalSpace.Opens.comap f.unop
    source
    @[simp]
    theorem topCatOpToFrm_obj (X : TopCatᵒᵖ) :
    topCatOpToFrm.obj X = Frm.of (TopologicalSpace.Opens ↑(Opposite.unop X))
    source
    instance CompHausOpToFrame.faithful :
    (compHausToTop.op.comp topCatOpToFrm).Faithful