The category of frames #

This file defines Frm, the category of frames.

References #

nLab, Frm

source

structure Frm :

Type (u_1 + 1)

The category of frames.

of :: (

carrier : Type u_1
The underlying frame.
str : Order.Frame ↑self

)

Instances For

source

instance Frm.instCoeSortType :

CoeSort Frm (Type u_1)

Equations

Frm.instCoeSortType = { coe := Frm.carrier }

source

structure Frm.Hom (X Y : Frm) :

Type u

The type of morphisms in Frm R.

hom' : FrameHom ↑X ↑Y
The underlying FrameHom.

Instances For

source

theorem Frm.Hom.ext {X Y : Frm} {x y : X.Hom Y} (hom' : x.hom' = y.hom') :

x = y

source

theorem Frm.Hom.ext_iff {X Y : Frm} {x y : X.Hom Y} :

x = y ↔ x.hom' = y.hom'

source

instance Frm.instCategory :

CategoryTheory.Category.{u, u + 1} Frm

Equations

One or more equations did not get rendered due to their size.

source

instance Frm.instConcreteCategoryFrameHomCarrier :

CategoryTheory.ConcreteCategory Frm fun (x1 x2 : Frm) => FrameHom ↑x1 ↑x2

Equations

One or more equations did not get rendered due to their size.

source

@[reducible, inline]

abbrev Frm.Hom.hom {X Y : Frm} (f : X.Hom Y) :

FrameHom ↑X ↑Y

Turn a morphism in Frm back into a FrameHom.

Equations

f.hom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

abbrev Frm.ofHom {X Y : Type u} [Order.Frame X] [Order.Frame Y] (f : FrameHom X Y) :

{ carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a FrameHom as a morphism in Frm.

Equations

Frm.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

def Frm.Hom.Simps.hom (X Y : Frm) (f : X.Hom Y) :

FrameHom ↑X ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

Frm.Hom.Simps.hom X Y f = f.hom

Instances For

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

source

@[simp]

theorem Frm.coe_id {X : Frm} :

⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

source

@[simp]

theorem Frm.coe_comp {X Y Z : Frm} {f : X ⟶ Y} {g : Y ⟶ Z} :

⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

source

@[simp]

theorem Frm.forget_map {X Y : Frm} (f : X ⟶ Y) :

(CategoryTheory.forget Frm).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

source

theorem Frm.ext {X Y : Frm} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) :

f = g

source

theorem Frm.ext_iff {X Y : Frm} {f g : X ⟶ Y} :

f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

source

theorem Frm.coe_of (X : Type u) [Order.Frame X] :

↑{ carrier := X, str := inst✝ } = X

source

@[simp]

theorem Frm.hom_id {X : Frm} :

Hom.hom (CategoryTheory.CategoryStruct.id X) = FrameHom.id ↑X

source

theorem Frm.id_apply (X : Frm) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

source

@[simp]

theorem Frm.hom_comp {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) :

Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

source

theorem Frm.comp_apply {X Y Z : Frm} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

source

theorem Frm.hom_ext {X Y : Frm} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) :

f = g

source

theorem Frm.hom_ext_iff {X Y : Frm} {f g : X ⟶ Y} :

f = g ↔ Hom.hom f = Hom.hom g

source

@[simp]

theorem Frm.hom_ofHom {X Y : Type u} [Order.Frame X] [Order.Frame Y] (f : FrameHom X Y) :

Hom.hom (ofHom f) = f

source

@[simp]

theorem Frm.ofHom_hom {X Y : Frm} (f : X ⟶ Y) :

ofHom (Hom.hom f) = f

source

@[simp]

theorem Frm.ofHom_id {X : Type u} [Order.Frame X] :

ofHom (FrameHom.id X) = CategoryTheory.CategoryStruct.id { carrier := X, str := inst✝ }

source

@[simp]

theorem Frm.ofHom_comp {X Y Z : Type u} [Order.Frame X] [Order.Frame Y] [Order.Frame Z] (f : FrameHom X Y) (g : FrameHom Y Z) :

ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

source

theorem Frm.ofHom_apply {X Y : Type u} [Order.Frame X] [Order.Frame Y] (f : FrameHom X Y) (x : X) :

(CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

source

theorem Frm.inv_hom_apply {X Y : Frm} (e : X ≅ Y) (x : ↑X) :

(CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

source

theorem Frm.hom_inv_apply {X Y : Frm} (e : X ≅ Y) (s : ↑Y) :

(CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

source

instance Frm.instInhabited :

Inhabited Frm

Equations

Frm.instInhabited = { default := { carrier := PUnit.{?u.2 + 1}, str := CompleteBooleanAlgebra.toCompleteDistribLattice.toFrame } }

source

instance Frm.hasForgetToLat :

CategoryTheory.HasForget₂ Frm Lat

Equations

One or more equations did not get rendered due to their size.

source

def Frm.Iso.mk {α β : Frm} (e : ↑α ≃o ↑β) :

α ≅ β

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Frm.Iso.mk_inv {α β : Frm} (e : ↑α ≃o ↑β) :

(mk e).inv = ofHom { toFun := ⇑e.symm, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

source

@[simp]

theorem Frm.Iso.mk_hom {α β : Frm} (e : ↑α ≃o ↑β) :

(mk e).hom = ofHom { toFun := ⇑e, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

Documentation

Mathlib.Order.Category.Frm

The category of frames #

References #