mathlib documentation

order.category.Frame

The category of frames #

This file defines Frame, the category of frames.

References #

nLab, Frm

def Frame :

Type (u_1+1)

The category of frames.

Equations

Frame = category_theory.bundled order.frame

Instances for Frame

@[protected, instance]

def Frame.has_coe_to_sort :

has_coe_to_sort Frame (Type u_1)

Equations

Frame.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

@[protected, instance]

def Frame.order.frame (X : Frame) :

order.frame ↥X

Equations

Frame.order.frame X = X.str

def Frame.of (α : Type u_1) [order.frame α] :

Construct a bundled Frame from a frame.

Equations

Frame.of α = category_theory.bundled.of α

@[simp]

theorem Frame.coe_of (α : Type u_1) [order.frame α] :

↥(Frame.of α) = α

@[protected, instance]

def Frame.inhabited :

inhabited Frame

Equations

Frame.inhabited = {default := Frame.of punit (complete_distrib_lattice.to_frame punit)}

@[reducible]

def Frame.hom (α : Type u_1) (β : Type u_2) [order.frame α] [order.frame β] :

Type (max u_1 u_2)

An abbreviation of frame_hom that assumes frame instead of the weaker complete_lattice. Necessary for the category theory machinery.

@[protected, instance]

def Frame.bundled_hom :

category_theory.bundled_hom Frame.hom

Equations

Frame.bundled_hom = {to_fun := λ (α β : Type u_1) [_inst_1 : order.frame α] [_inst_2 : order.frame β], coe_fn, id := λ (α : Type u_1) [_inst_1 : order.frame α], frame_hom.id α, comp := λ (α β γ : Type u_1) [_inst_1 : order.frame α] [_inst_2 : order.frame β] [_inst_3 : order.frame γ], frame_hom.comp, hom_ext := Frame.bundled_hom._proof_1, id_to_fun := Frame.bundled_hom._proof_2, comp_to_fun := Frame.bundled_hom._proof_3}

@[protected, instance]

def Frame.concrete_category :

category_theory.concrete_category Frame

@[protected, instance]

def Frame.large_category :

category_theory.large_category Frame

@[protected, instance]

def Frame.has_forget_to_Lattice :

category_theory.has_forget₂ Frame Lattice

Equations

Frame.has_forget_to_Lattice = {forget₂ := {obj := λ (X : Frame), {α := ↥X, str := conditionally_complete_lattice.to_lattice ↥X complete_lattice.to_conditionally_complete_lattice}, map := λ (X Y : Frame), frame_hom.to_lattice_hom, map_id' := Frame.has_forget_to_Lattice._proof_1, map_comp' := Frame.has_forget_to_Lattice._proof_2}, forget_comp := Frame.has_forget_to_Lattice._proof_3}

def Frame.iso.mk {α β : Frame} (e : ↥α ≃o ↥β) :

α ≅ β

Constructs an isomorphism of frames from an order isomorphism between them.

Equations

Frame.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem Frame.iso.mk_hom {α β : Frame} (e : ↥α ≃o ↥β) :

(Frame.iso.mk e).hom = ↑e

@[simp]

theorem Frame.iso.mk_inv {α β : Frame} (e : ↥α ≃o ↥β) :

(Frame.iso.mk e).inv = ↑(e.symm)

@[simp]

theorem Top_op_to_Frame_obj (X : Top ᵒᵖ) :

Top_op_to_Frame.obj X = Frame.of (topological_space.opens ↥(opposite.unop X))

@[simp]

theorem Top_op_to_Frame_map (X Y : Top ᵒᵖ) (f : X ⟶ Y) :

Top_op_to_Frame.map f = topological_space.opens.comap f.unop

def Top_op_to_Frame :

Top ᵒᵖ ⥤ Frame

The forgetful functor from Topᵒᵖ to Frame.

Equations

Top_op_to_Frame = {obj := λ (X : Top ᵒᵖ), Frame.of (topological_space.opens ↥(opposite.unop X)), map := λ (X Y : Top ᵒᵖ) (f : X ⟶ Y), topological_space.opens.comap f.unop, map_id' := Top_op_to_Frame._proof_1, map_comp' := Top_op_to_Frame._proof_2}

@[protected, instance]

def CompHaus_op_to_Frame.faithful :

category_theory.faithful (CompHaus_to_Top.op ⋙ Top_op_to_Frame)