The category of pointed types

This defines Pointed, the category of pointed types.

TODO

• Monoidal structure
• Upgrade typeToPointed to an equivalence

structure Pointed : Type (u + 1)

The category of pointed types.

• X : Type u

  the underlying type

• point : self.X

  the distinguished element

instance Pointed.instCoeSortPointedType : CoeSort Pointed (Type u_3)

Equations

• Pointed.instCoeSortPointedType = { coe := Pointed.X }

def Pointed.of {X : Type u_3} (point : X) : Pointed

Turns a point into a pointed type.

Equations

• Pointed.of point = { X := X, point := point }

@[simp]

theorem Pointed.coe_of {X : Type u_3} (point : X) : (Pointed.of point).X = X

def Prod.Pointed {X : Type u_3} (point : X) : Pointed

Alias of Pointed.of.

---

Turns a point into a pointed type.

Equations

• @Prod.Pointed = @Pointed.of

instance Pointed.instInhabitedPointed : Inhabited Pointed

Equations

• Pointed.instInhabitedPointed = { default := Pointed.of ((), ()) }

theorem Pointed.Hom.ext {X : Pointed} {Y : Pointed} (x : Pointed.Hom X Y) (y : Pointed.Hom X Y) (toFun : x.toFun = y.toFun) : x = y

theorem Pointed.Hom.ext_iff {X : Pointed} {Y : Pointed} (x : Pointed.Hom X Y) (y : Pointed.Hom X Y) : x = y ↔ x.toFun = y.toFun

structure Pointed.Hom (X : Pointed) (Y : Pointed) : Type u

Morphisms in Pointed.

• toFun : X.X → Y.X

  the underlying map

• map_point : self.toFun X.point = Y.point

  compatibility with the distinguished points

@[simp]

theorem Pointed.Hom.id_toFun (X : Pointed) (a : X.X) : (Pointed.Hom.id X).toFun a = id a

def Pointed.Hom.id (X : Pointed) : Pointed.Hom X X

The identity morphism of X : Pointed.

Equations

• Pointed.Hom.id X = { toFun := id, map_point := (_ : id X.point = id X.point) }

instance Pointed.Hom.instInhabitedHom (X : Pointed) : Inhabited (Pointed.Hom X X)

Equations

• Pointed.Hom.instInhabitedHom X = { default := Pointed.Hom.id X }

@[simp]

theorem Pointed.Hom.comp_toFun {X : Pointed} {Y : Pointed} {Z : Pointed} (f : Pointed.Hom X Y) (g : Pointed.Hom Y Z) : ∀ (a : X.X), (Pointed.Hom.comp f g).toFun a = (g.toFun ∘ f.toFun) a

def Pointed.Hom.comp {X : Pointed} {Y : Pointed} {Z : Pointed} (f : Pointed.Hom X Y) (g : Pointed.Hom Y Z) : Pointed.Hom X Z

Composition of morphisms of Pointed.

Equations

• Pointed.Hom.comp f g = { toFun := g.toFun ∘ f.toFun, map_point := (_ : (g.toFun ∘ f.toFun) X.point = Z.point) }

instance Pointed.largeCategory : CategoryTheory.LargeCategory Pointed

Equations

• Pointed.largeCategory = CategoryTheory.Category.mk

instance Pointed.concreteCategory : CategoryTheory.ConcreteCategory Pointed

Equations

• Pointed.concreteCategory = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.mk { obj := Pointed.X, map := @Pointed.Hom.toFun })

@[simp]

theorem Pointed.Iso.mk_hom_toFun {α : Pointed} {β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : α.X) : (Pointed.Iso.mk e he).hom.toFun a = e a

@[simp]

theorem Pointed.Iso.mk_inv_toFun {α : Pointed} {β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) (a : β.X) : (Pointed.Iso.mk e he).inv.toFun a = e.symm a

def Pointed.Iso.mk {α : Pointed} {β : Pointed} (e : α.X ≃ β.X) (he : e α.point = β.point) : α ≅ β

Constructs an isomorphism between pointed types from an equivalence that preserves the point between them.

Equations

• Pointed.Iso.mk e he = CategoryTheory.Iso.mk { toFun := ⇑e, map_point := he } { toFun := ⇑e.symm, map_point := (_ : e.symm β.point = α.point) }

@[simp]

theorem typeToPointed_map_toFun : ∀ {X Y : Type u} (f : X ⟶ Y) (a : Option X), (typeToPointed.toPrefunctor.map f).toFun a = Option.map f a

@[simp]

theorem typeToPointed_obj_point (X : Type u) : (typeToPointed.toPrefunctor.obj X).point = none

@[simp]

theorem typeToPointed_obj_X (X : Type u) : (typeToPointed.toPrefunctor.obj X).X = Option X

def typeToPointed : CategoryTheory.Functor (Type u) Pointed

Option as a functor from types to pointed types. This is the free functor.

Equations

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

def typeToPointedForgetAdjunction : typeToPointed ⊣ CategoryTheory.forget Pointed

typeToPointed is the free functor.

Equations

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