Documentation

Mathlib.Topology.Category.CompHaus.Frm

The forgetful functor from TopCatᵒᵖ to Frm.

source
🔸 coverage
def topCatOpToFrm :
CategoryTheory.Functor TopCatᵒᵖ Frm

The forgetful functor from TopCatᵒᵖ to Frm.

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