The category of frames.

Equations

• Frm = category_theory.bundled order.frame

Instances for Frm

• Frm.has_coe_to_sort
• Frm.inhabited
• Frm.large_category
• Frm.concrete_category
• Frm.has_forget_to_Lat

Equations

• Frm.has_coe_to_sort = category_theory.bundled.has_coe_to_sort

Equations

• Frm.order.frame X = X.str

Construct a bundled Frm from a frame.

Equations

• Frm.of α = category_theory.bundled.of α

Equations

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

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

Equations

• Frm.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 := Frm.bundled_hom._proof_1, id_to_fun := Frm.bundled_hom._proof_2, comp_to_fun := Frm.bundled_hom._proof_3}

Equations

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

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

Equations

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

The forgetful functor from Topᵒᵖ to Frm.

Equations

• Top_op_to_Frame = {obj := λ (X : Topᵒᵖ), Frm.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}