mathlib documentation

topology.category.Top.open_nhds

def topological_space.open_nhds {X : Top} (x : ↥X) :

Type u

Equations

topological_space.open_nhds x = {U // x ∈ U}

@[instance]

def topological_space.open_nhds.partial_order {X : Top} (x : ↥X) :

partial_order (topological_space.open_nhds x)

Equations

topological_space.open_nhds.partial_order x = {le := λ (U V : topological_space.open_nhds x), U.val ≤ V.val, lt := preorder.lt._default (λ (U V : topological_space.open_nhds x), U.val ≤ V.val), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[instance]

def topological_space.open_nhds.lattice {X : Top} (x : ↥X) :

lattice (topological_space.open_nhds x)

Equations

topological_space.open_nhds.lattice x = {sup := λ (U V : topological_space.open_nhds x), ⟨U.val ⊔ V.val, _⟩, le := partial_order.le (topological_space.open_nhds.partial_order x), lt := partial_order.lt (topological_space.open_nhds.partial_order x), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := λ (U V : topological_space.open_nhds x), ⟨U.val ⊓ V.val, _⟩, inf_le_left := _, inf_le_right := _, le_inf := _}

@[instance]

def topological_space.open_nhds.order_top {X : Top} (x : ↥X) :

order_top (topological_space.open_nhds x)

Equations

topological_space.open_nhds.order_top x = {top := ⟨⊤, trivial⟩, le := partial_order.le (topological_space.open_nhds.partial_order x), lt := partial_order.lt (topological_space.open_nhds.partial_order x), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := _}

@[instance]

def topological_space.open_nhds.open_nhds_category {X : Top} (x : ↥X) :

category_theory.category (topological_space.open_nhds x)

Equations

topological_space.open_nhds.open_nhds_category x = _.mpr (category_theory.full_subcategory (λ (U : topological_space.opens ↥X), x ∈ U))

@[instance]

def topological_space.open_nhds.opens_nhds_hom_has_coe_to_fun {X : Top} {x : ↥X} {U V : topological_space.open_nhds x} :

has_coe_to_fun (U ⟶ V)

Equations

topological_space.open_nhds.opens_nhds_hom_has_coe_to_fun = {F := λ (f : U ⟶ V), ↥(U.val) → ↥(V.val), coe := λ (f : U ⟶ V) (x_1 : ↥(U.val)), ⟨↑x_1, _⟩}

def topological_space.open_nhds.inf_le_left {X : Top} {x : ↥X} (U V : topological_space.open_nhds x) :

U ⊓ V ⟶ U

The inclusion U ⊓ V ⟶ U as a morphism in the category of open sets.

Equations

U.inf_le_left V = category_theory.hom_of_le _

def topological_space.open_nhds.inf_le_right {X : Top} {x : ↥X} (U V : topological_space.open_nhds x) :

U ⊓ V ⟶ V

The inclusion U ⊓ V ⟶ V as a morphism in the category of open sets.

Equations

U.inf_le_right V = category_theory.hom_of_le _

def topological_space.open_nhds.inclusion {X : Top} (x : ↥X) :

topological_space.open_nhds x ⥤ topological_space.opens ↥X

Equations

topological_space.open_nhds.inclusion x = category_theory.full_subcategory_inclusion (λ (U : topological_space.opens ↥X), x ∈ U)

@[simp]

theorem topological_space.open_nhds.inclusion_obj {X : Top} (x : ↥X) (U : topological_space.opens ↥X) (p : x ∈ U) :

(topological_space.open_nhds.inclusion x).obj ⟨U, p⟩ = U

@[instance]

def topological_space.open_nhds.open_nhds_is_filtered {X : Top} (x : ↥X) :

category_theory.is_filtered (topological_space.open_nhds x)ᵒᵖ

def topological_space.open_nhds.map {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

topological_space.open_nhds (⇑f x) ⥤ topological_space.open_nhds x

Equations

topological_space.open_nhds.map f x = {obj := λ (U : topological_space.open_nhds (⇑f x)), ⟨(topological_space.opens.map f).obj U.val, _⟩, map := λ (U V : topological_space.open_nhds (⇑f x)) (i : U ⟶ V), (topological_space.opens.map f).map i, map_id' := _, map_comp' := _}

@[simp]

theorem topological_space.open_nhds.map_obj {X Y : Top} (f : X ⟶ Y) (x : ↥X) (U : topological_space.opens ↥Y) (q : ⇑f x ∈ U) :

(topological_space.open_nhds.map f x).obj ⟨U, q⟩ = ⟨(topological_space.opens.map f).obj U, q⟩

@[simp]

theorem topological_space.open_nhds.map_id_obj {X : Top} (x : ↥X) (U : topological_space.open_nhds (⇑(𝟙 X) x)) :

(topological_space.open_nhds.map (𝟙 X) x).obj U = U

@[simp]

theorem topological_space.open_nhds.map_id_obj' {X : Top} (x : ↥X) (U : set ↥X) (p : is_open U) (q : ⇑(𝟙 X) x ∈ ⟨U, p⟩) :

(topological_space.open_nhds.map (𝟙 X) x).obj ⟨⟨U, p⟩, q⟩ = ⟨⟨U, p⟩, q⟩

@[simp]

theorem topological_space.open_nhds.map_id_obj_unop {X : Top} (x : ↥X) (U : (topological_space.open_nhds x)ᵒᵖ) :

(topological_space.open_nhds.map (𝟙 X) x).obj (opposite.unop U) = opposite.unop U

@[simp]

theorem topological_space.open_nhds.op_map_id_obj {X : Top} (x : ↥X) (U : (topological_space.open_nhds x)ᵒᵖ) :

(topological_space.open_nhds.map (𝟙 X) x).op.obj U = U

def topological_space.open_nhds.inclusion_map_iso {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f ≅ topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x

Equations

topological_space.open_nhds.inclusion_map_iso f x = category_theory.nat_iso.of_components (λ (U : topological_space.open_nhds (⇑f x)), {hom := 𝟙 ((topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f).obj U), inv := 𝟙 ((topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x).obj U), hom_inv_id' := _, inv_hom_id' := _}) _

@[simp]

theorem topological_space.open_nhds.inclusion_map_iso_hom {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

(topological_space.open_nhds.inclusion_map_iso f x).hom = 𝟙 (topological_space.open_nhds.inclusion (⇑f x) ⋙ topological_space.opens.map f)

@[simp]

theorem topological_space.open_nhds.inclusion_map_iso_inv {X Y : Top} (f : X ⟶ Y) (x : ↥X) :

(topological_space.open_nhds.inclusion_map_iso f x).inv = 𝟙 (topological_space.open_nhds.map f x ⋙ topological_space.open_nhds.inclusion x)